:: Planes in Affine Spaces
:: by Wojciech Leo\'nczuk, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received December 5, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

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 a, b, a9, p being Element of AS st ( LIN p,a,a9 or LIN p,a9,a ) & p <> a holds
ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 )

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 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

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

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, d, a9 being Element of AS
for A, K being Subset of AS st A // K & a in A & a9 in A & d in K holds
ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 )

proof end;

theorem Th8: :: AFF_4:8

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

proof end;

theorem Th9: :: AFF_4:9

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

proof end;

theorem Th10: :: AFF_4:10

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

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 being_line )

proof end;

theorem Th12: :: AFF_4:12

for AS being AffinSpace
for A being Subset of AS st A is being_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
{ a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P ) } is Subset of AS

proof end;

end;

:: deftheorem defines Plane AFF_4:def 1 :
for AS being AffinSpace
for K, P being Subset of AS holds Plane (K,P) = { a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P ) } ;

definition

let AS be AffinSpace;
let X be Subset of AS;

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

end;

:: deftheorem defines being_plane AFF_4:def 2 :
for AS being AffinSpace
for X being Subset of AS holds
( X is being_plane iff ex K, P being Subset of AS st
( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) );

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 being_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 being_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 a, b, a9, b9, p 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 & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_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, a9, b9 being Element of AS
for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & P is being_line & Q is being_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 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 being_line & P is being_line & Q is being_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 being_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 being_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 being_line & P is being_line & Q is being_line & 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 being_line & P is being_line & Q is being_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 M, N, X being Subset of AS st X is being_plane & M is being_line & N is being_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 M, N, X being Subset of AS st X is being_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 being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds
X /\ Y is being_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 being_plane & Y is being_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 being_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 M, N, X, Y being Subset of AS st X is being_plane & Y is being_plane & M is being_line & N is being_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 being_line ;

func a * K -> Subset of AS means :Def3: :: AFF_4:def 3
( a in it & K // it );

existence
ex b₁ being Subset of AS st
( a in b₁ & K // b₁ ) by A1, AFF_1:49;
uniqueness
for b₁, b₂ being Subset of AS st a in b₁ & K // b₁ & a in b₂ & K // b₂ holds
b₁ = b₂ by AFF_1:50;

end;

:: deftheorem Def3 defines * AFF_4:def 3 :
for AS being AffinSpace
for a being Element of AS
for K being Subset of AS st K is being_line holds
for b₄ being Subset of AS holds
( b₄ = a * K iff ( a in b₄ & K // b₄ ) );

theorem Th27: :: AFF_4:27

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

proof end;

theorem Th28: :: AFF_4:28

for AS being AffinSpace
for a being Element of AS
for M, X being Subset of AS st X is being_plane & M is being_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 being_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 being_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 being_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 being_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 :: AFF_4:def 4
for a being Element of AS
for A being Subset of AS st a in Y & A is being_line & A c= X holds
a * A c= Y;

end;

:: deftheorem defines '||' AFF_4:def 4 :
for AS being AffinSpace
for X, Y being Subset of AS holds
( X '||' Y iff for a being Element of AS
for A being Subset of AS st a in Y & A is being_line & A c= X holds
a * A c= Y );

theorem Th33: :: AFF_4:33

for AS being AffinSpace
for X, Y being Subset of AS st X c= Y & ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) holds
X = Y

proof end;

theorem Th34: :: AFF_4:34

for AS being AffinSpace
for X being Subset of AS st X is being_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 being_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 being_line & X is being_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 being_line holds
ex X being Subset of AS st
( a in X & A c= X & X is being_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 being_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 being_line & N is being_line holds
ex X being Subset of AS st
( M c= X & N c= X & X is being_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 being_plane )

proof end;

theorem :: AFF_4:40

for AS being AffinSpace
for M, N being Subset of AS st M is being_line & N is being_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 being_line & X is being_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 being_line & X is being_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 being_line & X is being_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 :: AFF_4:def 5
ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is being_plane );

end;

:: deftheorem defines is_coplanar AFF_4:def 5 :
for AS being AffinSpace
for K, M, N being Subset of AS holds
( K,M,N is_coplanar iff ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is being_plane ) );

theorem :: 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 ) ;

theorem :: AFF_4:45

for AS being AffinSpace
for A, K, M, N being Subset of AS st M is being_line & N is being_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 A, K, M, X being Subset of AS st K is being_line & M is being_line & X is being_plane & K c= X & M c= X & K <> M holds
( K,M,A is_coplanar iff A c= X ) by Th26;

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 being_line & M is being_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 being_plane holds
ex q being Element of AS st not q in X

proof end;

Lm10: for AS being AffinSpace
for a, b, c, a9, b9, c9, q being Element of AS
for A, C, P 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 & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9

proof end;

theorem Th49: :: AFF_4:49

for AS being AffinSpace
for a, b, c, a9, b9, c9, q being Element of AS
for A, C, P 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 & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9

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, b, c, a9, b9, c9 being Element of AS
for A, C, P being Subset of AS st A // P & A // C & not A,P,C is_coplanar & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9

proof end;

theorem Th51: :: AFF_4:51

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

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, a9, b9 being Element of AS st AS is AffinPlane & not LIN a,b,c holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )

proof end;

Lm12: for AS being AffinSpace
for a, b, c, a9, b9 being Element of AS
for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )

proof end;

theorem Th54: :: AFF_4:54

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

proof end;

theorem Th55: :: AFF_4:55

for AS being AffinSpace
for X, Y being Subset of AS st X is being_plane & Y is being_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 being_plane holds
X '||' X by Th28;

theorem Th58: :: AFF_4:58

for AS being AffinSpace
for X, Y being Subset of AS st X is being_plane & Y is being_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 being_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;

theorem Th61: :: AFF_4:61

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

proof end;

Lm13: for AS being AffinSpace
for X, Y being Subset of AS st X is being_plane & Y is being_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 being_plane & Y is being_plane & a in X & a in Y & X '||' Y holds
X = Y by Lm13;

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 being_plane & Y is being_plane & Z is being_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 being_plane & Y is being_plane & Z is being_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 being_plane holds
ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane )

proof end;

definition

let AS be AffinSpace;
let a be Element of AS;
let X be Subset of AS;
assume A1: X is being_plane ;

func a + X -> Subset of AS means :Def6: :: AFF_4:def 6
( a in it & X '||' it & it is being_plane );

existence
ex b₁ being Subset of AS st
( a in b₁ & X '||' b₁ & b₁ is being_plane ) by A1, Th65;
uniqueness
for b₁, b₂ being Subset of AS st a in b₁ & X '||' b₁ & b₁ is being_plane & a in b₂ & X '||' b₂ & b₂ is being_plane holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines + AFF_4:def 6 :
for AS being AffinSpace
for a being Element of AS
for X being Subset of AS st X is being_plane holds
for b₄ being Subset of AS holds
( b₄ = a + X iff ( a in b₄ & X '||' b₄ & b₄ is being_plane ) );

theorem :: AFF_4:66

for AS being AffinSpace
for a being Element of AS
for X being Subset of AS st X is being_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 being_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 being_line & X is being_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 being_plane & Y is being_plane & X '||' Y holds
a + X = a + Y

proof end;