:: DIRAF semantic presentation

definition

let c₁ be non empty set ;
let c₂ be Relation of [:c₁,c₁:];
func lambda c₂ -> Relation of [:a₁,a₁:] means :Def1: :: DIRAF:def 1
for b₁, b₂, b₃, b₄ being Element of a₁ holds
( [[b₁,b₂],[b₃,b₄]] in a₃ iff ( [[b₁,b₂],[b₃,b₄]] in a₂ or [[b₁,b₂],[b₄,b₃]] in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines lambda DIRAF:def 1 :

definition

let c₁ be non empty AffinStruct ;
func Lambda c₁ -> strict AffinStruct equals :: DIRAF:def 2
AffinStruct(# the carrier of a₁,(lambda the CONGR of a₁) #);
correctness ;

end;

:: deftheorem Def2 defines Lambda DIRAF:def 2 :

registration

let c₁ be non empty AffinStruct ;
cluster Lambda a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th1: :: DIRAF:1

canceled;

theorem Th2: :: DIRAF:2

canceled;

theorem Th3: :: DIRAF:3

canceled;

theorem Th4: :: DIRAF:4

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ holds b₂,b₃ // b₂,b₃

proof end;

Lemma3: for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₄,b₅ // b₂,b₃

proof end;

theorem Th5: :: DIRAF:5

for b₁ being OAffinSpace
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₂ )

proof end;

theorem Th6: :: DIRAF:6

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

proof end;

theorem Th7: :: DIRAF:7

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₂ // b₃,b₄ & b₃,b₄ // b₂,b₂ )

proof end;

theorem Th8: :: DIRAF:8

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ & b₂,b₃ // b₅,b₄ & not b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th9: :: DIRAF:9

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₃ // b₂,b₄ iff ( b₂,b₃ // b₃,b₄ or b₂,b₄ // b₄,b₃ ) )

proof end;

definition

let c₁ be non empty AffinStruct ;
let c₂, c₃, c₄ be Element of c₁;
pred Mid c₂,c₃,c₄ means :Def3: :: DIRAF:def 3
a₂,a₃ // a₃,a₄;

end;

:: deftheorem Def3 defines Mid DIRAF:def 3 :

theorem Th10: :: DIRAF:10

canceled;

theorem Th11: :: DIRAF:11

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₃ // b₂,b₄ iff ( Mid b₂,b₃,b₄ or Mid b₂,b₄,b₃ ) )

proof end;

theorem Th12: :: DIRAF:12

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ st Mid b₂,b₃,b₂ holds
b₂ = b₃

proof end;

theorem Th13: :: DIRAF:13

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ st Mid b₂,b₃,b₄ holds
Mid b₄,b₃,b₂

proof end;

theorem Th14: :: DIRAF:14

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ holds
( Mid b₂,b₂,b₃ & Mid b₂,b₃,b₃ )

proof end;

theorem Th15: :: DIRAF:15

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₂,b₄,b₅ holds
Mid b₃,b₄,b₅

proof end;

theorem Th16: :: DIRAF:16

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & Mid b₄,b₂,b₃ & Mid b₂,b₃,b₅ holds
Mid b₄,b₃,b₅

proof end;

theorem Th17: :: DIRAF:17

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st
( Mid b₂,b₃,b₄ & b₃ <> b₄ )

proof end;

theorem Th18: :: DIRAF:18

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₃,b₂,b₄ holds
b₂ = b₃

proof end;

theorem Th19: :: DIRAF:19

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & Mid b₂,b₃,b₄ & Mid b₂,b₃,b₅ & not Mid b₃,b₄,b₅ holds
Mid b₃,b₅,b₄

proof end;

theorem Th20: :: DIRAF:20

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & Mid b₂,b₃,b₄ & Mid b₂,b₃,b₅ & not Mid b₂,b₄,b₅ holds
Mid b₂,b₅,b₄

proof end;

theorem Th21: :: DIRAF:21

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st Mid b₂,b₃,b₄ & Mid b₂,b₅,b₄ & not Mid b₂,b₃,b₅ holds
Mid b₂,b₅,b₃

proof end;

definition

let c₁ be non empty AffinStruct ;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃ '||' c₄,c₅ means :Def4: :: DIRAF:def 4
( a₂,a₃ // a₄,a₅ or a₂,a₃ // a₅,a₄ );

end;

:: deftheorem Def4 defines '||' DIRAF:def 4 :

theorem Th22: :: DIRAF:22

canceled;

theorem Th23: :: DIRAF:23

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( b₂,b₃ '||' b₄,b₅ iff [[b₂,b₃],[b₄,b₅]] in lambda the CONGR of b₁ )

proof end;

theorem Th24: :: DIRAF:24

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ holds
( b₂,b₃ '||' b₃,b₂ & b₂,b₃ '||' b₂,b₃ )

proof end;

theorem Th25: :: DIRAF:25

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ holds
( b₂,b₃ '||' b₄,b₄ & b₄,b₄ '||' b₂,b₃ )

proof end;

Lemma16: for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & b₂,b₃ '||' b₄,b₅ & b₂,b₃ '||' b₆,b₇ holds
b₄,b₅ '||' b₆,b₇

proof end;

theorem Th26: :: DIRAF:26

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃ '||' b₂,b₄ holds
b₃,b₂ '||' b₃,b₄

proof end;

theorem Th27: :: DIRAF:27

for b₁ being OAffinSpace
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 Th28: :: DIRAF:28

for b₁ being OAffinSpace
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 Th29: :: DIRAF:29

for b₁ being OAffinSpace holds
not for b₂, b₃, b₄ being Element of b₁ holds b₂,b₃ '||' b₂,b₄

proof end;

theorem Th30: :: DIRAF:30

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₂,b₃ '||' b₄,b₅ & b₄ <> b₅ )

proof end;

theorem Th31: :: DIRAF:31

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st
( b₂,b₃ '||' b₄,b₅ & b₂,b₄ '||' b₃,b₅ )

proof end;

theorem Th32: :: DIRAF:32

for b₁ being OAffinSpace
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₆ )

proof end;

definition

let c₁ be non empty AffinStruct ;
let c₂, c₃, c₄ be Element of c₁;
pred LIN c₂,c₃,c₄ means :Def5: :: DIRAF:def 5
a₂,a₃ '||' a₂,a₄;

end;

:: deftheorem Def5 defines LIN DIRAF:def 5 :

notation

let c₁ be non empty AffinStruct ;
let c₂, c₃, c₄ be Element of c₁;
synonym c₂,c₃,c₄ is_collinear for LIN c₂,c₃,c₄;

end;

theorem Th33: :: DIRAF:33

canceled;

theorem Th34: :: DIRAF:34

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ st Mid b₂,b₃,b₄ holds
b₂,b₃,b₄ is_collinear

proof end;

theorem Th35: :: DIRAF:35

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ holds
( not b₂,b₃,b₄ is_collinear or Mid b₂,b₃,b₄ or Mid b₃,b₂,b₄ or Mid b₂,b₄,b₃ )

proof end;

Lemma25: for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃,b₄ is_collinear holds
( b₂,b₄,b₃ is_collinear & b₃,b₂,b₄ is_collinear )

proof end;

theorem Th36: :: DIRAF:36

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃,b₄ is_collinear holds
( b₂,b₄,b₃ is_collinear & b₃,b₂,b₄ is_collinear & b₃,b₄,b₂ is_collinear & b₄,b₂,b₃ is_collinear & b₄,b₃,b₂ is_collinear )

proof end;

theorem Th37: :: DIRAF:37

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ holds
( b₂,b₂,b₃ is_collinear & b₂,b₃,b₃ is_collinear & b₂,b₃,b₂ is_collinear )

proof end;

theorem Th38: :: DIRAF:38

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₃,b₆ is_collinear holds
b₄,b₅,b₆ is_collinear

proof end;

theorem Th39: :: DIRAF:39

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃ '||' b₄,b₅ holds
b₂,b₃,b₅ is_collinear

proof end;

theorem Th40: :: DIRAF:40

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
b₂,b₃ '||' b₄,b₅

proof end;

theorem Th41: :: DIRAF:41

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₄,b₅,b₂ is_collinear & b₄,b₅,b₃ is_collinear & b₂,b₃,b₆ is_collinear holds
b₄,b₅,b₆ is_collinear

proof end;

theorem Th42: :: DIRAF:42

for b₁ being OAffinSpace holds
not for b₂, b₃, b₄ being Element of b₁ holds b₂,b₃,b₄ is_collinear

proof end;

theorem Th43: :: DIRAF:43

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear

proof end;

theorem Th44: :: DIRAF:44

canceled;

theorem Th45: :: DIRAF:45

for b₁ being OAffinSpace
for b₂ being non empty AffinStruct st b₂ = Lambda b₁ holds
for b₃, b₄, b₅, b₆ being Element of b₁
for b₇, b₈, b₉, b₁₀ being Element of b₂ st b₃ = b₇ & b₄ = b₈ & b₅ = b₉ & b₆ = b₁₀ holds
( b₇,b₈ // b₉,b₁₀ iff b₃,b₄ '||' b₅,b₆ )

proof end;

theorem Th46: :: DIRAF:46

for b₁ being OAffinSpace
for b₂ being non empty AffinStruct st b₂ = Lambda b₁ holds
( ex b₃, b₄ being Element of b₂ st b₃ <> b₄ & ( for 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₄ // b₇,b₈ implies b₅,b₆ // b₇,b₈ ) & ( b₃,b₄ // b₃,b₅ implies b₄,b₃ // b₄,b₅ ) ) ) & not for b₃, b₄, b₅ being Element of b₂ holds 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₆ ) ) & ( for b₃, b₄, b₅ being Element of b₂ 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 b₅,b₃ // b₃,b₆ & b₃ <> b₅ holds
ex b₇ being Element of b₂ st
( b₄,b₃ // b₃,b₇ & b₄,b₅ // b₆,b₇ ) ) )

proof end;

definition

let c₁ be non empty AffinStruct ;
canceled;
attr a₁ is AffinSpace-like means :Def7: :: DIRAF:def 7
( ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ holds
( b₁,b₂ // b₂,b₁ & b₁,b₂ // 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₃ ) ) ) & not for b₁, b₂, b₃ being Element of a₁ holds 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₄ ) ) & ( for b₁, b₂, b₃ being Element of a₁ ex b₄ being Element of a₁ st
( 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 Def6 DIRAF:def 6 :

:: deftheorem Def7 defines AffinSpace-like DIRAF:def 7 :

registration

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

proof end;

end;

definition

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

end;

theorem Th47: :: DIRAF:47

for b₁ being AffinSpace holds
( ex b₂, b₃ being Element of b₁ st b₂ <> b₃ & ( for 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₃ // b₆,b₇ implies b₄,b₅ // b₆,b₇ ) & ( b₂,b₃ // b₂,b₄ implies b₃,b₂ // b₃,b₄ ) ) ) & not for b₂, b₃, b₄ being Element of b₁ holds 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₅ ) ) & ( for b₂, b₃, b₄ being Element of b₁ 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 b₄,b₂ // b₂,b₅ & b₂ <> b₄ holds
ex b₆ being Element of b₁ st
( b₃,b₂ // b₂,b₆ & b₃,b₄ // b₅,b₆ ) ) ) by Def7, REALSET2:def 7;

theorem Th48: :: DIRAF:48

for b₁ being OAffinSpace holds Lambda b₁ is AffinSpace

proof end;

theorem Th49: :: DIRAF:49

for b₁ being non empty AffinStruct holds
( ( ex b₂, b₃ being Element of b₁ st b₂ <> b₃ & ( for 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₃ // b₆,b₇ implies b₄,b₅ // b₆,b₇ ) & ( b₂,b₃ // b₂,b₄ implies b₃,b₂ // b₃,b₄ ) ) ) & not for b₂, b₃, b₄ being Element of b₁ holds 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₅ ) ) & ( for b₂, b₃, b₄ being Element of b₁ 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 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 AffinSpace ) by Def7, REALSET2:def 7;

theorem Th50: :: DIRAF:50

for b₁ being OAffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃ '||' b₄,b₅ holds
ex b₆ being Element of b₁ st
( b₂,b₃ '||' b₂,b₆ & b₄,b₅ '||' b₄,b₆ )

proof end;

theorem Th51: :: DIRAF:51

for b₁ being non empty AffinStruct
for b₂ being OAffinPlane st b₁ = Lambda b₂ holds
for b₃, b₄, b₅, b₆ being Element of b₁ st not b₃,b₄ // b₅,b₆ holds
ex b₇ being Element of b₁ st
( b₃,b₄ // b₃,b₇ & b₅,b₆ // b₅,b₇ )

proof end;

definition

let c₁ be non empty AffinStruct ;
attr a₁ is 2-dimensional means :Def8: :: DIRAF:def 8
for b₁, b₂, b₃, b₄ being Element of a₁ st not b₁,b₂ // b₃,b₄ holds
ex b₅ being Element of a₁ st
( b₁,b₂ // b₁,b₅ & b₃,b₄ // b₃,b₅ );

end;

:: deftheorem Def8 defines 2-dimensional DIRAF:def 8 :

registration

cluster strict 2-dimensional AffinStruct ;
existence

proof end;

end;

definition

mode AffinPlane is 2-dimensional AffinSpace;

end;

theorem Th52: :: DIRAF:52

canceled;

theorem Th53: :: DIRAF:53

for b₁ being OAffinPlane holds Lambda b₁ is AffinPlane

proof end;

theorem Th54: :: DIRAF:54

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