:: Planes in Affine Spaces :: by Wojciech Leo\'nczuk, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received December 5, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin 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, a9, b 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 ) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; Lm2: for AS being AffinSpace for a, a9, d 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 ) proofend; theorem Th8: :: AFF_4:8 for AS being AffinSpace for q, a, b, b9, a9 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 proofend; theorem Th9: :: AFF_4:9 for AS being AffinSpace for q, a, a9, b, b9 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 proofend; theorem Th10: :: AFF_4:10 for AS being AffinSpace for a, b, b9, a9 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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; attrX is being_plane means :Def2: :: 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 Def2 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 ) ) proofend; 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) = {} proofend; 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) proofend; theorem :: AFF_4:15 for AS being AffinSpace for K, P being Subset of AS st K // P holds Plane (K,P) = P proofend; 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) proofend; theorem :: AFF_4:17 for AS being AffinSpace for p, a, b, a9, b9 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 ) proofend; 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 ) proofend; Lm4: for AS being AffinSpace for a being Element of AS for Q, K, P being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds Q c= Plane (K,P) proofend; 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) proofend; 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 proofend; Lm6: for AS being AffinSpace for K, Q, P being Subset of AS st K is being_line & Q c= Plane (K,P) holds Plane (K,Q) c= Plane (K,P) proofend; 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) proofend; 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 ) proofend; theorem Th22: :: AFF_4:22 for AS being AffinSpace for X, M, N 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 ) proofend; 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 being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds N c= X proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th26: :: AFF_4:26 for AS being AffinSpace for X, Y, M, N 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 proofend; definition let AS be AffinSpace; let a be Element of AS; let K be Subset of AS; assume A1: K is being_line ; funca * 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 A1, AFF_1:49; 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 proofend; 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 being_plane & M is being_line & a in X & M c= X holds a * M c= X proofend; 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 proofend; 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 ) proofend; 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) proofend; 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 proofend; 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 proofend; definition let AS be AffinSpace; let X, Y be Subset of AS; predX '||' 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 being_line & A c= X holds a * A c= Y; end; :: deftheorem Def4 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) ) ) proofend; 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 proofend; 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 proofend; definition let AS be AffinSpace; let K, M, N be Subset of AS; predK,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 being_plane ); end; :: deftheorem Def5 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 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 ) proofend; theorem :: AFF_4:45 for AS being AffinSpace for M, N, K, A 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 proofend; theorem Th46: :: AFF_4:46 for AS being AffinSpace for K, M, X, A 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 ) proofend; 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 ) proofend; 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 proofend; Lm10: for AS being AffinSpace for q, a, b, c, a9, b9, c9 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 & 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 proofend; theorem Th49: :: AFF_4:49 for AS being AffinSpace for q, a, b, c, a9, b9, c9 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 & 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 proofend; theorem :: AFF_4:50 for AS being AffinSpace st AS is not AffinPlane holds AS is Desarguesian proofend; Lm11: for AS being AffinSpace for a, a9, b, b9, c, c9 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 & 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 proofend; theorem Th51: :: AFF_4:51 for AS being AffinSpace for a, a9, b, b9, c, c9 being Element of AS for A, P, C 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 proofend; theorem :: AFF_4:52 for AS being AffinSpace st AS is not AffinPlane holds AS is translational proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) ) ) proofend; theorem :: AFF_4:56 for AS being AffinSpace for A, M, X being Subset of AS st A // M & M '||' X holds A '||' X proofend; theorem Th57: :: AFF_4:57 for AS being AffinSpace for X being Subset of AS st X is being_plane holds X '||' X proofend; 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 proofend; theorem Th59: :: AFF_4:59 for AS being AffinSpace for X being Subset of AS st X is being_plane holds X <> {} proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; definition let AS be AffinSpace; let a be Element of AS; let X be Subset of AS; assume B1: X is being_plane ; funca + 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 B1, Th65; 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 proofend; 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 ) proofend; 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) proofend; 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 proofend; 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 proofend;