:: AFF_1 semantic presentation

definition

let c₁ be AffinSpace;
let c₂, c₃, c₄ be Element of c₁;
pred LIN c₂,c₃,c₄ means :Def1: :: AFF_1:def 1
a₂,a₃ // a₂,a₄;

end;

:: deftheorem Def1 defines LIN AFF_1:def 1 :

theorem Th1: :: AFF_1:1

canceled;

theorem Th2: :: AFF_1:2

canceled;

theorem Th3: :: AFF_1:3

canceled;

theorem Th4: :: AFF_1:4

canceled;

theorem Th5: :: AFF_1:5

canceled;

theorem Th6: :: AFF_1:6

canceled;

theorem Th7: :: AFF_1:7

canceled;

theorem Th8: :: AFF_1:8

canceled;

theorem Th9: :: AFF_1:9

canceled;

theorem Th10: :: AFF_1:10

for b₁ being AffinSpace
for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ <> b₃

proof end;

theorem Th11: :: AFF_1:11

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

proof end;

Lemma4: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₄,b₅ // b₂,b₃

proof end;

theorem Th12: :: AFF_1:12

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

proof end;

Lemma6: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₃,b₂ // b₄,b₅

proof end;

Lemma7: for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ // b₄,b₅ holds
b₂,b₃ // b₅,b₄

proof end;

theorem Th13: :: AFF_1:13

for b₁ being AffinSpace
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 Th14: :: AFF_1:14

for b₁ being AffinSpace
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;

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

proof end;

theorem Th15: :: AFF_1:15

for b₁ being AffinSpace
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 Th16: :: AFF_1:16

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁ holds
( LIN b₂,b₂,b₃ & LIN b₂,b₃,b₃ & LIN b₂,b₃,b₂ )

proof end;

theorem Th17: :: AFF_1:17

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

proof end;

theorem Th18: :: AFF_1:18

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & LIN b₂,b₃,b₄ & b₂,b₃ // b₄,b₅ holds
LIN b₂,b₃,b₅

proof end;

theorem Th19: :: AFF_1:19

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ holds
b₂,b₃ // b₄,b₅

proof end;

theorem Th20: :: AFF_1:20

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

proof end;

theorem Th21: :: AFF_1:21

for b₁ being AffinSpace holds
not for b₂, b₃, b₄ being Element of b₁ holds LIN b₂,b₃,b₄

proof end;

theorem Th22: :: AFF_1:22

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

proof end;

theorem Th23: :: AFF_1:23

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

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃ be Element of c₁;
func Line c₂,c₃ -> Subset of a₁ means :Def2: :: AFF_1:def 2
for b₁ being Element of a₁ holds
( b₁ in a₄ iff LIN a₂,a₃,b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Line AFF_1:def 2 :

Lemma19: for b₁ being AffinSpace
for b₂, b₃ being Element of b₁ holds Line b₂,b₃ c= Line b₃,b₂

proof end;

theorem Th24: :: AFF_1:24

canceled;

theorem Th25: :: AFF_1:25

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁ holds Line b₂,b₃ = Line b₃,b₂

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃ be Element of c₁;
redefine func Line as Line c₂,c₃ -> Subset of a₁;
commutativity by Th25;

end;

theorem Th26: :: AFF_1:26

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁ holds
( b₂ in Line b₂,b₃ & b₃ in Line b₂,b₃ )

proof end;

theorem Th27: :: AFF_1:27

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ in Line b₃,b₄ & b₅ in Line b₃,b₄ & b₂ <> b₅ holds
Line b₂,b₅ c= Line b₃,b₄

proof end;

theorem Th28: :: AFF_1:28

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ in Line b₃,b₄ & b₅ in Line b₃,b₄ & b₃ <> b₄ holds
Line b₃,b₄ c= Line b₂,b₅

proof end;

definition

let c₁ be AffinSpace;
let c₂ be Subset of c₁;
attr a₂ is being_line means :Def3: :: AFF_1:def 3
ex b₁, b₂ being Element of a₁ st
( b₁ <> b₂ & a₂ = Line b₁,b₂ );

end;

:: deftheorem Def3 defines being_line AFF_1:def 3 :

notation

let c₁ be AffinSpace;
let c₂ be Subset of c₁;
synonym c₂ is_line for being_line c₂;

end;

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

proof end;

theorem Th29: :: AFF_1:29

canceled;

theorem Th30: :: AFF_1:30

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₄ is_line & b₅ is_line & b₂ in b₄ & b₃ in b₄ & b₂ in b₅ & b₃ in b₅ & not b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th31: :: AFF_1:31

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_line holds
ex b₃, b₄ being Element of b₁ st
( b₃ in b₂ & b₄ in b₂ & b₃ <> b₄ )

proof end;

theorem Th32: :: AFF_1:32

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line holds
ex b₄ being Element of b₁ st
( b₂ <> b₄ & b₄ in b₃ )

proof end;

theorem Th33: :: AFF_1:33

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁ holds
( LIN b₂,b₃,b₄ iff ex b₅ being Subset of b₁ st
( b₅ is_line & b₂ in b₅ & b₃ in b₅ & b₄ in b₅ ) )

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃ be Element of c₁;
let c₄ be Subset of c₁;
pred c₂,c₃ // c₄ means :Def4: :: AFF_1:def 4
ex b₁, b₂ being Element of a₁ st
( b₁ <> b₂ & a₄ = Line b₁,b₂ & a₂,a₃ // b₁,b₂ );

end;

:: deftheorem Def4 defines // AFF_1:def 4 :

definition

let c₁ be AffinSpace;
let c₂, c₃ be Subset of c₁;
pred c₂ // c₃ means :Def5: :: AFF_1:def 5
ex b₁, b₂ being Element of a₁ st
( a₂ = Line b₁,b₂ & b₁ <> b₂ & b₁,b₂ // a₃ );

end;

:: deftheorem Def5 defines // AFF_1:def 5 :

theorem Th34: :: AFF_1:34

canceled;

theorem Th35: :: AFF_1:35

canceled;

theorem Th36: :: AFF_1:36

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ in Line b₃,b₄ & b₃ <> b₄ holds
( b₅ in Line b₃,b₄ iff b₃,b₄ // b₂,b₅ )

proof end;

theorem Th37: :: AFF_1:37

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_line & b₂ in b₄ holds
( b₃ in b₄ iff b₂,b₃ // b₄ )

proof end;

theorem Th38: :: AFF_1:38

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ holds
( b₂ <> b₃ & b₄ = Line b₂,b₃ iff ( b₄ is_line & b₂ in b₄ & b₃ in b₄ & b₂ <> b₃ ) ) by Def3, Lemma25, Th26;

theorem Th39: :: AFF_1:39

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Subset of b₁ st b₅ is_line & b₂ in b₅ & b₃ in b₅ & b₂ <> b₃ & LIN b₂,b₃,b₄ holds
b₄ in b₅

proof end;

theorem Th40: :: AFF_1:40

for b₁ being AffinSpace
for b₂ being Subset of b₁ st ex b₃, b₄ being Element of b₁ st b₃,b₄ // b₂ holds
b₂ is_line

proof end;

theorem Th41: :: AFF_1:41

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st b₂ in b₆ & b₃ in b₆ & b₆ is_line & b₂ <> b₃ holds
( b₄,b₅ // b₆ iff b₄,b₅ // b₂,b₃ )

proof end;

theorem Th42: :: AFF_1:42

canceled;

theorem Th43: :: AFF_1:43

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
b₂,b₃ // Line b₂,b₃

proof end;

theorem Th44: :: AFF_1:44

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_line holds
( b₂,b₃ // b₄ iff ex b₅, b₆ being Element of b₁ st
( b₅ <> b₆ & b₅ in b₄ & b₆ in b₄ & b₂,b₃ // b₅,b₆ ) )

proof end;

theorem Th45: :: AFF_1:45

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st b₆ is_line & b₂,b₃ // b₆ & b₄,b₅ // b₆ holds
b₂,b₃ // b₄,b₅

proof end;

theorem Th46: :: AFF_1:46

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

proof end;

theorem Th47: :: AFF_1:47

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line holds
b₂,b₂ // b₃

proof end;

theorem Th48: :: AFF_1:48

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ holds
b₃,b₂ // b₄

proof end;

theorem Th49: :: AFF_1:49

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ holds
not b₃ in b₄

proof end;

theorem Th50: :: AFF_1:50

for b₁ being AffinSpace
for b₂, b₃ being Subset of b₁ st b₂ // b₃ holds
( b₂ is_line & b₃ is_line )

proof end;

theorem Th51: :: AFF_1:51

for b₁ being AffinSpace
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₄,b₅ // b₆,b₇ & b₂ = Line b₄,b₅ & b₃ = Line b₆,b₇ ) )

proof end;

theorem Th52: :: AFF_1:52

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

proof end;

theorem Th53: :: AFF_1:53

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇ being Subset 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 Th54: :: AFF_1:54

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₂ in b₄ & b₃ in b₄ & b₄ // b₅ holds
b₂,b₃ // b₅

proof end;

theorem Th55: :: AFF_1:55

for b₁ being AffinSpace
for b₂ being Subset of b₁ st b₂ is_line holds
b₂ // b₂

proof end;

theorem Th56: :: AFF_1:56

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

proof end;

definition

let c₁ be AffinSpace;
let c₂, c₃ be Subset of c₁;
redefine pred // as c₂ // c₃;
symmetry by Th56;

end;

theorem Th57: :: AFF_1:57

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₂,b₃ // b₄ & b₄ // b₅ holds
b₂,b₃ // b₅

proof end;

Lemma49: for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ // b₃ & b₃ // b₄ holds
b₂ // b₄

proof end;

theorem Th58: :: AFF_1:58

for b₁ being AffinSpace
for b₂, b₃, b₄ being Subset of b₁ st ( ( b₂ // b₃ & b₃ // b₄ ) or ( b₂ // b₃ & b₄ // b₃ ) or ( b₃ // b₂ & b₃ // b₄ ) or ( b₃ // b₂ & b₄ // b₃ ) ) holds
b₂ // b₄ by Lemma49;

theorem Th59: :: AFF_1:59

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ // b₄ & b₂ in b₃ & b₂ in b₄ holds
b₃ = b₄

proof end;

theorem Th60: :: AFF_1:60

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Subset of b₁ st b₂ in b₅ & not b₃ in b₅ & b₃,b₄ // b₅ & not b₃ = b₄ holds
not LIN b₂,b₃,b₄

proof end;

theorem Th61: :: AFF_1:61

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁
for b₇ being Subset of b₁ st b₂,b₃ // b₇ & b₄,b₅ // b₇ & LIN b₆,b₂,b₄ & LIN b₆,b₃,b₅ & b₆ in b₇ & not b₂ in b₇ & b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th62: :: AFF_1:62

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

proof end;

theorem Th63: :: AFF_1:63

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is_line holds
ex b₄ being Subset of b₁ st
( b₂ in b₄ & b₃ // b₄ )

proof end;

theorem Th64: :: AFF_1:64

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄, b₅ being Subset of b₁ st b₃ // b₄ & b₃ // b₅ & b₂ in b₄ & b₂ in b₅ holds
b₄ = b₅

proof end;

theorem Th65: :: AFF_1:65

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st b₆ is_line & b₂ in b₆ & b₃ in b₆ & b₄ in b₆ & b₅ in b₆ holds
b₂,b₃ // b₄,b₅

proof end;

theorem Th66: :: AFF_1:66

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_line & b₂ in b₄ & b₃ in b₄ holds
b₂,b₃ // b₄ by Th37;

theorem Th67: :: AFF_1:67

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₂,b₃ // b₄ & b₂,b₃ // b₅ & b₂ <> b₃ holds
b₄ // b₅

proof end;

theorem Th68: :: AFF_1:68

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ & LIN b₂,b₄,b₆ & b₃,b₄ // b₅,b₆ & b₅ = b₆ holds
( b₅ = b₂ & b₆ = b₂ )

proof end;

theorem Th69: :: AFF_1:69

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

proof end;

theorem Th70: :: AFF_1:70

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ & LIN b₂,b₄,b₆ & LIN b₂,b₄,b₇ & b₃,b₄ // b₅,b₆ & b₃,b₄ // b₅,b₇ holds
b₆ = b₇

proof end;

theorem Th71: :: AFF_1:71

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

theorem Th72: :: AFF_1:72

for b₁ being AffinPlane
for b₂, b₃ being Subset of b₁ st b₂ is_line & b₃ is_line & not b₂ // b₃ holds
ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ in b₃ )

proof end;

theorem Th73: :: AFF_1:73

for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₄ is_line & not b₂,b₃ // b₄ holds
ex b₅ being Element of b₁ st
( b₅ in b₄ & LIN b₂,b₃,b₅ )

proof end;

theorem Th74: :: AFF_1:74

for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃ // b₄,b₅ holds
ex b₆ being Element of b₁ st
( LIN b₂,b₃,b₆ & LIN b₄,b₅,b₆ )

proof end;