:: ANALMETR semantic presentation

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

proof end;

Lemma2: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds (0 * b₂) + (0 * b₃) = 0. b₁

proof end;

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

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
pred Gen c₂,c₃ means :Def1: :: ANALMETR:def 1
( ( for b₁ being VECTOR of a₁ ex b₂, b₃ being Real st b₁ = (b₂ * a₂) + (b₃ * a₃) ) & ( for b₁, b₂ being Real st (b₁ * a₂) + (b₂ * a₃) = 0. a₁ holds
( b₁ = 0 & b₂ = 0 ) ) );

end;

:: deftheorem Def1 defines Gen ANALMETR:def 1 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅ be VECTOR of c₁;
pred c₂,c₃ are_Ort_wrt c₄,c₅ means :Def2: :: ANALMETR:def 2
ex b₁, b₂, b₃, b₄ being Real st
( a₂ = (b₁ * a₄) + (b₂ * a₅) & a₃ = (b₃ * a₄) + (b₄ * a₅) & (b₁ * b₃) + (b₂ * b₄) = 0 );

end;

:: deftheorem Def2 defines are_Ort_wrt ANALMETR:def 2 :

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

proof end;

theorem Th1: :: ANALMETR:1

canceled;

theorem Th2: :: ANALMETR:2

canceled;

theorem Th3: :: ANALMETR:3

canceled;

theorem Th4: :: ANALMETR:4

canceled;

theorem Th5: :: ANALMETR:5

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₄,b₅ holds
( b₂,b₃ are_Ort_wrt b₄,b₅ iff for b₆, b₇, b₈, b₉ being Real st b₂ = (b₆ * b₄) + (b₇ * b₅) & b₃ = (b₈ * b₄) + (b₉ * b₅) holds
(b₆ * b₈) + (b₇ * b₉) = 0 )

proof end;

Lemma8: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
( b₂ <> 0. b₁ & b₃ <> 0. b₁ )

proof end;

theorem Th6: :: ANALMETR:6

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds b₂,b₃ are_Ort_wrt b₂,b₃

proof end;

theorem Th7: :: ANALMETR:7

ex b₁ being RealLinearSpaceex b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃

proof end;

theorem Th8: :: ANALMETR:8

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂,b₃ are_Ort_wrt b₄,b₅ holds
b₃,b₂ are_Ort_wrt b₄,b₅

proof end;

theorem Th9: :: ANALMETR:9

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅ being VECTOR of b₁ holds
( b₄, 0. b₁ are_Ort_wrt b₂,b₃ & 0. b₁,b₅ are_Ort_wrt b₂,b₃ )

proof end;

theorem Th10: :: ANALMETR:10

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇ being Real st b₂,b₃ are_Ort_wrt b₄,b₅ holds
b₆ * b₂,b₇ * b₃ are_Ort_wrt b₄,b₅

proof end;

theorem Th11: :: ANALMETR:11

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇ being Real st b₂,b₃ are_Ort_wrt b₄,b₅ holds
( b₆ * b₂,b₃ are_Ort_wrt b₄,b₅ & b₂,b₇ * b₃ are_Ort_wrt b₄,b₅ )

proof end;

theorem Th12: :: ANALMETR:12

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄ being VECTOR of b₁ ex b₅ being VECTOR of b₁ st
( b₄,b₅ are_Ort_wrt b₂,b₃ & b₅ <> 0. b₁ )

proof end;

theorem Th13: :: ANALMETR:13

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

proof end;

theorem Th14: :: ANALMETR:14

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅ are_Ort_wrt b₂,b₃ & b₄,b₆ are_Ort_wrt b₂,b₃ holds
( b₄,b₅ + b₆ are_Ort_wrt b₂,b₃ & b₄,b₅ - b₆ are_Ort_wrt b₂,b₃ )

proof end;

theorem Th15: :: ANALMETR:15

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₄ are_Ort_wrt b₂,b₃ holds
b₄ = 0. b₁

proof end;

theorem Th16: :: ANALMETR:16

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅ - b₆ are_Ort_wrt b₂,b₃ & b₅,b₆ - b₄ are_Ort_wrt b₂,b₃ holds
b₆,b₄ - b₅ are_Ort_wrt b₂,b₃

proof end;

theorem Th17: :: ANALMETR:17

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

proof end;

theorem Th18: :: ANALMETR:18

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds
( ( b₂,b₃ // b₄,b₅ or b₂,b₃ // b₅,b₄ ) iff ex b₆, b₇ being Real st
( b₆ * (b₃ - b₂) = b₇ * (b₅ - b₄) & ( b₆ <> 0 or b₇ <> 0 ) ) )

proof end;

theorem Th19: :: ANALMETR:19

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds
( [[b₂,b₃],[b₄,b₅]] in lambda (DirPar b₁) iff ex b₆, b₇ being Real st
( b₆ * (b₃ - b₂) = b₇ * (b₅ - b₄) & ( b₆ <> 0 or b₇ <> 0 ) ) )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇ be VECTOR of c₁;
pred c₂,c₃,c₄,c₅ are_Ort_wrt c₆,c₇ means :Def3: :: ANALMETR:def 3
a₃ - a₂,a₅ - a₄ are_Ort_wrt a₆,a₇;

end;

:: deftheorem Def3 defines are_Ort_wrt ANALMETR:def 3 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func Orthogonality c₁,c₂,c₃ -> Relation of [:the carrier of a₁,the carrier of a₁:] means :Def4: :: ANALMETR:def 4
for b₁, b₂ being set holds
( [b₁,b₂] in a₄ iff ex b₃, b₄, b₅, b₆ being VECTOR of a₁ st
( b₁ = [b₃,b₄] & b₂ = [b₅,b₆] & b₃,b₄,b₅,b₆ are_Ort_wrt a₂,a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Orthogonality ANALMETR:def 4 :

theorem Th20: :: ANALMETR:20

canceled;

theorem Th21: :: ANALMETR:21

canceled;

theorem Th22: :: ANALMETR:22

for b₁ being RealLinearSpace holds the carrier of (Lambda (OASpace b₁)) = the carrier of b₁

proof end;

theorem Th23: :: ANALMETR:23

for b₁ being RealLinearSpace holds the CONGR of (Lambda (OASpace b₁)) = lambda (DirPar b₁)

proof end;

theorem Th24: :: ANALMETR:24

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇, b₈, b₉ being Element of (Lambda (OASpace b₁)) st b₆ = b₂ & b₇ = b₃ & b₈ = b₄ & b₉ = b₅ holds
( b₆,b₇ // b₈,b₉ iff ex b₁₀, b₁₁ being Real st
( b₁₀ * (b₃ - b₂) = b₁₁ * (b₅ - b₄) & ( b₁₀ <> 0 or b₁₁ <> 0 ) ) )

proof end;

definition

attr a₁ is strict;
struct ParOrtStr -> AffinStruct ;
aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;
sel orthogonality c₁ -> Relation of [:the carrier of a₁,the carrier of a₁:];

end;

registration

cluster non empty ParOrtStr ;
existence

proof end;

end;

definition

let c₁ be non empty ParOrtStr ;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃ // c₄,c₅ means :Def5: :: ANALMETR:def 5
[[a₂,a₃],[a₄,a₅]] in the CONGR of a₁;
pred c₂,c₃ _|_ c₄,c₅ means :Def6: :: ANALMETR:def 6
[[a₂,a₃],[a₄,a₅]] in the orthogonality of a₁;

end;

:: deftheorem Def5 defines // ANALMETR:def 5 :

:: deftheorem Def6 defines _|_ ANALMETR:def 6 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func AMSpace c₁,c₂,c₃ -> strict ParOrtStr equals :: ANALMETR:def 7
ParOrtStr(# the carrier of a₁,(lambda (DirPar a₁)),(Orthogonality a₁,a₂,a₃) #);
correctness ;

end;

:: deftheorem Def7 defines AMSpace ANALMETR:def 7 :

registration

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
cluster AMSpace a₁,a₂,a₃ -> non empty strict ;
coherence

proof end;

end;

theorem Th25: :: ANALMETR:25

canceled;

theorem Th26: :: ANALMETR:26

canceled;

theorem Th27: :: ANALMETR:27

canceled;

theorem Th28: :: ANALMETR:28

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( the carrier of (AMSpace b₁,b₂,b₃) = the carrier of b₁ & the CONGR of (AMSpace b₁,b₂,b₃) = lambda (DirPar b₁) & the orthogonality of (AMSpace b₁,b₂,b₃) = Orthogonality b₁,b₂,b₃ ) ;

definition

let c₁ be non empty ParOrtStr ;
func Af c₁ -> strict AffinStruct equals :: ANALMETR:def 8
AffinStruct(# the carrier of a₁,the CONGR of a₁ #);
correctness ;

end;

:: deftheorem Def8 defines Af ANALMETR:def 8 :

registration

let c₁ be non empty ParOrtStr ;
cluster Af a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th29: :: ANALMETR:29

canceled;

theorem Th30: :: ANALMETR:30

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds Af (AMSpace b₁,b₂,b₃) = Lambda (OASpace b₁)

proof end;

theorem Th31: :: ANALMETR:31

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁
for b₈, b₉, b₁₀, b₁₁ being Element of (AMSpace b₁,b₆,b₇) st b₈ = b₂ & b₉ = b₃ & b₁₀ = b₄ & b₁₁ = b₅ holds
( b₈,b₁₀ _|_ b₉,b₁₁ iff b₂,b₄,b₃,b₅ are_Ort_wrt b₆,b₇ )

proof end;

theorem Th32: :: ANALMETR:32

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁
for b₈, b₉, b₁₀, b₁₁ being Element of (AMSpace b₁,b₂,b₃) st b₈ = b₄ & b₉ = b₅ & b₁₀ = b₆ & b₁₁ = b₇ holds
( b₈,b₉ // b₁₀,b₁₁ iff ex b₁₂, b₁₃ being Real st
( b₁₂ * (b₅ - b₄) = b₁₃ * (b₇ - b₆) & ( b₁₂ <> 0 or b₁₃ <> 0 ) ) )

proof end;

theorem Th33: :: ANALMETR:33

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (AMSpace b₁,b₂,b₃) st b₄,b₅ _|_ b₆,b₇ holds
b₆,b₇ _|_ b₄,b₅

proof end;

theorem Th34: :: ANALMETR:34

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (AMSpace b₁,b₂,b₃) st b₄,b₅ _|_ b₆,b₇ holds
b₄,b₅ _|_ b₇,b₆

proof end;

theorem Th35: :: ANALMETR:35

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆ being Element of (AMSpace b₁,b₂,b₃) holds b₄,b₅ _|_ b₆,b₆

proof end;

theorem Th36: :: ANALMETR:36

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈, b₉ being Element of (AMSpace b₁,b₂,b₃) st b₄,b₅ _|_ b₆,b₇ & b₄,b₅ // b₈,b₉ & not b₄ = b₅ holds
b₆,b₇ _|_ b₈,b₉

proof end;

theorem Th37: :: ANALMETR:37

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆ being Element of (AMSpace b₁,b₂,b₃) ex b₇ being Element of (AMSpace b₁,b₂,b₃) st
( b₄,b₅ _|_ b₆,b₇ & b₆ <> b₇ )

proof end;

theorem Th38: :: ANALMETR:38

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈, b₉ being Element of (AMSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ _|_ b₆,b₇ & b₄,b₅ _|_ b₈,b₉ & not b₄ = b₅ holds
b₆,b₇ // b₈,b₉

proof end;

theorem Th39: :: ANALMETR:39

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈ being Element of (AMSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ _|_ b₆,b₇ & b₄,b₅ _|_ b₆,b₈ holds
b₄,b₅ _|_ b₇,b₈

proof end;

theorem Th40: :: ANALMETR:40

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅ being Element of (AMSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ _|_ b₄,b₅ holds
b₄ = b₅

proof end;

theorem Th41: :: ANALMETR:41

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (AMSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ _|_ b₆,b₇ & b₆,b₅ _|_ b₇,b₄ holds
b₇,b₅ _|_ b₄,b₆

proof end;

theorem Th42: :: ANALMETR:42

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅ being Element of (AMSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄ <> b₅ holds
for b₆ being Element of (AMSpace b₁,b₂,b₃) ex b₇ being Element of (AMSpace b₁,b₂,b₃) st
( b₄,b₅ // b₄,b₇ & b₄,b₅ _|_ b₇,b₆ )

proof end;

consider c₁ being RealLinearSpace such that
Lemma40: ex b₁, b₂ being VECTOR of c₁ st Gen b₁,b₂ by Th7;

consider c₂, c₃ being VECTOR of c₁ such that
Lemma41: Gen c₂,c₃ by Lemma40;

E42: now

set c₄ = AffinStruct(# the carrier of (AMSpace c₁,c₂,c₃),the CONGR of (AMSpace c₁,c₂,c₃) #);
AffinStruct(# the carrier of (AMSpace c₁,c₂,c₃),the CONGR of (AMSpace c₁,c₂,c₃) #) = Af (AMSpace c₁,c₂,c₃) ;
then E43: AffinStruct(# the carrier of (AMSpace c₁,c₂,c₃),the CONGR of (AMSpace c₁,c₂,c₃) #) = Lambda (OASpace c₁) by Th30;
for b₁, b₂ being Real st (b₁ * c₂) + (b₂ * c₃) = 0. c₁ holds
( b₁ = 0 & b₂ = 0 ) by Def1, Lemma41;
then OASpace c₁ is OAffinSpace by ANALOAF:38;
hence ( AffinStruct(# the carrier of (AMSpace c₁,c₂,c₃),the CONGR of (AMSpace c₁,c₂,c₃) #) is AffinSpace & ( for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of (AMSpace c₁,c₂,c₃) holds
( ( b₁,b₂ _|_ b₁,b₂ implies b₁ = b₂ ) & b₁,b₂ _|_ b₃,b₃ & ( b₁,b₂ _|_ b₃,b₄ implies ( b₁,b₂ _|_ b₄,b₃ & b₃,b₄ _|_ b₁,b₂ ) ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ // b₇,b₈ & not b₅,b₆ _|_ b₇,b₈ implies b₁ = b₂ ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ _|_ b₅,b₈ implies b₁,b₂ _|_ b₆,b₈ ) ) ) & ( for b₁, b₂, b₃ being Element of (AMSpace c₁,c₂,c₃) st b₁ <> b₂ holds
ex b₄ being Element of (AMSpace c₁,c₂,c₃) st
( b₁,b₂ // b₁,b₄ & b₁,b₂ _|_ b₄,b₃ ) ) & ( for b₁, b₂, b₃ being Element of (AMSpace c₁,c₂,c₃) ex b₄ being Element of (AMSpace c₁,c₂,c₃) st
( b₁,b₂ _|_ b₃,b₄ & b₃ <> b₄ ) ) ) by E43, Lemma41, Th33, Th34, Th35, Th36, Th37, Th39, Th40, Th42, DIRAF:48;

end;

definition

let c₄ be non empty ParOrtStr ;
attr a₁ is OrtAfSp-like means :Def9: :: ANALMETR:def 9
( AffinStruct(# the carrier of a₁,the CONGR of a₁ #) is AffinSpace & ( for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ holds
( ( b₁,b₂ _|_ b₁,b₂ implies b₁ = b₂ ) & b₁,b₂ _|_ b₃,b₃ & ( b₁,b₂ _|_ b₃,b₄ implies ( b₁,b₂ _|_ b₄,b₃ & b₃,b₄ _|_ b₁,b₂ ) ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ // b₇,b₈ & not b₅,b₆ _|_ b₇,b₈ implies b₁ = b₂ ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ _|_ b₅,b₈ implies b₁,b₂ _|_ b₆,b₈ ) ) ) & ( for b₁, b₂, b₃ being Element of a₁ st b₁ <> b₂ holds
ex b₄ being Element of a₁ st
( b₁,b₂ // b₁,b₄ & b₁,b₂ _|_ b₄,b₃ ) ) & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st
( b₁,b₂ _|_ b₃,b₄ & b₃ <> b₄ ) ) );

end;

:: deftheorem Def9 defines OrtAfSp-like ANALMETR:def 9 :

registration

cluster non empty strict OrtAfSp-like ParOrtStr ;
existence

proof end;

end;

definition

mode OrtAfSp is non empty OrtAfSp-like ParOrtStr ;

end;

theorem Th43: :: ANALMETR:43

canceled;

theorem Th44: :: ANALMETR:44

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
AMSpace b₁,b₂,b₃ is OrtAfSp

proof end;

consider c₄ being RealLinearSpace such that
Lemma44: ex b₁, b₂ being VECTOR of c₄ st Gen b₁,b₂ by Th7;

consider c₅, c₆ being VECTOR of c₄ such that
Lemma45: Gen c₅,c₆ by Lemma44;

E46: now

set c₇ = AffinStruct(# the carrier of (AMSpace c₄,c₅,c₆),the CONGR of (AMSpace c₄,c₅,c₆) #);
AffinStruct(# the carrier of (AMSpace c₄,c₅,c₆),the CONGR of (AMSpace c₄,c₅,c₆) #) = Af (AMSpace c₄,c₅,c₆) ;
then E47: AffinStruct(# the carrier of (AMSpace c₄,c₅,c₆),the CONGR of (AMSpace c₄,c₅,c₆) #) = Lambda (OASpace c₄) by Th30;
( ( for b₁, b₂ being Real st (b₁ * c₅) + (b₂ * c₆) = 0. c₄ holds
( b₁ = 0 & b₂ = 0 ) ) & ( for b₁ being VECTOR of c₄ ex b₂, b₃ being Real st b₁ = (b₂ * c₅) + (b₃ * c₆) ) ) by Def1, Lemma45;
then OASpace c₄ is OAffinPlane by ANALOAF:51;
hence ( AffinStruct(# the carrier of (AMSpace c₄,c₅,c₆),the CONGR of (AMSpace c₄,c₅,c₆) #) is AffinPlane & ( for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of (AMSpace c₄,c₅,c₆) holds
( ( b₁,b₂ _|_ b₁,b₂ implies b₁ = b₂ ) & b₁,b₂ _|_ b₃,b₃ & ( b₁,b₂ _|_ b₃,b₄ implies ( b₁,b₂ _|_ b₄,b₃ & b₃,b₄ _|_ b₁,b₂ ) ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ // b₇,b₈ & not b₅,b₆ _|_ b₇,b₈ implies b₁ = b₂ ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ _|_ b₇,b₈ & not b₅,b₆ // b₇,b₈ implies b₁ = b₂ ) ) ) & ( for b₁, b₂, b₃ being Element of (AMSpace c₄,c₅,c₆) ex b₄ being Element of (AMSpace c₄,c₅,c₆) st
( b₁,b₂ _|_ b₃,b₄ & b₃ <> b₄ ) ) ) by E47, Lemma45, Th33, Th34, Th35, Th36, Th37, Th38, Th40, DIRAF:53;

end;

definition

let c₇ be non empty ParOrtStr ;
attr a₁ is OrtAfPl-like means :Def10: :: ANALMETR:def 10
( AffinStruct(# the carrier of a₁,the CONGR of a₁ #) is AffinPlane & ( for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ holds
( ( b₁,b₂ _|_ b₁,b₂ implies b₁ = b₂ ) & b₁,b₂ _|_ b₃,b₃ & ( b₁,b₂ _|_ b₃,b₄ implies ( b₁,b₂ _|_ b₄,b₃ & b₃,b₄ _|_ b₁,b₂ ) ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ // b₇,b₈ & not b₅,b₆ _|_ b₇,b₈ implies b₁ = b₂ ) & ( b₁,b₂ _|_ b₅,b₆ & b₁,b₂ _|_ b₇,b₈ & not b₅,b₆ // b₇,b₈ implies b₁ = b₂ ) ) ) & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st
( b₁,b₂ _|_ b₃,b₄ & b₃ <> b₄ ) ) );

end;

:: deftheorem Def10 defines OrtAfPl-like ANALMETR:def 10 :

registration

cluster non empty strict OrtAfPl-like ParOrtStr ;
existence

proof end;

end;

definition

mode OrtAfPl is non empty OrtAfPl-like ParOrtStr ;

end;

theorem Th45: :: ANALMETR:45

canceled;

theorem Th46: :: ANALMETR:46

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

proof end;

theorem Th47: :: ANALMETR:47

for b₁ being non empty ParOrtStr
for b₂ being set holds
( b₂ is Element of b₁ iff b₂ is Element of (Af b₁) ) ;

theorem Th48: :: ANALMETR:48

for b₁ being non empty ParOrtStr
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇, b₈, b₉ being Element of (Af b₁) st b₂ = b₆ & b₃ = b₇ & b₄ = b₈ & b₅ = b₉ holds
( b₂,b₃ // b₄,b₅ iff b₆,b₇ // b₈,b₉ )

proof end;

Lemma49: for b₁ being OrtAfSp holds Af b₁ is AffinSpace
by Def9;

registration

let c₇ be OrtAfSp;
cluster Af a₁ -> non empty non trivial strict AffinSpace-like ;
correctness by Lemma49;

end;

Lemma50: for b₁ being OrtAfPl holds Af b₁ is AffinPlane
by Def10;

registration

let c₇ be OrtAfPl;
cluster Af a₁ -> non empty non trivial strict AffinSpace-like 2-dimensional ;
correctness by Lemma50;

end;

theorem Th49: :: ANALMETR:49

for b₁ being OrtAfPl holds b₁ is OrtAfSp

proof end;

registration

cluster non empty OrtAfPl-like -> non empty OrtAfSp-like ParOrtStr ;
coherence by Th49;

end;

theorem Th50: :: ANALMETR:50

for b₁ being OrtAfSp st Af b₁ is AffinPlane holds
b₁ is OrtAfPl

proof end;

theorem Th51: :: ANALMETR:51

for b₁ being non empty ParOrtStr holds
( b₁ is OrtAfPl-like iff ( ex b₂, b₃ being Element of b₁ st b₂ <> b₃ & ( for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ holds
( b₂,b₃ // b₃,b₂ & b₂,b₃ // b₄,b₄ & ( b₂,b₃ // b₆,b₇ & b₂,b₃ // b₈,b₉ & not b₆,b₇ // b₈,b₉ implies b₂ = b₃ ) & ( b₂,b₃ // b₂,b₄ implies b₃,b₂ // b₃,b₄ ) & ex b₁₀ being Element of b₁ st
( b₂,b₃ // b₄,b₁₀ & b₂,b₄ // b₃,b₁₀ ) & not for b₁₀, b₁₁, b₁₂ being Element of b₁ holds b₁₀,b₁₁ // b₁₀,b₁₂ & ex b₁₀ being Element of b₁ st
( b₂,b₃ // b₄,b₁₀ & b₄ <> b₁₀ ) & ( b₂,b₃ // b₃,b₅ & b₃ <> b₂ implies ex b₁₀ being Element of b₁ st
( b₄,b₃ // b₃,b₁₀ & b₄,b₂ // b₅,b₁₀ ) ) & ( b₂,b₃ _|_ b₂,b₃ implies b₂ = b₃ ) & b₂,b₃ _|_ b₄,b₄ & ( b₂,b₃ _|_ b₄,b₅ implies ( b₂,b₃ _|_ b₅,b₄ & b₄,b₅ _|_ b₂,b₃ ) ) & ( b₂,b₃ _|_ b₆,b₇ & b₂,b₃ // b₈,b₉ & not b₆,b₇ _|_ b₈,b₉ implies b₂ = b₃ ) & ( b₂,b₃ _|_ b₆,b₇ & b₂,b₃ _|_ b₈,b₉ & not b₆,b₇ // b₈,b₉ implies b₂ = b₃ ) & ex b₁₀ being Element of b₁ st
( b₂,b₃ _|_ b₄,b₁₀ & b₄ <> b₁₀ ) & ( not b₂,b₃ // b₄,b₅ implies ex b₁₀ being Element of b₁ st
( b₂,b₃ // b₂,b₁₀ & b₄,b₅ // b₄,b₁₀ ) ) ) ) ) )

proof end;

definition

let c₇ be non empty ParOrtStr ;
let c₈, c₉, c₁₀ be Element of c₇;
pred LIN c₂,c₃,c₄ means :Def11: :: ANALMETR:def 11
a₂,a₃ // a₂,a₄;

end;

:: deftheorem Def11 defines LIN ANALMETR:def 11 :

definition

let c₇ be non empty ParOrtStr ;
let c₈, c₉ be Element of c₇;
func Line c₂,c₃ -> Subset of a₁ means :Def12: :: ANALMETR:def 12
for b₁ being Element of a₁ holds
( b₁ in a₄ iff LIN a₂,a₃,b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Line ANALMETR:def 12 :

definition

let c₇ be non empty ParOrtStr ;
let c₈ be Subset of c₇;
attr a₂ is being_line means :Def13: :: ANALMETR:def 13
ex b₁, b₂ being Element of a₁ st
( b₁ <> b₂ & a₂ = Line b₁,b₂ );

end;

:: deftheorem Def13 defines being_line ANALMETR:def 13 :

notation

let c₇ be non empty ParOrtStr ;
let c₈ be Subset of c₇;
synonym c₂ is_line for being_line c₂;

end;

theorem Th52: :: ANALMETR:52

canceled;

theorem Th53: :: ANALMETR:53

canceled;

theorem Th54: :: ANALMETR:54

canceled;

theorem Th55: :: ANALMETR:55

for b₁ being OrtAfSp
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆, b₇ being Element of (Af b₁) st b₂ = b₅ & b₃ = b₆ & b₄ = b₇ holds
( LIN b₂,b₃,b₄ iff LIN b₅,b₆,b₇ )

proof end;

theorem Th56: :: ANALMETR:56

for b₁ being OrtAfSp
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (Af b₁) st b₂ = b₄ & b₃ = b₅ holds
Line b₂,b₃ = Line b₄,b₅

proof end;

theorem Th57: :: ANALMETR:57

for b₁ being non empty ParOrtStr
for b₂ being set holds
( b₂ is Subset of b₁ iff b₂ is Subset of (Af b₁) ) ;

theorem Th58: :: ANALMETR:58

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃ being Subset of (Af b₁) st b₂ = b₃ holds
( b₂ is_line iff b₃ is_line )

proof end;

definition

let c₇ be non empty ParOrtStr ;
let c₈, c₉ be Element of c₇;
let c₁₀ be Subset of c₇;
pred c₂,c₃ _|_ c₄ means :Def14: :: ANALMETR:def 14
ex b₁, b₂ being Element of a₁ st
( b₁ <> b₂ & a₄ = Line b₁,b₂ & a₂,a₃ _|_ b₁,b₂ );

end;

:: deftheorem Def14 defines _|_ ANALMETR:def 14 :

definition

let c₇ be non empty ParOrtStr ;
let c₈, c₉ be Subset of c₇;
pred c₂ _|_ c₃ means :Def15: :: ANALMETR:def 15
ex b₁, b₂ being Element of a₁ st
( b₁ <> b₂ & a₂ = Line b₁,b₂ & b₁,b₂ _|_ a₃ );

end;

:: deftheorem Def15 defines _|_ ANALMETR:def 15 :

definition

let c₇ be non empty ParOrtStr ;
let c₈, c₉ be Subset of c₇;
pred c₂ // c₃ means :Def16: :: ANALMETR:def 16
ex b₁, b₂, b₃, b₄ being Element of a₁ st
( b₁ <> b₂ & b₃ <> b₄ & a₂ = Line b₁,b₂ & a₃ = Line b₃,b₄ & b₁,b₂ // b₃,b₄ );

end;

:: deftheorem Def16 defines // ANALMETR:def 16 :

theorem Th59: :: ANALMETR:59

canceled;

theorem Th60: :: ANALMETR:60

canceled;

theorem Th61: :: ANALMETR:61

canceled;

theorem Th62: :: ANALMETR:62

for b₁ being non empty ParOrtStr
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ holds
( ( b₂,b₃ _|_ b₄ implies b₄ is_line ) & ( b₄ _|_ b₅ implies ( b₄ is_line & b₅ is_line ) ) )

proof end;

theorem Th63: :: ANALMETR:63

for b₁ being non empty ParOrtStr
for b₂, b₃ being Subset of b₁ holds
( b₂ _|_ b₃ iff ex b₄, b₅, b₆, b₇ being Element of b₁ st
( b₄ <> b₅ & b₆ <> b₇ & b₂ = Line b₄,b₅ & b₃ = Line b₆,b₇ & b₄,b₅ _|_ b₆,b₇ ) )

proof end;

theorem Th64: :: ANALMETR:64

for b₁ being OrtAfSp
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Subset of (Af b₁) st b₂ = b₄ & b₃ = b₅ holds
( b₂ // b₃ iff b₄ // b₅ )

proof end;

theorem Th65: :: ANALMETR:65

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₂ is_line holds
b₃,b₃ _|_ b₂

proof end;

theorem Th66: :: ANALMETR:66

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

proof end;

theorem Th67: :: ANALMETR:67

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₃,b₄ _|_ b₂ holds
b₄,b₃ _|_ b₂

proof end;

theorem Th68: :: ANALMETR:68

for b₁ being OrtAfSp
for b₂, b₃ being Subset of b₁ st b₂ // b₃ holds
b₃ // b₂

proof end;

theorem Th69: :: ANALMETR:69

for b₁ being OrtAfSp
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Element of b₁ st b₄,b₅ _|_ b₂ & ( b₂ // b₃ or b₃ // b₂ ) holds
b₄,b₅ _|_ b₃

proof end;

theorem Th70: :: ANALMETR:70

for b₁ being OrtAfSp
for b₂, b₃ being Subset of b₁ st b₂ _|_ b₃ holds
b₃ _|_ b₂

proof end;

definition

let c₇ be OrtAfSp;
let c₈, c₉ be Subset of c₇;
redefine pred // as c₂ // c₃;
symmetry by Th68;
redefine pred _|_ as c₂ _|_ c₃;
symmetry by Th70;

end;

theorem Th71: :: ANALMETR:71

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & b₃,b₄ _|_ b₂ holds
b₃ = b₄

proof end;

theorem Th72: :: ANALMETR:72

for b₁ being OrtAfSp
for b₂ being Subset of b₁ holds not b₂ _|_ b₂

proof end;

theorem Th73: :: ANALMETR:73

for b₁ being OrtAfSp
for b₂, b₃, b₄ being Subset of b₁ st ( b₂ _|_ b₃ or b₃ _|_ b₂ ) & ( b₂ // b₄ or b₄ // b₂ ) holds
( b₃ _|_ b₄ & b₄ _|_ b₃ )

proof end;

theorem Th74: :: ANALMETR:74

for b₁ being OrtAfSp
for b₂, b₃ being Subset of b₁ st b₂ // b₃ holds
not b₂ _|_ b₃

proof end;

theorem Th75: :: ANALMETR:75

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & b₅,b₆ _|_ b₂ holds
( b₅,b₆ _|_ b₃,b₄ & b₃,b₄ _|_ b₅,b₆ )

proof end;

theorem Th76: :: ANALMETR:76

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ & b₂ is_line holds
b₂ = Line b₃,b₄

proof end;

theorem Th77: :: ANALMETR:77

for b₁ being OrtAfSp
for b₂ being Subset of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ & b₂ is_line & ( b₃,b₄ _|_ b₅,b₆ or b₅,b₆ _|_ b₃,b₄ ) holds
b₅,b₆ _|_ b₂

proof end;

theorem Th78: :: ANALMETR:78

for b₁ being OrtAfSp
for b₂, b₃ being Subset of b₁
for b₄, b₅, b₆, b₇ being Element of b₁ st b₄ in b₂ & b₅ in b₂ & b₆ in b₃ & b₇ in b₃ & b₂ _|_ b₃ holds
b₄,b₅ _|_ b₆,b₇

proof end;

theorem Th79: :: ANALMETR:79

for b₁ being OrtAfSp
for b₂, b₃, b₄, b₅ being Subset of b₁
for b₆, b₇, b₈ being Element of b₁ st b₆ in b₂ & b₆ in b₃ & b₇ in b₂ & b₈ in b₃ & b₇ <> b₈ & b₇ in b₄ & b₈ in b₄ & b₅ _|_ b₂ & b₅ _|_ b₃ & b₄ is_line holds
b₅ _|_ b₄

proof end;

theorem Th80: :: ANALMETR:80

for b₁ being OrtAfSp
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₃ _|_ b₄,b₄ & b₄,b₄ _|_ b₂,b₃ & b₂,b₃ // b₄,b₄ & b₄,b₄ // b₂,b₃ )

proof end;

theorem Th81: :: ANALMETR:81

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

proof end;

theorem Th82: :: ANALMETR:82

for b₁ being OrtAfSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & ( ( b₂,b₃ // b₄,b₅ & b₂,b₃ // b₆,b₇ ) or ( b₂,b₃ // b₄,b₅ & b₆,b₇ // b₂,b₃ ) or ( b₄,b₅ // b₂,b₃ & b₆,b₇ // b₂,b₃ ) or ( b₄,b₅ // b₂,b₃ & b₂,b₃ // b₆,b₇ ) ) holds
b₄,b₅ // b₆,b₇

proof end;

theorem Th83: :: ANALMETR:83

proof end;

theorem Th84: :: ANALMETR:84

for b₁ being OrtAfSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & ( ( b₂,b₃ // b₄,b₅ & b₂,b₃ _|_ b₆,b₇ ) or ( b₂,b₃ // b₆,b₇ & b₂,b₃ _|_ b₄,b₅ ) or ( b₂,b₃ // b₄,b₅ & b₆,b₇ _|_ b₂,b₃ ) or ( b₂,b₃ // b₆,b₇ & b₄,b₅ _|_ b₂,b₃ ) or ( b₄,b₅ // b₂,b₃ & b₆,b₇ _|_ b₂,b₃ ) or ( b₆,b₇ // b₂,b₃ & b₄,b₅ _|_ b₂,b₃ ) or ( b₄,b₅ // b₂,b₃ & b₂,b₃ _|_ b₆,b₇ ) or ( b₆,b₇ // b₂,b₃ & b₂,b₃ _|_ b₄,b₅ ) ) holds
b₄,b₅ _|_ b₆,b₇

proof end;

theorem Th85: :: ANALMETR:85

proof end;

theorem Th86: :: ANALMETR:86

for b₁ being OrtAfPl
for b₂, b₃ being Subset of b₁
for b₄, b₅, b₆, b₇ being Element of b₁ st b₄ in b₂ & b₅ in b₂ & b₄ <> b₅ & b₂ is_line & b₆ in b₃ & b₇ in b₃ & b₆ <> b₇ & b₃ is_line & b₄,b₅ // b₆,b₇ holds
b₂ // b₃

proof end;

theorem Th87: :: ANALMETR:87

for b₁ being OrtAfPl
for b₂, b₃, b₄ being Subset of b₁ st ( b₂ _|_ b₃ or b₃ _|_ b₂ ) & ( b₂ _|_ b₄ or b₄ _|_ b₂ ) holds
( b₃ // b₄ & b₄ // b₃ )

proof end;

theorem Th88: :: ANALMETR:88

for b₁ being OrtAfPl
for b₂, b₃ being Subset of b₁ st b₂ _|_ b₃ holds
ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ in b₃ )

proof end;

theorem Th89: :: ANALMETR:89

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

proof end;

theorem Th90: :: ANALMETR:90

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

proof end;

theorem Th91: :: ANALMETR:91

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

proof end;

theorem Th92: :: ANALMETR:92

for b₁ being OrtAfPl
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₂ is_line holds
ex b₄ being Element of b₁ st
( b₃,b₄ _|_ b₂ & b₄ in b₂ )

proof end;