:: AFF_4 semantic presentation

Lm1: for AS being AffinSpace
for X being Subset of AS
for x being set st x in X holds
x is Element of AS
;

theorem Th1: :: AFF_4:1

for AS being AffinSpace
for p, a, a', b being Element of AS st ( LIN p,a,a' or LIN p,a',a ) & p <> a holds
ex b' being Element of AS st
( LIN p,b,b' & a,b // a',b' )

proof end;

theorem Th2: :: AFF_4:2

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st ( a,b // A or b,a // A ) & a in A holds
b in A

proof end;

theorem Th3: :: AFF_4:3

for AS being AffinSpace
for a, b being Element of AS
for A, K being Subset of AS st ( a,b // A or b,a // A ) & ( A // K or K // A ) holds
( a,b // K & b,a // K )

proof end;

theorem Th4: :: AFF_4:4

for AS being AffinSpace
for a, b, c, d being Element of AS
for A being Subset of AS st ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) & a <> b holds
( c,d // A & d,c // A )

proof end;

theorem :: AFF_4:5

for AS being AffinSpace
for a, b being Element of AS
for M, N being Subset of AS st ( a,b // M or b,a // M ) & ( a,b // N or b,a // N ) & a <> b holds
( M // N & N // M )

proof end;

theorem :: AFF_4:6

for AS being AffinSpace
for a, b, c, d being Element of AS
for M being Subset of AS st ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) holds
( a,b // c,d & a,b // d,c )

proof end;

theorem Th7: :: AFF_4:7

for AS being AffinSpace
for a, b, c, d being Element of AS
for A, C being Subset of AS st ( A // C or C // A ) & a <> b & ( a,b // c,d or c,d // a,b ) & a in A & b in A & c in C holds
d in C

proof end;

Lm2: for AS being AffinSpace
for a, a', d being Element of AS
for A, K being Subset of AS st A // K & a in A & a' in A & d in K holds
ex d' being Element of AS st
( d' in K & a,d // a',d' )

proof end;

theorem Th8: :: AFF_4:8

for AS being AffinSpace
for q, a, a', b, b' being Element of AS
for M, N being Subset of AS st q in M & q in N & a in M & a' in M & b in N & b' in N & q <> a & q <> b & M <> N & ( a,b // a',b' or b,a // b',a' ) & M is_line & N is_line & q = a' holds
q = b'

proof end;

theorem Th9: :: AFF_4:9

proof end;

theorem Th10: :: AFF_4:10

for AS being AffinSpace
for a, a', b, b' being Element of AS
for M, N being Subset of AS st ( M // N or N // M ) & a in M & a' in M & b in N & b' in N & M <> N & ( a,b // a',b' or b,a // b',a' ) & a = a' holds
b = b'

proof end;

theorem Th11: :: AFF_4:11

for AS being AffinSpace
for a, b being Element of AS ex A being Subset of AS st
( a in A & b in A & A is_line )

proof end;

theorem Th12: :: AFF_4:12

for AS being AffinSpace
for A being Subset of AS st A is_line holds
ex q being Element of AS st not q in A

proof end;

definition

let AS be AffinSpace;
let K, P be Subset of AS;
func Plane K,P -> Subset of AS equals :: AFF_4:def 1
{ a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P ) } ;
coherence

proof end;

end;

:: deftheorem defines Plane AFF_4:def 1 :

definition

let AS be AffinSpace;
let X be Subset of AS;
attr X is being_plane means :Def2: :: AFF_4:def 2
ex K, P being Subset of AS st
( K is_line & P is_line & not K // P & X = Plane K,P );

end;

:: deftheorem Def2 defines being_plane AFF_4:def 2 :

notation

let AS be AffinSpace;
let X be Subset of AS;
synonym X is_plane for being_plane X;

end;

Lm3: for AS being AffinSpace
for K, P being Subset of AS
for q being Element of AS holds
( q in Plane K,P iff ex b being Element of AS st
( q,b // K & b in P ) )

proof end;

theorem :: AFF_4:13

for AS being AffinSpace
for K, P being Subset of AS st not K is_line holds
Plane K,P = {}

proof end;

theorem Th14: :: AFF_4:14

for AS being AffinSpace
for K, P being Subset of AS st K is_line holds
P c= Plane K,P

proof end;

theorem :: AFF_4:15

for AS being AffinSpace
for K, P being Subset of AS st K // P holds
Plane K,P = P

proof end;

theorem Th16: :: AFF_4:16

for AS being AffinSpace
for K, M, P being Subset of AS st K // M holds
Plane K,P = Plane M,P

proof end;

theorem :: AFF_4:17

for AS being AffinSpace
for p, a, b, a', b' being Element of AS
for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a' in N & b' in N & not p in P & not p in Q & M <> N & a in P & a' in P & b in Q & b' in Q & M is_line & N is_line & P is_line & Q is_line & not P // Q holds
ex q being Element of AS st
( q in P & q in Q )

proof end;

theorem Th18: :: AFF_4:18

for AS being AffinSpace
for a, b, a', b' being Element of AS
for M, N, P, Q being Subset of AS st a in M & b in M & a' in N & b' in N & a in P & a' in P & b in Q & b' in Q & M <> N & M // N & P is_line & Q is_line & not P // Q holds
ex q being Element of AS st
( q in P & q in Q )

proof end;

Lm4: for AS being AffinSpace
for a being Element of AS
for K, P, Q being Subset of AS st K is_line & P is_line & a in Q & a in Plane K,P & K // Q holds
Q c= Plane K,P

proof end;

Lm5: for AS being AffinSpace
for a, b being Element of AS
for K, P, Q being Subset of AS st K is_line & P is_line & Q is_line & a in Plane K,P & b in Plane K,P & a <> b & a in Q & b in Q holds
Q c= Plane K,P

proof end;

theorem Th19: :: AFF_4:19

for AS being AffinSpace
for a, b being Element of AS
for X being Subset of AS st X is_plane & a in X & b in X & a <> b holds
Line a,b c= X

proof end;

Lm6: for AS being AffinSpace
for K, P, Q being Subset of AS st K is_line & P is_line & Q is_line & Q c= Plane K,P holds
Plane K,Q c= Plane K,P

proof end;

theorem Th20: :: AFF_4:20

for AS being AffinSpace
for K, P, Q being Subset of AS st K is_line & P is_line & Q is_line & not K // P & not K // Q & Q c= Plane K,P holds
Plane K,Q = Plane K,P

proof end;

theorem Th21: :: AFF_4:21

for AS being AffinSpace
for K, P, Q being Subset of AS st K is_line & P is_line & Q is_line & Q c= Plane K,P & not P // Q holds
ex q being Element of AS st
( q in P & q in Q )

proof end;

theorem Th22: :: AFF_4:22

for AS being AffinSpace
for X, M, N being Subset of AS st X is_plane & M is_line & N is_line & M c= X & N c= X & not M // N holds
ex q being Element of AS st
( q in M & q in N )

proof end;

theorem Th23: :: AFF_4:23

for AS being AffinSpace
for a being Element of AS
for X, M, N being Subset of AS st X is_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds
N c= X

proof end;

theorem Th24: :: AFF_4:24

for AS being AffinSpace
for a, b being Element of AS
for X, Y being Subset of AS st X is_plane & Y is_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds
X /\ Y is_line

proof end;

theorem Th25: :: AFF_4:25

for AS being AffinSpace
for a, b, c being Element of AS
for X, Y being Subset of AS st X is_plane & Y is_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds
X = Y

proof end;

Lm7: for AS being AffinSpace
for a, b, c being Element of AS
for M being Subset of AS st M is_line & a in M & b in M & a <> b & not c in M holds
not LIN a,b,c

proof end;

theorem Th26: :: AFF_4:26

for AS being AffinSpace
for X, Y, M, N being Subset of AS st X is_plane & Y is_plane & M is_line & N is_line & M c= X & N c= X & M c= Y & N c= Y & M <> N holds
X = Y

proof end;

definition

let AS be AffinSpace;
let a be Element of AS;
let K be Subset of AS;
assume A1: K is_line ;
func a * K -> Subset of AS means :Def3: :: AFF_4:def 3
( a in it & K // it );
existence by A1, AFF_1:63;
uniqueness by AFF_1:64;

end;

:: deftheorem Def3 defines * AFF_4:def 3 :

theorem Th27: :: AFF_4:27

for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line holds
a * A is_line

proof end;

theorem Th28: :: AFF_4:28

for AS being AffinSpace
for a being Element of AS
for X, M being Subset of AS st X is_plane & M is_line & a in X & M c= X holds
a * M c= X

proof end;

theorem Th29: :: AFF_4:29

for AS being AffinSpace
for a, b, c, d being Element of AS
for X being Subset of AS st X is_plane & a in X & b in X & c in X & a,b // c,d & a <> b holds
d in X

proof end;

theorem :: AFF_4:30

for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line holds
( a in A iff a * A = A )

proof end;

theorem Th31: :: AFF_4:31

for AS being AffinSpace
for a, q being Element of AS
for A being Subset of AS st A is_line holds
a * A = a * (q * A)

proof end;

Lm8: for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line & a in A holds
a * A = A

proof end;

theorem Th32: :: AFF_4:32

for AS being AffinSpace
for a being Element of AS
for K, M being Subset of AS st K // M holds
a * K = a * M

proof end;

definition

let AS be AffinSpace;
let X, Y be Subset of AS;
pred X '||' Y means :Def4: :: AFF_4:def 4
for a being Element of AS
for A being Subset of AS st a in Y & A is_line & A c= X holds
a * A c= Y;

end;

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

theorem Th33: :: AFF_4:33

for AS being AffinSpace
for X, Y being Subset of AS st X c= Y & ( ( X is_line & Y is_line ) or ( X is_plane & Y is_plane ) ) holds
X = Y

proof end;

theorem Th34: :: AFF_4:34

for AS being AffinSpace
for X being Subset of AS st X is_plane holds
ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )

proof end;

Lm9: for AS being AffinSpace
for a being Element of AS
for X being Subset of AS st X is_plane holds
ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )

proof end;

theorem :: AFF_4:35

for AS being AffinSpace
for M, X being Subset of AS st M is_line & X is_plane holds
ex q being Element of AS st
( q in X & not q in M )

proof end;

theorem Th36: :: AFF_4:36

for AS being AffinSpace
for a being Element of AS
for A being Subset of AS st A is_line holds
ex X being Subset of AS st
( a in X & A c= X & X is_plane )

proof end;

theorem Th37: :: AFF_4:37

for AS being AffinSpace
for a, b, c being Element of AS ex X being Subset of AS st
( a in X & b in X & c in X & X is_plane )

proof end;

theorem Th38: :: AFF_4:38

for AS being AffinSpace
for q being Element of AS
for M, N being Subset of AS st q in M & q in N & M is_line & N is_line holds
ex X being Subset of AS st
( M c= X & N c= X & X is_plane )

proof end;

theorem Th39: :: AFF_4:39

for AS being AffinSpace
for M, N being Subset of AS st M // N holds
ex X being Subset of AS st
( M c= X & N c= X & X is_plane )

proof end;

theorem :: AFF_4:40

for AS being AffinSpace
for M, N being Subset of AS st M is_line & N is_line holds
( M // N iff M '||' N )

proof end;

theorem Th41: :: AFF_4:41

for AS being AffinSpace
for M, X being Subset of AS st M is_line & X is_plane holds
( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )

proof end;

theorem :: AFF_4:42

for AS being AffinSpace
for M, X being Subset of AS st M is_line & X is_plane & M c= X holds
M '||' X

proof end;

theorem :: AFF_4:43

for AS being AffinSpace
for a being Element of AS
for A, X being Subset of AS st A is_line & X is_plane & a in A & a in X & A '||' X holds
A c= X

proof end;

definition

let AS be AffinSpace;
let K, M, N be Subset of AS;
pred K,M,N is_coplanar means :Def5: :: AFF_4:def 5
ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is_plane );

end;

:: deftheorem Def5 defines is_coplanar AFF_4:def 5 :

theorem Th44: :: AFF_4:44

for AS being AffinSpace
for K, M, N being Subset of AS st K,M,N is_coplanar holds
( K,N,M is_coplanar & M,K,N is_coplanar & M,N,K is_coplanar & N,K,M is_coplanar & N,M,K is_coplanar )

proof end;

theorem :: AFF_4:45

for AS being AffinSpace
for A, K, M, N being Subset of AS st A is_line & K is_line & M is_line & N is_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N holds
M,K,A is_coplanar

proof end;

theorem Th46: :: AFF_4:46

for AS being AffinSpace
for K, M, X, A being Subset of AS st K is_line & M is_line & X is_plane & K c= X & M c= X & K <> M holds
( K,M,A is_coplanar iff A c= X )

proof end;

theorem Th47: :: AFF_4:47

for AS being AffinSpace
for q being Element of AS
for K, M being Subset of AS st q in K & q in M & K is_line & M is_line holds
( K,M,M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar )

proof end;

theorem Th48: :: AFF_4:48

for AS being AffinSpace
for X being Subset of AS st AS is not AffinPlane & X is_plane holds
ex q being Element of AS st not q in X

proof end;

Lm10: for AS being AffinSpace
for q, a, b, c, a', b', c' being Element of AS
for A, P, C being Subset of AS st q in A & q in P & q in C & not A,P,C is_coplanar & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'

proof end;

theorem Th49: :: AFF_4:49

for AS being AffinSpace
for q, a, b, c, a', b', c' being Element of AS
for A, P, C being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'

proof end;

theorem :: AFF_4:50

for AS being AffinSpace st AS is not AffinPlane holds
AS is Desarguesian

proof end;

Lm11: for AS being AffinSpace
for a, a', b, b', c, c' being Element of AS
for A, P, C being Subset of AS st A // P & A // C & not A,P,C is_coplanar & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'

proof end;

theorem Th51: :: AFF_4:51

for AS being AffinSpace
for a, a', b, b', c, c' being Element of AS
for A, P, C being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'

proof end;

theorem :: AFF_4:52

for AS being AffinSpace st AS is not AffinPlane holds
AS is translational

proof end;

theorem Th53: :: AFF_4:53

for AS being AffinSpace
for a, b, c, a', b' being Element of AS st AS is AffinPlane & not LIN a,b,c holds
ex c' being Element of AS st
( a,c // a',c' & b,c // b',c' )

proof end;

Lm12: for AS being AffinSpace
for a, b, c, a', b' being Element of AS
for X being Subset of AS st not LIN a,b,c & a' <> b' & a,b // a',b' & a in X & b in X & c in X & X is_plane & a' in X holds
ex c' being Element of AS st
( a,c // a',c' & b,c // b',c' )

proof end;

theorem Th54: :: AFF_4:54

for AS being AffinSpace
for a, b, c, a', b' being Element of AS st not LIN a,b,c & a' <> b' & a,b // a',b' holds
ex c' being Element of AS st
( a,c // a',c' & b,c // b',c' )

proof end;

theorem Th55: :: AFF_4:55

for AS being AffinSpace
for X, Y being Subset of AS st X is_plane & Y is_plane holds
( X '||' Y iff ex A, P, M, N being Subset of AS st
( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )

proof end;

theorem :: AFF_4:56

for AS being AffinSpace
for A, M, X being Subset of AS st A // M & M '||' X holds
A '||' X

proof end;

theorem Th57: :: AFF_4:57

for AS being AffinSpace
for X being Subset of AS st X is_plane holds
X '||' X

proof end;

theorem Th58: :: AFF_4:58

for AS being AffinSpace
for X, Y being Subset of AS st X is_plane & Y is_plane & X '||' Y holds
Y '||' X

proof end;

theorem Th59: :: AFF_4:59

for AS being AffinSpace
for X being Subset of AS st X is_plane holds
X <> {}

proof end;

theorem Th60: :: AFF_4:60

for AS being AffinSpace
for X, Y, Z being Subset of AS st X '||' Y & Y '||' Z & Y <> {} holds
X '||' Z

proof end;

Lm13: for AS being AffinSpace
for X, Y, Z being Subset of AS st X is_plane & Y is_plane & Z is_plane & X '||' Y & Y '||' Z holds
X '||' Z

proof end;

theorem Th61: :: AFF_4:61

for AS being AffinSpace
for X, Y, Z being Subset of AS st X is_plane & Y is_plane & Z is_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) holds
( X '||' Z & Z '||' X )

proof end;

Lm14: for AS being AffinSpace
for X, Y being Subset of AS st X is_plane & Y is_plane & X '||' Y & X <> Y holds
for a being Element of AS holds
( not a in X or not a in Y )

proof end;

theorem :: AFF_4:62

for AS being AffinSpace
for a being Element of AS
for X, Y being Subset of AS st X is_plane & Y is_plane & a in X & a in Y & X '||' Y holds
X = Y by Lm14;

theorem Th63: :: AFF_4:63

for AS being AffinSpace
for a, b, c, d being Element of AS
for X, Y, Z being Subset of AS st X is_plane & Y is_plane & Z is_plane & X '||' Y & X <> Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z holds
a,b // c,d

proof end;

theorem :: AFF_4:64

for AS being AffinSpace
for a, b, c, d being Element of AS
for X, Y, Z being Subset of AS st X is_plane & Y is_plane & Z is_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds
X /\ Z // Y /\ Z

proof end;

theorem Th65: :: AFF_4:65

for AS being AffinSpace
for a being Element of AS
for X being Subset of AS st X is_plane holds
ex Y being Subset of AS st
( a in Y & X '||' Y & Y is_plane )

proof end;

definition

let AS be AffinSpace;
let a be Element of AS;
let X be Subset of AS;
assume A1: X is_plane ;
func a + X -> Subset of AS means :Def6: :: AFF_4:def 6
( a in it & X '||' it & it is_plane );
existence by A1, Th65;
uniqueness

proof end;

end;

:: deftheorem Def6 defines + AFF_4:def 6 :

theorem :: AFF_4:66

for AS being AffinSpace
for a being Element of AS
for X being Subset of AS st X is_plane holds
( a in X iff a + X = X )

proof end;

theorem :: AFF_4:67

for AS being AffinSpace
for a, q being Element of AS
for X being Subset of AS st X is_plane holds
a + X = a + (q + X)

proof end;

theorem :: AFF_4:68

for AS being AffinSpace
for a being Element of AS
for A, X being Subset of AS st A is_line & X is_plane & A '||' X holds
a * A c= a + X

proof end;

theorem :: AFF_4:69

for AS being AffinSpace
for a being Element of AS
for X, Y being Subset of AS st X is_plane & Y is_plane & X '||' Y holds
a + X = a + Y

proof end;