:: ANALOAF semantic presentation

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅ be VECTOR of c₁;
pred c₂,c₃ // c₄,c₅ means :Def1: :: ANALOAF:def 1
( a₂ = a₃ or a₄ = a₅ or ex b₁, b₂ being Real st
( 0 < b₁ & 0 < b₂ & b₁ * (a₃ - a₂) = b₂ * (a₅ - a₄) ) );

end;

:: deftheorem Def1 defines // ANALOAF:def 1 :

Lemma2: for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
0 < b₁ + b₂
by XREAL_1:36;

Lemma3: for b₁, b₂ being Real holds
( not b₁ <> b₂ or 0 < b₁ - b₂ or 0 < b₂ - b₁ )
by XREAL_1:57;

theorem Th1: :: ANALOAF:1

canceled;

theorem Th2: :: ANALOAF:2

canceled;

theorem Th3: :: ANALOAF:3

canceled;

theorem Th4: :: ANALOAF:4

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

proof end;

theorem Th5: :: ANALOAF:5

canceled;

theorem Th6: :: ANALOAF:6

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds b₂ - (b₃ - b₄) = b₂ + (b₄ - b₃) by VECTSP_1:81;

theorem Th7: :: ANALOAF:7

canceled;

theorem Th8: :: ANALOAF:8

canceled;

theorem Th9: :: ANALOAF:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂ + b₃ = b₄ + b₅ holds
b₂ - b₅ = b₄ - b₃

proof end;

theorem Th10: :: ANALOAF:10

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Real holds b₄ * (b₂ - b₃) = - (b₄ * (b₃ - b₂))

proof end;

theorem Th11: :: ANALOAF:11

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

proof end;

theorem Th12: :: ANALOAF:12

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Real st b₄ <> 0 & b₄ * b₂ = b₃ holds
b₂ = (b₄ " ) * b₃

proof end;

theorem Th13: :: ANALOAF:13

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Real holds
( ( b₄ <> 0 & b₄ * b₂ = b₃ implies b₂ = (b₄ " ) * b₃ ) & ( b₄ <> 0 & b₂ = (b₄ " ) * b₃ implies b₄ * b₂ = b₃ ) )

proof end;

theorem Th14: :: ANALOAF:14

canceled;

theorem Th15: :: ANALOAF:15

canceled;

theorem Th16: :: ANALOAF:16

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

proof end;

theorem Th17: :: ANALOAF:17

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

proof end;

theorem Th18: :: ANALOAF:18

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds
( b₂,b₃ // b₄,b₄ & b₂,b₂ // b₃,b₄ ) by Def1;

theorem Th19: :: ANALOAF:19

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st b₂,b₃ // b₃,b₂ holds
b₂ = b₃

proof end;

theorem Th20: :: ANALOAF:20

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

proof end;

theorem Th21: :: ANALOAF:21

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

proof end;

theorem Th22: :: ANALOAF:22

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

proof end;

theorem Th23: :: ANALOAF:23

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds
( not b₂,b₃ // b₂,b₄ or b₂,b₃ // b₃,b₄ or b₂,b₄ // b₄,b₃ )

proof end;

theorem Th24: :: ANALOAF:24

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂ - b₃ = b₄ - b₅ holds
b₃,b₂ // b₅,b₄

proof end;

theorem Th25: :: ANALOAF:25

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂ = (b₃ + b₄) - b₅ holds
( b₅,b₃ // b₄,b₂ & b₅,b₄ // b₃,b₂ )

proof end;

theorem Th26: :: ANALOAF:26

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

proof end;

theorem Th27: :: ANALOAF:27

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

proof end;

theorem Th28: :: ANALOAF:28

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st ( for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) ) holds
( b₂ <> b₃ & b₂ <> 0. b₁ & b₃ <> 0. b₁ )

proof end;

theorem Th29: :: ANALOAF:29

for b₁ being RealLinearSpace st ex b₂, b₃ being VECTOR of b₁ st
for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) holds
ex b₂, b₃, b₄, b₅ being VECTOR of b₁ st
( not b₂,b₃ // b₄,b₅ & not b₂,b₃ // b₅,b₄ )

proof end;

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

proof end;

theorem Th30: :: ANALOAF:30

canceled;

theorem Th31: :: ANALOAF:31

for b₁ being RealLinearSpace st ex b₂, b₃ being VECTOR of b₁ st
for b₄ being VECTOR of b₁ ex b₅, b₆ being Real st (b₅ * b₂) + (b₆ * b₃) = b₄ holds
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st not b₂,b₃ // b₄,b₅ & not b₂,b₃ // b₅,b₄ holds
ex b₆ being VECTOR of b₁ st
( ( b₂,b₃ // b₂,b₆ or b₂,b₃ // b₆,b₂ ) & ( b₄,b₅ // b₄,b₆ or b₄,b₅ // b₆,b₄ ) )

proof end;

definition

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

end;

registration

cluster non empty strict AffinStruct ;
existence

proof end;

end;

definition

let c₁ be non empty AffinStruct ;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃ // c₄,c₅ means :Def2: :: ANALOAF:def 2
[[a₂,a₃],[a₄,a₅]] in the CONGR of a₁;

end;

:: deftheorem Def2 defines // ANALOAF:def 2 :

definition

let c₁ be RealLinearSpace;
func DirPar c₁ -> Relation of [:the carrier of a₁,the carrier of a₁:] means :Def3: :: ANALOAF:def 3
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₆ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines DirPar ANALOAF:def 3 :

theorem Th32: :: ANALOAF:32

canceled;

theorem Th33: :: ANALOAF:33

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds
( [[b₂,b₃],[b₄,b₅]] in DirPar b₁ iff b₂,b₃ // b₄,b₅ )

proof end;

definition

let c₁ be RealLinearSpace;
func OASpace c₁ -> strict AffinStruct equals :: ANALOAF:def 4
AffinStruct(# the carrier of a₁,(DirPar a₁) #);
correctness ;

end;

:: deftheorem Def4 defines OASpace ANALOAF:def 4 :

registration

let c₁ be RealLinearSpace;
cluster OASpace a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th34: :: ANALOAF:34

canceled;

theorem Th35: :: ANALOAF:35

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

proof end;

theorem Th36: :: ANALOAF:36

for b₁ being RealLinearSpace st ex b₂, b₃ being VECTOR of b₁ st
for b₄ being VECTOR of b₁ ex b₅, b₆ being Real st (b₅ * b₂) + (b₆ * b₃) = b₄ holds
for b₂, b₃, b₄, b₅ being Element of (OASpace b₁) st not b₂,b₃ // b₄,b₅ & not b₂,b₃ // b₅,b₄ holds
ex b₆ being Element of (OASpace b₁) st
( ( b₂,b₃ // b₂,b₆ or b₂,b₃ // b₆,b₂ ) & ( b₄,b₅ // b₄,b₆ or b₄,b₅ // b₆,b₄ ) )

proof end;

definition

let c₁ be non empty AffinStruct ;
attr a₁ is OAffinSpace-like means :Def5: :: ANALOAF:def 5
( ( for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ holds
( b₁,b₂ // b₃,b₃ & ( b₁,b₂ // b₂,b₁ implies b₁ = b₂ ) & ( b₁ <> b₂ & b₁,b₂ // b₅,b₆ & b₁,b₂ // b₇,b₈ implies b₅,b₆ // b₇,b₈ ) & ( b₁,b₂ // b₃,b₄ implies b₂,b₁ // b₄,b₃ ) & ( b₁,b₂ // b₂,b₃ implies b₁,b₂ // b₁,b₃ ) & ( not b₁,b₂ // b₁,b₃ or b₁,b₂ // b₂,b₃ or b₁,b₃ // b₃,b₂ ) ) ) & ex b₁, b₂, b₃, b₄ being Element of a₁ st
( not b₁,b₂ // b₃,b₄ & not 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₃ // b₂,b₄ & b₂ <> b₄ ) ) & ( for b₁, b₂, b₃, b₄ being Element of a₁ st b₁ <> b₃ & b₃,b₁ // b₁,b₄ holds
ex b₅ being Element of a₁ st
( b₂,b₁ // b₁,b₅ & b₂,b₃ // b₄,b₅ ) ) );

end;

:: deftheorem Def5 defines OAffinSpace-like ANALOAF:def 5 :

registration

cluster non empty non trivial strict OAffinSpace-like AffinStruct ;
existence

proof end;

end;

definition

mode OAffinSpace is non empty non trivial OAffinSpace-like AffinStruct ;

end;

theorem Th37: :: ANALOAF:37

for b₁ being non empty AffinStruct holds
( ( 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₂ implies b₂ = b₃ ) & ( b₂ <> b₃ & b₂,b₃ // b₆,b₇ & b₂,b₃ // b₈,b₉ implies b₆,b₇ // b₈,b₉ ) & ( b₂,b₃ // b₄,b₅ implies b₃,b₂ // b₅,b₄ ) & ( b₂,b₃ // b₃,b₄ implies b₂,b₃ // b₂,b₄ ) & ( not b₂,b₃ // b₂,b₄ or b₂,b₃ // b₃,b₄ or b₂,b₄ // b₄,b₃ ) ) ) & ex b₂, b₃, b₄, b₅ being Element of b₁ st
( not b₂,b₃ // b₄,b₅ & not b₂,b₃ // b₅,b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ & b₃ <> b₅ ) ) & ( for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₄ & b₄,b₂ // b₂,b₅ holds
ex b₆ being Element of b₁ st
( b₃,b₂ // b₂,b₆ & b₃,b₄ // b₅,b₆ ) ) ) iff b₁ is OAffinSpace ) by Def5, REALSET2:def 7;

theorem Th38: :: ANALOAF:38

for b₁ being RealLinearSpace st ex b₂, b₃ being VECTOR of b₁ st
for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) holds
OASpace b₁ is OAffinSpace

proof end;

definition

let c₁ be OAffinSpace;
attr a₁ is 2-dimensional means :Def6: :: ANALOAF:def 6
for b₁, b₂, b₃, b₄ being Element of a₁ st not b₁,b₂ // b₃,b₄ & not b₁,b₂ // b₄,b₃ holds
ex b₅ being Element of a₁ st
( ( b₁,b₂ // b₁,b₅ or b₁,b₂ // b₅,b₁ ) & ( b₃,b₄ // b₃,b₅ or b₃,b₄ // b₅,b₃ ) );

end;

:: deftheorem Def6 defines 2-dimensional ANALOAF:def 6 :

registration

cluster strict 2-dimensional AffinStruct ;
existence

proof end;

end;

definition

mode OAffinPlane is 2-dimensional OAffinSpace;

end;

theorem Th39: :: ANALOAF:39

canceled;

theorem Th40: :: ANALOAF:40

canceled;

theorem Th41: :: ANALOAF:41

canceled;

theorem Th42: :: ANALOAF:42

canceled;

theorem Th43: :: ANALOAF:43

canceled;

theorem Th44: :: ANALOAF:44

canceled;

theorem Th45: :: ANALOAF:45

canceled;

theorem Th46: :: ANALOAF:46

canceled;

theorem Th47: :: ANALOAF:47

canceled;

theorem Th48: :: ANALOAF:48

canceled;

theorem Th49: :: ANALOAF:49

canceled;

theorem Th50: :: ANALOAF:50

for b₁ being non empty AffinStruct holds
( ( 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₂ implies b₂ = b₃ ) & ( b₂ <> b₃ & b₂,b₃ // b₆,b₇ & b₂,b₃ // b₈,b₉ implies b₆,b₇ // b₈,b₉ ) & ( b₂,b₃ // b₄,b₅ implies b₃,b₂ // b₅,b₄ ) & ( b₂,b₃ // b₃,b₄ implies b₂,b₃ // b₂,b₄ ) & ( not b₂,b₃ // b₂,b₄ or b₂,b₃ // b₃,b₄ or b₂,b₄ // b₄,b₃ ) ) ) & ex b₂, b₃, b₄, b₅ being Element of b₁ st
( not b₂,b₃ // b₄,b₅ & not b₂,b₃ // b₅,b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₂,b₃ // b₄,b₅ & b₂,b₄ // b₃,b₅ & b₃ <> b₅ ) ) & ( for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₄ & b₄,b₂ // b₂,b₅ holds
ex b₆ being Element of b₁ st
( b₃,b₂ // b₂,b₆ & b₃,b₄ // b₅,b₆ ) ) & ( for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃ // b₄,b₅ & not b₂,b₃ // b₅,b₄ holds
ex b₆ being Element of b₁ st
( ( b₂,b₃ // b₂,b₆ or b₂,b₃ // b₆,b₂ ) & ( b₄,b₅ // b₄,b₆ or b₄,b₅ // b₆,b₄ ) ) ) ) iff b₁ is OAffinPlane ) by Def5, Def6, REALSET2:def 7;

theorem Th51: :: ANALOAF:51

for b₁ being RealLinearSpace st ex b₂, b₃ being VECTOR of b₁ st
( ( for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) ) & ( for b₄ being VECTOR of b₁ ex b₅, b₆ being Real st b₄ = (b₅ * b₂) + (b₆ * b₃) ) ) holds
OASpace b₁ is OAffinPlane

proof end;