:: ANALORT semantic presentation

definition

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be Element of c₁;
redefine func + as c₂ + c₃ -> M3(the carrier of a₁);
commutativity by RLVECT_1:def 5;

end;

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₃, 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;

Lemma3: 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;

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

proof end;

Lemma5: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
b₄ = ((pr1 b₂,b₃,b₄) * b₂) + ((pr2 b₂,b₃,b₄) * b₃)

proof end;

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

proof end;

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

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄ be VECTOR of c₁;
func Ortm c₂,c₃,c₄ -> VECTOR of a₁ equals :: ANALORT:def 1
((pr1 a₂,a₃,a₄) * a₂) + ((- (pr2 a₂,a₃,a₄)) * a₃);
correctness ;

end;

:: deftheorem Def1 defines Ortm ANALORT:def 1 :

theorem Th1: :: ANALORT:1

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
Ortm b₂,b₃,(b₄ + b₅) = (Ortm b₂,b₃,b₄) + (Ortm b₂,b₃,b₅)

proof end;

theorem Th2: :: ANALORT:2

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Real st Gen b₂,b₃ holds
Ortm b₂,b₃,(b₅ * b₄) = b₅ * (Ortm b₂,b₃,b₄)

proof end;

theorem Th3: :: ANALORT:3

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
Ortm b₂,b₃,(0. b₁) = 0. b₁

proof end;

theorem Th4: :: ANALORT:4

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
Ortm b₂,b₃,(- b₄) = - (Ortm b₂,b₃,b₄)

proof end;

theorem Th5: :: ANALORT:5

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
Ortm b₂,b₃,(b₄ - b₅) = (Ortm b₂,b₃,b₄) - (Ortm b₂,b₃,b₅)

proof end;

theorem Th6: :: ANALORT:6

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ & Ortm b₂,b₃,b₄ = Ortm b₂,b₃,b₅ holds
b₄ = b₅

proof end;

theorem Th7: :: ANALORT:7

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
Ortm b₂,b₃,(Ortm b₂,b₃,b₄) = b₄

proof end;

theorem Th8: :: ANALORT:8

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
ex b₅ being VECTOR of b₁ st b₄ = Ortm b₂,b₃,b₅

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄ be VECTOR of c₁;
func Orte c₂,c₃,c₄ -> VECTOR of a₁ equals :: ANALORT:def 2
((pr2 a₂,a₃,a₄) * a₂) + ((- (pr1 a₂,a₃,a₄)) * a₃);
correctness ;

end;

:: deftheorem Def2 defines Orte ANALORT:def 2 :

theorem Th9: :: ANALORT:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
Orte b₂,b₃,(- b₄) = - (Orte b₂,b₃,b₄)

proof end;

theorem Th10: :: ANALORT:10

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
Orte b₂,b₃,(b₄ + b₅) = (Orte b₂,b₃,b₄) + (Orte b₂,b₃,b₅)

proof end;

theorem Th11: :: ANALORT:11

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
Orte b₂,b₃,(b₄ - b₅) = (Orte b₂,b₃,b₄) - (Orte b₂,b₃,b₅)

proof end;

theorem Th12: :: ANALORT:12

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Real st Gen b₂,b₃ holds
Orte b₂,b₃,(b₅ * b₄) = b₅ * (Orte b₂,b₃,b₄)

proof end;

theorem Th13: :: ANALORT:13

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ & Orte b₂,b₃,b₄ = Orte b₂,b₃,b₅ holds
b₄ = b₅

proof end;

theorem Th14: :: ANALORT:14

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
Orte b₂,b₃,(Orte b₂,b₃,b₄) = - b₄

proof end;

theorem Th15: :: ANALORT:15

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
ex b₅ being VECTOR of b₁ st Orte b₂,b₃,b₅ = b₄

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇ be VECTOR of c₁;
pred c₄,c₅,c₆,c₇ are_COrte_wrt c₂,c₃ means :Def3: :: ANALORT:def 3
Orte a₂,a₃,a₄, Orte a₂,a₃,a₅ // a₆,a₇;
pred c₄,c₅,c₆,c₇ are_COrtm_wrt c₂,c₃ means :Def4: :: ANALORT:def 4
Ortm a₂,a₃,a₄, Ortm a₂,a₃,a₅ // a₆,a₇;

end;

:: deftheorem Def3 defines are_COrte_wrt ANALORT:def 3 :

:: deftheorem Def4 defines are_COrtm_wrt ANALORT:def 4 :

theorem Th16: :: ANALORT:16

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ holds
Orte b₂,b₃,b₄, Orte b₂,b₃,b₅ // Orte b₂,b₃,b₆, Orte b₂,b₃,b₇

proof end;

theorem Th17: :: ANALORT:17

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ holds
Ortm b₂,b₃,b₄, Ortm b₂,b₃,b₅ // Ortm b₂,b₃,b₆, Ortm b₂,b₃,b₇

proof end;

theorem Th18: :: ANALORT:18

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

proof end;

theorem Th19: :: ANALORT:19

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

proof end;

theorem Th20: :: ANALORT:20

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ holds b₂,b₂,b₃,b₄ are_COrte_wrt b₅,b₆

proof end;

theorem Th21: :: ANALORT:21

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ holds b₂,b₂,b₃,b₄ are_COrtm_wrt b₅,b₆

proof end;

theorem Th22: :: ANALORT:22

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ holds b₂,b₃,b₄,b₄ are_COrte_wrt b₅,b₆

proof end;

theorem Th23: :: ANALORT:23

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ holds b₂,b₃,b₄,b₄ are_COrtm_wrt b₅,b₆

proof end;

theorem Th24: :: ANALORT:24

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

proof end;

theorem Th25: :: ANALORT:25

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds b₂,b₃, Orte b₄,b₅,b₂, Orte b₄,b₅,b₃ are_COrte_wrt b₄,b₅

proof end;

theorem Th26: :: ANALORT:26

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds b₂,b₃, Ortm b₄,b₅,b₂, Ortm b₄,b₅,b₃ are_COrtm_wrt b₄,b₅

proof end;

theorem Th27: :: ANALORT:27

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ holds
( b₄,b₅ // b₆,b₇ iff ex b₈, b₉ being VECTOR of b₁ st
( b₈ <> b₉ & b₈,b₉,b₄,b₅ are_COrte_wrt b₂,b₃ & b₈,b₉,b₆,b₇ are_COrte_wrt b₂,b₃ ) )

proof end;

theorem Th28: :: ANALORT:28

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ holds
( b₄,b₅ // b₆,b₇ iff ex b₈, b₉ being VECTOR of b₁ st
( b₈ <> b₉ & b₈,b₉,b₄,b₅ are_COrtm_wrt b₂,b₃ & b₈,b₉,b₆,b₇ are_COrtm_wrt b₂,b₃ ) )

proof end;

theorem Th29: :: ANALORT:29

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ holds
( b₄,b₅,b₆,b₇ are_Ort_wrt b₂,b₃ iff ( b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ or b₄,b₅,b₇,b₆ are_COrte_wrt b₂,b₃ ) )

proof end;

theorem Th30: :: ANALORT:30

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ & b₄,b₅,b₇,b₆ are_COrte_wrt b₂,b₃ & not b₄ = b₅ holds
b₆ = b₇

proof end;

theorem Th31: :: ANALORT:31

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₄,b₅,b₇,b₆ are_COrtm_wrt b₂,b₃ & not b₄ = b₅ holds
b₆ = b₇

proof end;

theorem Th32: :: ANALORT:32

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ & b₄,b₅,b₆,b₈ are_COrte_wrt b₂,b₃ & not b₄,b₅,b₇,b₈ are_COrte_wrt b₂,b₃ holds
b₄,b₅,b₈,b₇ are_COrte_wrt b₂,b₃

proof end;

theorem Th33: :: ANALORT:33

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₄,b₅,b₆,b₈ are_COrtm_wrt b₂,b₃ & not b₄,b₅,b₇,b₈ are_COrtm_wrt b₂,b₃ holds
b₄,b₅,b₈,b₇ are_COrtm_wrt b₂,b₃

proof end;

theorem Th34: :: ANALORT:34

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

proof end;

theorem Th35: :: ANALORT:35

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

proof end;

theorem Th36: :: ANALORT:36

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ & b₄,b₅,b₇,b₈ are_COrte_wrt b₂,b₃ holds
b₄,b₅,b₆,b₈ are_COrte_wrt b₂,b₃

proof end;

theorem Th37: :: ANALORT:37

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₄,b₅,b₇,b₈ are_COrtm_wrt b₂,b₃ holds
b₄,b₅,b₆,b₈ are_COrtm_wrt b₂,b₃

proof end;

theorem Th38: :: ANALORT:38

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

proof end;

theorem Th39: :: ANALORT:39

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

proof end;

theorem Th40: :: ANALORT:40

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

proof end;

theorem Th41: :: ANALORT:41

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

proof end;

theorem Th42: :: ANALORT:42

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ & b₈,b₉,b₆,b₇ are_COrte_wrt b₂,b₃ & b₈,b₉,b₁₀,b₁₁ are_COrte_wrt b₂,b₃ & not b₈ = b₉ & not b₆ = b₇ holds
b₄,b₅,b₁₀,b₁₁ are_COrte_wrt b₂,b₃

proof end;

theorem Th43: :: ANALORT:43

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₈,b₉,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₈,b₉,b₁₀,b₁₁ are_COrtm_wrt b₂,b₃ & not b₈ = b₉ & not b₆ = b₇ holds
b₄,b₅,b₁₀,b₁₁ are_COrtm_wrt b₂,b₃

proof end;

theorem Th44: :: ANALORT:44

canceled;

theorem Th45: :: ANALORT:45

canceled;

theorem Th46: :: ANALORT:46

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ & b₆,b₇,b₈,b₉ are_COrte_wrt b₂,b₃ & b₁₀,b₁₁,b₈,b₉ are_COrte_wrt b₂,b₃ & not b₄,b₅,b₁₀,b₁₁ are_COrte_wrt b₂,b₃ & not b₆ = b₇ holds
b₈ = b₉

proof end;

theorem Th47: :: ANALORT:47

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₆,b₇,b₈,b₉ are_COrtm_wrt b₂,b₃ & b₁₀,b₁₁,b₈,b₉ are_COrtm_wrt b₂,b₃ & not b₄,b₅,b₁₀,b₁₁ are_COrtm_wrt b₂,b₃ & not b₆ = b₇ holds
b₈ = b₉

proof end;

theorem Th48: :: ANALORT:48

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrte_wrt b₂,b₃ & b₆,b₇,b₈,b₉ are_COrte_wrt b₂,b₃ & b₄,b₅,b₁₀,b₁₁ are_COrte_wrt b₂,b₃ & not b₁₀,b₁₁,b₈,b₉ are_COrte_wrt b₂,b₃ & not b₆ = b₇ holds
b₄ = b₅

proof end;

theorem Th49: :: ANALORT:49

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_COrtm_wrt b₂,b₃ & b₆,b₇,b₈,b₉ are_COrtm_wrt b₂,b₃ & b₄,b₅,b₁₀,b₁₁ are_COrtm_wrt b₂,b₃ & not b₁₀,b₁₁,b₈,b₉ are_COrtm_wrt b₂,b₃ & not b₆ = b₇ holds
b₄ = b₅

proof end;

theorem Th50: :: ANALORT:50

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st not b₄,b₇,b₅,b₆ are_COrte_wrt b₂,b₃ & not b₄,b₇,b₆,b₅ are_COrte_wrt b₂,b₃ & b₆,b₈,b₆,b₅ are_COrte_wrt b₂,b₃ holds
ex b₉ being VECTOR of b₁ st
( ( b₄,b₇,b₄,b₉ are_COrte_wrt b₂,b₃ or b₄,b₇,b₉,b₄ are_COrte_wrt b₂,b₃ ) & ( b₆,b₈,b₆,b₉ are_COrte_wrt b₂,b₃ or b₆,b₈,b₉,b₆ are_COrte_wrt b₂,b₃ ) )

proof end;

theorem Th51: :: ANALORT:51

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
ex b₄, b₅, b₆ being VECTOR of b₁ st
( b₄,b₅,b₄,b₆ are_COrte_wrt b₂,b₃ & ( for b₇, b₈ being VECTOR of b₁ holds
( not b₇,b₈,b₄,b₅ are_COrte_wrt b₂,b₃ or ( not b₇,b₈,b₄,b₆ are_COrte_wrt b₂,b₃ & not b₇,b₈,b₆,b₄ are_COrte_wrt b₂,b₃ ) or b₇ = b₈ ) ) )

proof end;

theorem Th52: :: ANALORT:52

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st not b₄,b₇,b₅,b₆ are_COrtm_wrt b₂,b₃ & not b₄,b₇,b₆,b₅ are_COrtm_wrt b₂,b₃ & b₆,b₈,b₆,b₅ are_COrtm_wrt b₂,b₃ holds
ex b₉ being VECTOR of b₁ st
( ( b₄,b₇,b₄,b₉ are_COrtm_wrt b₂,b₃ or b₄,b₇,b₉,b₄ are_COrtm_wrt b₂,b₃ ) & ( b₆,b₈,b₆,b₉ are_COrtm_wrt b₂,b₃ or b₆,b₈,b₉,b₆ are_COrtm_wrt b₂,b₃ ) )

proof end;

theorem Th53: :: ANALORT:53

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
ex b₄, b₅, b₆ being VECTOR of b₁ st
( b₄,b₅,b₄,b₆ are_COrtm_wrt b₂,b₃ & ( for b₇, b₈ being VECTOR of b₁ holds
( not b₇,b₈,b₄,b₅ are_COrtm_wrt b₂,b₃ or ( not b₇,b₈,b₄,b₆ are_COrtm_wrt b₂,b₃ & not b₇,b₈,b₆,b₄ are_COrtm_wrt b₂,b₃ ) or b₇ = b₈ ) ) )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func CORTE c₁,c₂,c₃ -> Relation of [:the carrier of a₁,the carrier of a₁:] means :Def5: :: ANALORT:def 5
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_COrte_wrt a₂,a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines CORTE ANALORT:def 5 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func CORTM c₁,c₂,c₃ -> Relation of [:the carrier of a₁,the carrier of a₁:] means :Def6: :: ANALORT:def 6
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_COrtm_wrt a₂,a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines CORTM ANALORT:def 6 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func CESpace c₁,c₂,c₃ -> strict AffinStruct equals :: ANALORT:def 7
AffinStruct(# the carrier of a₁,(CORTE a₁,a₂,a₃) #);
correctness ;

end;

:: deftheorem Def7 defines CESpace ANALORT:def 7 :

registration

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

proof end;

end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func CMSpace c₁,c₂,c₃ -> strict AffinStruct equals :: ANALORT:def 8
AffinStruct(# the carrier of a₁,(CORTM a₁,a₂,a₃) #);
correctness ;

end;

:: deftheorem Def8 defines CMSpace ANALORT:def 8 :

registration

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

proof end;

end;

theorem Th54: :: ANALORT:54

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being set holds
( b₄ is Element of (CESpace b₁,b₂,b₃) iff b₄ is VECTOR of b₁ ) ;

theorem Th55: :: ANALORT:55

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being set holds
( b₄ is Element of (CMSpace b₁,b₂,b₃) iff b₄ is VECTOR of b₁ ) ;

theorem Th56: :: ANALORT:56

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁
for b₈, b₉, b₁₀, b₁₁ being Element of (CESpace b₁,b₆,b₇) st b₂ = b₈ & b₃ = b₉ & b₄ = b₁₀ & b₅ = b₁₁ holds
( b₈,b₉ // b₁₀,b₁₁ iff b₂,b₃,b₄,b₅ are_COrte_wrt b₆,b₇ )

proof end;

theorem Th57: :: ANALORT:57

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁
for b₈, b₉, b₁₀, b₁₁ being Element of (CMSpace b₁,b₆,b₇) st b₂ = b₈ & b₃ = b₉ & b₄ = b₁₀ & b₅ = b₁₁ holds
( b₈,b₉ // b₁₀,b₁₁ iff b₂,b₃,b₄,b₅ are_COrtm_wrt b₆,b₇ )

proof end;