:: EUCLMETR semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be OrtAfSp;
attr IT is Euclidean means :Def1: :: EUCLMETR:def 1
for a, b, c, d being Element of the carrier of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c;
end;

:: deftheorem Def1 defines Euclidean EUCLMETR:def 1 :
for IT being OrtAfSp holds
( IT is Euclidean iff for a, b, c, d being Element of the carrier of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c );

definition
let IT be OrtAfSp;
attr IT is Pappian means :Def2: :: EUCLMETR:def 2
 Af IT is Pappian;
end;

:: deftheorem Def2 defines Pappian EUCLMETR:def 2 :
for IT being OrtAfSp holds
( IT is Pappian iff Af IT is Pappian );

definition
let IT be OrtAfSp;
attr IT is Desarguesian means :Def3: :: EUCLMETR:def 3
 Af IT is Desarguesian;
end;

:: deftheorem Def3 defines Desarguesian EUCLMETR:def 3 :
for IT being OrtAfSp holds
( IT is Desarguesian iff Af IT is Desarguesian );

definition
let IT be OrtAfSp;
attr IT is Fanoian means :Def4: :: EUCLMETR:def 4
 Af IT is Fanoian;
end;

:: deftheorem Def4 defines Fanoian EUCLMETR:def 4 :
for IT being OrtAfSp holds
( IT is Fanoian iff Af IT is Fanoian );

definition
let IT be OrtAfSp;
attr IT is Moufangian means :Def5: :: EUCLMETR:def 5
 Af IT is Moufangian;
end;

:: deftheorem Def5 defines Moufangian EUCLMETR:def 5 :
for IT being OrtAfSp holds
( IT is Moufangian iff Af IT is Moufangian );

definition
let IT be OrtAfSp;
attr IT is translation means :Def6: :: EUCLMETR:def 6
 Af IT is translational;
end;

:: deftheorem Def6 defines translation EUCLMETR:def 6 :
for IT being OrtAfSp holds
( IT is translation iff Af IT is translational );

definition
let IT be OrtAfSp;
attr IT is Homogeneous means :Def7: :: EUCLMETR:def 7
for o, a, a1, b, b1, c, c1 being Element of IT st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1;
end;

:: deftheorem Def7 defines Homogeneous EUCLMETR:def 7 :
for IT being OrtAfSp holds
( IT is Homogeneous iff for o, a, a1, b, b1, c, c1 being Element of IT st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );

theorem Th1: :: EUCLMETR:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MP being OrtAfSp
for a, b, c being Element of MP st not LIN a,b,c holds
( a <> b & b <> c & a <> c )
proof end;

theorem Th2: :: EUCLMETR:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for a, b, c, d being Element of MS
for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
proof end;

theorem :: EUCLMETR:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for a, b being Element of MS
for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & ( a,b _|_ A or b,a _|_ A ) holds
K // A
proof end;

theorem Th4: :: EUCLMETR:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MP being OrtAfSp
for x, y, z being Element of MP st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
proof end;

theorem Th5: :: EUCLMETR:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
proof end;

theorem Th6: :: EUCLMETR:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for a, b, c, d1, d2 being Element of MS st not LIN a,b,c & d1,a _|_ b,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds
d1 = d2
proof end;

theorem Th7: :: EUCLMETR:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for a, b, c, d being Element of MS st a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c & not a = c & not a = b holds
b = c
proof end;

theorem Th8: :: EUCLMETR:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl holds
( MS is Euclidean iff 3H_holds_in MS )
proof end;

theorem Th9: :: EUCLMETR:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl holds
( MS is Homogeneous iff ODES_holds_in MS )
proof end;

Lm1: for MS being OrtAfPl holds
( PAP_holds_in MS iff Af MS satisfies_PAP' )
proof end;

theorem Th10: :: EUCLMETR:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl holds
( MS is Pappian iff PAP_holds_in MS )
proof end;

Lm2: for MS being OrtAfPl holds
( DES_holds_in MS iff Af MS satisfies_DES' )
proof end;

theorem Th11: :: EUCLMETR:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl holds
( MS is Desarguesian iff DES_holds_in MS )
proof end;

theorem :: EUCLMETR:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl holds
( MS is Moufangian iff TDES_holds_in MS )
proof end;

Lm3: for MS being OrtAfPl holds
( des_holds_in MS iff Af MS satisfies_des' )
proof end;

theorem :: EUCLMETR:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl holds
( MS is translation iff des_holds_in MS )
proof end;

theorem Th14: :: EUCLMETR:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl st MS is Homogeneous holds
MS is Desarguesian
proof end;

theorem Th15: :: EUCLMETR:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl st MS is Euclidean & MS is Desarguesian holds
MS is Pappian
proof end;

theorem Th16: :: EUCLMETR:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for o, c, c1, a, a1, a2 being Element of MS st not LIN o,c,a & o <> c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 holds
a1 = a2
proof end;

theorem :: EUCLMETR:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for o, c, c1, a being Element of MS st not LIN o,c,a & o <> c1 holds
ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
proof end;

Lm4: for V being RealLinearSpace
for u, v, y being VECTOR of V holds
( (u - y) - (v - y) = u - v & (u + y) - (v + y) = u - v )
proof end;

Lm5: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for a, b, c being Real holds
( PProJ w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y)) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
proof end;

theorem Th18: :: EUCLMETR:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u, v being VECTOR of V
for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
proof end;

theorem Th19: :: EUCLMETR:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u, v being VECTOR of V st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y holds
ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
proof end;

Lm6: for V being RealLinearSpace
for w, y being VECTOR of V
for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
proof end;

Lm7: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
proof end;

theorem :: EUCLMETR:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: EUCLMETR:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
LIN_holds_in MS
proof end;

theorem Th22: :: EUCLMETR:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for o, a, a1, b, b1, c, c1 being Element of MS st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 holds
b,c _|_ b1,c1
proof end;

theorem Th23: :: EUCLMETR:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
MS is Homogeneous
proof end;

registration
cluster Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous ParOrtStr ;
existence
ex b1 being OrtAfPl st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian )
proof end;
end;

registration
cluster Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous ParOrtStr ;
existence
ex b1 being OrtAfSp st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian )
proof end;
end;

theorem :: EUCLMETR:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
proof end;

registration
let MS be Pappian OrtAfPl;
cluster Af MS -> Pappian ;
correctness
coherence
Af MS is Pappian;
by Def2;
end;

registration
let MS be Desarguesian OrtAfPl;
cluster Af MS -> Desarguesian ;
correctness
coherence
Af MS is Desarguesian;
by Def3;
end;

registration
let MS be Moufangian OrtAfPl;
cluster Af MS -> Moufangian ;
correctness
coherence
Af MS is Moufangian;
by Def5;
end;

registration
let MS be translation OrtAfPl;
cluster Af MS -> translational ;
correctness
coherence
Af MS is translational;
by Def6;
end;

registration
let MS be Fanoian OrtAfPl;
cluster Af MS -> Fanoian ;
correctness
coherence
Af MS is Fanoian;
by Def4;
end;

registration
let MS be Homogeneous OrtAfPl;
cluster Af MS -> Desarguesian ;
correctness
coherence
Af MS is Desarguesian;
proof end;
end;

registration
let MS be Euclidean Desarguesian OrtAfPl;
cluster Af MS -> Pappian Desarguesian ;
correctness
coherence
Af MS is Pappian;
proof end;
end;

registration
let MS be Pappian OrtAfSp;
cluster Af MS -> Pappian ;
correctness
coherence
Af MS is Pappian;
by Def2;
end;

registration
let MS be Desarguesian OrtAfSp;
cluster Af MS -> Desarguesian ;
correctness
coherence
Af MS is Desarguesian;
by Def3;
end;

registration
let MS be Moufangian OrtAfSp;
cluster Af MS -> Moufangian ;
correctness
coherence
Af MS is Moufangian;
by Def5;
end;

registration
let MS be translation OrtAfSp;
cluster Af MS -> translational ;
correctness
coherence
Af MS is translational;
by Def6;
end;

registration
let MS be Fanoian OrtAfSp;
cluster Af MS -> Fanoian ;
correctness
coherence
Af MS is Fanoian;
by Def4;
end;