:: EUCLMETR semantic presentation

definition

let c₁ be OrtAfSp;
attr a₁ is Euclidean means :Def1: :: EUCLMETR:def 1
for b₁, b₂, b₃, b₄ being Element of the carrier of a₁ st b₁,b₂ _|_ b₃,b₄ & b₂,b₃ _|_ b₁,b₄ holds
b₂,b₄ _|_ b₁,b₃;

end;

:: deftheorem Def1 defines Euclidean EUCLMETR:def 1 :

definition

let c₁ be OrtAfSp;
attr a₁ is Pappian means :Def2: :: EUCLMETR:def 2
Af a₁ is Pappian;

end;

:: deftheorem Def2 defines Pappian EUCLMETR:def 2 :

definition

let c₁ be OrtAfSp;
attr a₁ is Desarguesian means :Def3: :: EUCLMETR:def 3
Af a₁ is Desarguesian;

end;

:: deftheorem Def3 defines Desarguesian EUCLMETR:def 3 :

definition

let c₁ be OrtAfSp;
attr a₁ is Fanoian means :Def4: :: EUCLMETR:def 4
Af a₁ is Fanoian;

end;

:: deftheorem Def4 defines Fanoian EUCLMETR:def 4 :

definition

let c₁ be OrtAfSp;
attr a₁ is Moufangian means :Def5: :: EUCLMETR:def 5
Af a₁ is Moufangian;

end;

:: deftheorem Def5 defines Moufangian EUCLMETR:def 5 :

definition

let c₁ be OrtAfSp;
attr a₁ is translation means :Def6: :: EUCLMETR:def 6
Af a₁ is translational;

end;

:: deftheorem Def6 defines translation EUCLMETR:def 6 :

definition

end;

:: deftheorem Def7 defines Homogeneous EUCLMETR:def 7 :

theorem Th1: :: EUCLMETR:1

for b₁ being OrtAfSp
for b₂, b₃, b₄ being Element of b₁ st not LIN b₂,b₃,b₄ holds
( b₂ <> b₃ & b₃ <> b₄ & b₂ <> b₄ )

proof end;

theorem Th2: :: EUCLMETR:2

for b₁ being OrtAfPl
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of the carrier of b₁ st b₂,b₃ _|_ b₆ & b₄,b₅ _|_ b₆ holds
( b₂,b₃ // b₄,b₅ & b₂,b₃ // b₅,b₄ )

proof end;

theorem Th3: :: EUCLMETR:3

for b₁ being OrtAfPl
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of the carrier of b₁ st b₂ <> b₃ & ( b₂,b₃ _|_ b₅ or b₃,b₂ _|_ b₅ ) & ( b₂,b₃ _|_ b₄ or b₃,b₂ _|_ b₄ ) holds
b₅ // b₄

proof end;

theorem Th4: :: EUCLMETR:4

for b₁ being OrtAfSp
for b₂, b₃, b₄ being Element of b₁ st LIN b₂,b₃,b₄ holds
( LIN b₂,b₄,b₃ & LIN b₃,b₂,b₄ & LIN b₃,b₄,b₂ & LIN b₄,b₂,b₃ & LIN b₄,b₃,b₂ )

proof end;

theorem Th5: :: EUCLMETR:5

for b₁ being OrtAfPl
for b₂, b₃, b₄ being Element of b₁ st not LIN b₂,b₃,b₄ holds
ex b₅ being Element of b₁ st
( b₅,b₂ _|_ b₃,b₄ & b₅,b₃ _|_ b₂,b₄ )

proof end;

theorem Th6: :: EUCLMETR:6

for b₁ being OrtAfPl
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₅,b₂ _|_ b₃,b₄ & b₅,b₃ _|_ b₂,b₄ & b₆,b₂ _|_ b₃,b₄ & b₆,b₃ _|_ b₂,b₄ holds
b₅ = b₆

proof end;

theorem Th7: :: EUCLMETR:7

for b₁ being OrtAfPl
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ _|_ b₄,b₅ & b₃,b₄ _|_ b₂,b₅ & LIN b₂,b₃,b₄ & not b₂ = b₄ & not b₂ = b₃ holds
b₃ = b₄

proof end;

theorem Th8: :: EUCLMETR:8

for b₁ being OrtAfPl holds
( b₁ is Euclidean iff 3H_holds_in b₁ )

proof end;

theorem Th9: :: EUCLMETR:9

for b₁ being OrtAfPl holds
( b₁ is Homogeneous iff ODES_holds_in b₁ )

proof end;

Lemma16: for b₁ being OrtAfPl holds
( PAP_holds_in b₁ iff Af b₁ satisfies_PAP' )

proof end;

theorem Th10: :: EUCLMETR:10

for b₁ being OrtAfPl holds
( b₁ is Pappian iff PAP_holds_in b₁ )

proof end;

Lemma18: for b₁ being OrtAfPl holds
( DES_holds_in b₁ iff Af b₁ satisfies_DES' )

proof end;

theorem Th11: :: EUCLMETR:11

for b₁ being OrtAfPl holds
( b₁ is Desarguesian iff DES_holds_in b₁ )

proof end;

theorem Th12: :: EUCLMETR:12

for b₁ being OrtAfPl holds
( b₁ is Moufangian iff TDES_holds_in b₁ )

proof end;

Lemma20: for b₁ being OrtAfPl holds
( des_holds_in b₁ iff Af b₁ satisfies_des' )

proof end;

theorem Th13: :: EUCLMETR:13

for b₁ being OrtAfPl holds
( b₁ is translation iff des_holds_in b₁ )

proof end;

theorem Th14: :: EUCLMETR:14

for b₁ being OrtAfPl st b₁ is Homogeneous holds
b₁ is Desarguesian

proof end;

theorem Th15: :: EUCLMETR:15

for b₁ being OrtAfPl st b₁ is Euclidean & b₁ is Desarguesian holds
b₁ is Pappian

proof end;

theorem Th16: :: EUCLMETR:16

proof end;

theorem Th17: :: EUCLMETR:17

for b₁ being OrtAfPl
for b₂, b₃, b₄, b₅ being Element of b₁ st not LIN b₂,b₃,b₅ & b₂ <> b₄ holds
ex b₆ being Element of b₁ st
( b₂,b₅ _|_ b₂,b₆ & b₃,b₅ _|_ b₄,b₆ )

proof end;

Lemma24: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds
( (b₂ - b₄) - (b₃ - b₄) = b₂ - b₃ & (b₂ + b₄) - (b₃ + b₄) = b₂ - b₃ )

proof end;

Lemma25: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆ being Real holds
( PProJ b₂,b₃,((b₄ * b₂) + (b₅ * b₃)),(((b₆ * b₅) * b₂) + ((- (b₆ * b₄)) * b₃)) = 0 & (b₄ * b₂) + (b₅ * b₃),((b₆ * b₅) * b₂) + ((- (b₆ * b₄)) * b₃) are_Ort_wrt b₂,b₃ )

proof end;

theorem Th18: :: EUCLMETR:18

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇ being Real st Gen b₂,b₃ & 0. b₁ <> b₄ & 0. b₁ <> b₅ & b₄,b₅ are_Ort_wrt b₂,b₃ & b₄ = (b₆ * b₂) + (b₇ * b₃) holds
ex b₈ being Real st
( b₈ <> 0 & b₅ = ((b₈ * b₇) * b₂) + ((- (b₈ * b₆)) * b₃) )

proof end;

theorem Th19: :: EUCLMETR:19

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ & 0. b₁ <> b₄ & 0. b₁ <> b₅ & b₄,b₅ are_Ort_wrt b₂,b₃ holds
ex b₆ being Real st
for b₇, b₈ being Real holds
( (b₇ * b₂) + (b₈ * b₃),((b₆ * b₈) * b₂) + ((- (b₆ * b₇)) * b₃) are_Ort_wrt b₂,b₃ & ((b₇ * b₂) + (b₈ * b₃)) - b₄,(((b₆ * b₈) * b₂) + ((- (b₆ * b₇)) * b₃)) - b₅ are_Ort_wrt b₂,b₃ )

proof end;

Lemma28: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Real holds ((b₄ * b₂) + (b₅ * b₃)) - ((b₆ * b₂) + (b₇ * b₃)) = ((b₄ - b₆) * b₂) + ((b₅ - b₇) * b₃)

proof end;

Lemma29: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇ being Real st (b₄ * b₂) + (b₆ * b₃) = (b₅ * b₂) + (b₇ * b₃) holds
( b₄ = b₅ & b₆ = b₇ )

proof end;

theorem Th20: :: EUCLMETR:20

canceled;

theorem Th21: :: EUCLMETR:21

for b₁ being OrtAfPl
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ st Gen b₃,b₄ & b₁ = AMSpace b₂,b₃,b₄ holds
LIN_holds_in b₁

proof end;

theorem Th22: :: EUCLMETR:22

proof end;

theorem Th23: :: EUCLMETR:23

for b₁ being OrtAfPl
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ st Gen b₃,b₄ & b₁ = AMSpace b₂,b₃,b₄ holds
b₁ is Homogeneous

proof end;

registration

cluster Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous ParOrtStr ;
existence

proof end;

end;

registration

cluster Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous ParOrtStr ;
existence

proof end;

end;

theorem Th24: :: EUCLMETR:24

for b₁ being OrtAfPl
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of b₂ st Gen b₃,b₄ & b₁ = AMSpace b₂,b₃,b₄ holds
b₁ is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl

proof end;

registration

let c₁ be Pappian OrtAfPl;
cluster Af a₁ -> Pappian ;
correctness by Def2;

end;

registration

let c₁ be Desarguesian OrtAfPl;
cluster Af a₁ -> Desarguesian ;
correctness by Def3;

end;

registration

let c₁ be Moufangian OrtAfPl;
cluster Af a₁ -> Moufangian ;
correctness by Def5;

end;

registration

let c₁ be translation OrtAfPl;
cluster Af a₁ -> translational ;
correctness by Def6;

end;

registration

let c₁ be Fanoian OrtAfPl;
cluster Af a₁ -> Fanoian ;
correctness by Def4;

end;

registration

let c₁ be Homogeneous OrtAfPl;
cluster Af a₁ -> Desarguesian ;
correctness

proof end;

end;

registration

let c₁ be Euclidean Desarguesian OrtAfPl;
cluster Af a₁ -> Pappian Desarguesian ;
correctness

proof end;

end;

registration

let c₁ be Pappian OrtAfSp;
cluster Af a₁ -> Pappian ;
correctness by Def2;

end;

registration

let c₁ be Desarguesian OrtAfSp;
cluster Af a₁ -> Desarguesian ;
correctness by Def3;

end;

registration

let c₁ be Moufangian OrtAfSp;
cluster Af a₁ -> Moufangian ;
correctness by Def5;

end;

registration

let c₁ be translation OrtAfSp;
cluster Af a₁ -> translational ;
correctness by Def6;

end;

registration

let c₁ be Fanoian OrtAfSp;
cluster Af a₁ -> Fanoian ;
correctness by Def4;

end;