:: Planes in Affine Spaces
:: by Wojciech Leo\'nczuk, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: 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 b1 being Subset of AS st
( a in b1 & K // b1 )
by ;
uniqueness
for b1, b2 being Subset of AS st a in b1 & K // b1 & a in b2 & K // b2 holds
b1 = b2
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 b4 being Subset of AS holds
( b4 = a * K iff ( a in b4 & K // b4 ) );

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 b1 being Subset of AS st
( a in b1 & X '||' b1 & b1 is being_plane )
by ;
uniqueness
for b1, b2 being Subset of AS st a in b1 & X '||' b1 & b1 is being_plane & a in b2 & X '||' b2 & b2 is being_plane holds
b1 = b2
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 b4 being Subset of AS holds
( b4 = a + X iff ( a in b4 & X '||' b4 & b4 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;