:: 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
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies DIRAF, SUBSET_1, ANALOAF, AFF_1, INCSP_1, STRUCT_0, XBOOLE_0,
      TARSKI, RELAT_1, PARSP_1, AFF_2, ARYTM_3, AFF_4;
 notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2;
 constructors AFF_1, AFF_2;
 registrations XBOOLE_0, STRUCT_0;
 requirements SUBSET, BOOLE;


begin

reserve AS for AffinSpace;
reserve a,b,c,d,a9,b9,c9,d9,p,q,r,x,y for Element of AS;
reserve A,C,K,M,N,P,Q,X,Y,Z for Subset of AS;

theorem :: AFF_4:1
  (LIN p,a,a9 or LIN p,a9,a) & p<>a implies ex b9 st LIN p,b,b9 & a ,b // a9,b9
;

theorem :: AFF_4:2
  (a,b // A or b,a // A) & a in A implies b in A;

theorem :: AFF_4:3
  (a,b // A or b,a // A) & A // K implies a,b // K & b,a // K;

theorem :: AFF_4:4
  (a,b // A or b,a // A) & (a,b // c,d or c,d // a,b) & a<>b
  implies c,d // A & d,c // A;

theorem :: AFF_4:5
  (a,b // M or b,a // M) & (a,b // N or b,a // N) & a<>b implies M // N;

theorem :: AFF_4:6
  (a,b // M or b,a // M) & (c,d // M or d,c // M) implies a,b // c,d;

theorem :: AFF_4:7
  (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 implies d in C;

theorem :: AFF_4:8
  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
  implies q=b9;

theorem :: AFF_4:9
  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 implies b=b9;

theorem :: AFF_4:10
  (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 implies b=b9;

theorem :: AFF_4:11
  ex A st a in A & b in A & A is being_line;

theorem :: AFF_4:12
  A is being_line implies ex q st not q in A;

definition
  let AS,K,P;
  func Plane(K,P) -> Subset of AS equals
:: AFF_4:def 1
  {a: ex b st a,b // K & b in P};
end;

definition
  let AS,X;
  attr X is being_plane means
:: AFF_4:def 2

  ex K,P st K is being_line & P is being_line & not K // P & X = Plane(K,P);
end;

theorem :: AFF_4:13
  not K is being_line implies Plane(K,P) = {};

theorem :: AFF_4:14
  K is being_line implies P c= Plane(K,P);

theorem :: AFF_4:15
  K // P implies Plane(K,P) = P;

theorem :: AFF_4:16
  K // M implies Plane(K,P) = Plane(M,P);

theorem :: AFF_4:17
  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 implies (P // Q or ex q st q
  in P & q in Q);

theorem :: AFF_4:18
  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 implies (P // Q
  or ex q st q in P & q in Q);

theorem :: AFF_4:19
  X is being_plane & a in X & b in X & a<>b implies Line(a,b) c= X;

theorem :: AFF_4:20
  K is being_line & P is being_line & Q is being_line & not K // Q
  & Q c= Plane(K,P) implies Plane(K,Q) = Plane(K,P);

theorem :: AFF_4:21
  K is being_line & P is being_line & Q is being_line & Q c= Plane
  (K,P) implies P // Q or ex q st q in P & q in Q;

theorem :: AFF_4:22
  X is being_plane & M is being_line & N is being_line & M c= X &
  N c= X implies M // N or ex q st q in M & q in N;

theorem :: AFF_4:23
  X is being_plane & a in X & M c= X & a in N & (M // N or N // M)
  implies N c= X;

theorem :: AFF_4:24
  X is being_plane & Y is being_plane & a in X & b in X & a in Y &
  b in Y & X<>Y & a<>b implies X /\ Y is being_line;

theorem :: AFF_4:25
  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 implies X = Y;

theorem :: AFF_4:26
  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 implies X = Y;

definition
  let AS,a,K such that
 K is being_line;
  func a*K -> Subset of AS means
:: AFF_4:def 3

  a in it & K // it;
end;

theorem :: AFF_4:27
  A is being_line implies a*A is being_line;

theorem :: AFF_4:28
  X is being_plane & M is being_line & a in X & M c= X implies a*M c= X;

theorem :: AFF_4:29
  X is being_plane & a in X & b in X & c in X & a,b // c,d & a<>b
  implies d in X;

theorem :: AFF_4:30
  A is being_line implies ( a in A iff a*A = A );

theorem :: AFF_4:31
  A is being_line implies a*A = a*(q*A);

theorem :: AFF_4:32
  K // M implies a*K=a*M;

definition
  let AS,X,Y;
  pred X '||' Y means
:: AFF_4:def 4

  for a,A st a in Y & A is being_line & A c= X holds a*A c= Y;
end;

theorem :: AFF_4:33
  X c= Y & ( X is being_line & Y is being_line or X is being_plane
  & Y is being_plane ) implies X=Y;

theorem :: AFF_4:34
  X is being_plane implies ex a,b,c st a in X & b in X & c in X & not LIN a,b,c
;

theorem :: AFF_4:35
  M is being_line & X is being_plane implies ex q st q in X & not q in M;

theorem :: AFF_4:36
  for a,A st A is being_line ex X st a in X & A c= X & X is being_plane;

theorem :: AFF_4:37
  ex X st a in X & b in X & c in X & X is being_plane;

theorem :: AFF_4:38
  q in M & q in N & M is being_line & N is being_line implies ex X
  st M c= X & N c= X & X is being_plane;

theorem :: AFF_4:39
  M // N implies ex X st M c= X & N c= X & X is being_plane;

theorem :: AFF_4:40
  M is being_line & N is being_line implies (M // N iff M '||' N);

theorem :: AFF_4:41
  M is being_line & X is being_plane implies (M '||' X iff ex N st
  N c= X & (M // N or N // M) );

theorem :: AFF_4:42
  M is being_line & X is being_plane & M c= X implies M '||' X;

theorem :: AFF_4:43
  A is being_line & X is being_plane & a in A & a in X & A '||' X
  implies A c= X;

definition
  let AS,K,M,N;
  pred K,M,N is_coplanar means
:: AFF_4:def 5

  ex X st K c= X & M c= X & N c= X & X is being_plane;
end;

theorem :: AFF_4:44
  K,M,N is_coplanar implies 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
  M is being_line & N is being_line & M,N,K is_coplanar & M,N,A
  is_coplanar & M<>N implies M,K,A is_coplanar;

theorem :: AFF_4:46
  K is being_line & M is being_line & X is being_plane & K c= X &
  M c= X & K<>M implies (K,M,A is_coplanar iff A c= X);

theorem :: AFF_4:47
  q in K & q in M & K is being_line & M is being_line implies K,M,
  M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar;

theorem :: AFF_4:48
  AS is not AffinPlane & X is being_plane implies ex q st not q in X;

theorem :: AFF_4:49
  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
  implies b,c // b9,c9;

theorem :: AFF_4:50
  AS is not AffinPlane implies AS is Desarguesian;

theorem :: AFF_4:51
  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 implies b,c // b9,c9;

theorem :: AFF_4:52
  AS is not AffinPlane implies AS is translational;

theorem :: AFF_4:53
  AS is AffinPlane & not LIN a,b,c implies ex c9 st a,c // a9,c9 & b,c // b9,c9
;

theorem :: AFF_4:54
  not LIN a,b,c & a9<>b9 & a,b // a9,b9 implies ex c9 st a,c // a9
  ,c9 & b,c // b9,c9;

theorem :: AFF_4:55
  X is being_plane & Y is being_plane implies (X '||' Y iff ex A,P
,M,N 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) );

theorem :: AFF_4:56
  A // M & M '||' X implies A '||' X;

theorem :: AFF_4:57
  X is being_plane implies X '||' X;

theorem :: AFF_4:58
  X is being_plane & Y is being_plane & X '||' Y implies Y '||' X;

theorem :: AFF_4:59
  X is being_plane implies X <> {};

theorem :: AFF_4:60
  X '||' Y & Y '||' Z & Y <> {} implies X '||' Z;

theorem :: AFF_4:61
  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 ) implies X '||' Z;

theorem :: AFF_4:62
  X is being_plane & Y is being_plane & a in X & a in Y & X '||' Y
  implies X=Y;

theorem :: AFF_4:63
  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 implies a,b //
  c,d;

theorem :: AFF_4:64
  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
  implies X/\Z // Y/\Z;

theorem :: AFF_4:65
  for a,X st X is being_plane ex Y st a in Y & X '||' Y & Y is being_plane;

definition
  let AS,a,X such that
 X is being_plane;
  func a+X -> Subset of AS means
:: AFF_4:def 6

  a in it & X '||' it & it is being_plane;
end;

theorem :: AFF_4:66
  X is being_plane implies ( a in X iff a+X = X );

theorem :: AFF_4:67
  X is being_plane implies a+X = a+(q+X);

theorem :: AFF_4:68
  A is being_line & X is being_plane & A '||' X implies a*A c= a+X;

theorem :: AFF_4:69
  X is being_plane & Y is being_plane & X '||' Y implies a+X = a+Y;