:: Planes in Affine Spaces
:: by Wojciech Leo\'nczuk, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received December 5, 1990
:: Copyright (c) 1990-2026 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;
definitions TARSKI;
expansions TARSKI;
theorems AFF_1, DIRAF, TARSKI, AFF_2, XBOOLE_0, XBOOLE_1;
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;
Lm1: for x being set st x in X holds x is Element of AS;
theorem Th1:
(LIN p,a,a9 or LIN p,a9,a) & p<>a implies ex b9 st LIN p,b,b9 & a ,b // a9,b9
proof
assume that
A1: LIN p,a,a9 or LIN p,a9,a and
A2: p<>a;
LIN p,a,a9 by A1,AFF_1:6;
then p,a // p,a9 by AFF_1:def 1;
then a,p // p,a9 by AFF_1:4;
then consider b9 such that
A3: b,p // p,b9 and
A4: b,a // a9,b9 by A2,DIRAF:40;
p,b // p,b9 by A3,AFF_1:4;
then
A5: LIN p,b, b9 by AFF_1:def 1;
a,b // a9,b9 by A4,AFF_1:4;
hence thesis by A5;
end;
theorem Th2:
(a,b // A or b,a // A) & a in A implies b in A
proof
assume that
A1: a,b // A or b,a // A and
A2: a in A;
a,b // A & A is being_line by A1,AFF_1:26,34;
hence thesis by A2,AFF_1:23;
end;
theorem Th3:
(a,b // A or b,a // A) & A // K implies a,b // K & b,a // K
proof
assume that
A1: a,b // A or b,a // A and
A2: A // K;
a,b // A by A1,AFF_1:34;
hence a,b // K by A2,AFF_1:43;
hence thesis by AFF_1:34;
end;
theorem Th4:
(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
proof
assume that
A1: ( a,b // A or b,a // A)&( a,b // c,d or c,d // a,b) and
A2: a<>b;
a,b // A & a,b // c,d by A1,AFF_1:4,34;
hence c,d // A by A2,AFF_1:32;
hence thesis by AFF_1:34;
end;
theorem
(a,b // M or b,a // M) & (a,b // N or b,a // N) & a<>b implies M // N
proof
assume that
A1: ( a,b // M or b,a // M)&( a,b // N or b,a // N) and
A2: a<>b;
a,b // M & a,b // N by A1,AFF_1:34;
hence thesis by A2,AFF_1:53;
end;
theorem
(a,b // M or b,a // M) & (c,d // M or d,c // M) implies a,b // c,d
proof
assume ( a,b // M or b,a // M)&( c,d // M or d,c // M);
then A1: a,b // M & c,d // M by AFF_1:34;
then M is being_line by AFF_1:26;
hence thesis by A1,AFF_1:31;
end;
theorem Th7:
(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
proof
assume that
A1: A // C or C // A and
A2: a<>b &( a,b // c,d or c,d // a,b) and
A3: a in A & b in A and
A4: c in C;
A is being_line by A1,AFF_1:36;
then a,b // A by A3,AFF_1:52;
then c,d // A by A2,Th4;
then c,d // C by A1,Th3;
hence thesis by A4,Th2;
end;
Lm2: A // K & a in A & a9 in A & d in K implies ex d9 st d9 in K & a,d // a9,
d9
proof
assume that
A1: A // K and
A2: a in A & a9 in A and
A3: d in K;
A4: A is being_line by A1,AFF_1:36;
now
assume
A5: a<>a9;
consider d9 such that
A6: a,a9 // d,d9 and
A7: a,d // a9,d9 by DIRAF:40;
d,d9 // a,a9 by A6,AFF_1:4;
then d,d9 // A by A2,A4,A5,AFF_1:27;
then d,d9 // K by A1,Th3;
then d9 in K by A3,Th2;
hence thesis by A7;
end;
hence thesis by A3,AFF_1:2;
end;
theorem Th8:
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
proof
assume that
A1: q in M and
A2: q in N and
A3: a in M and
A4: b in N and
A5: b9 in N and
A6: q<>a and
A7: q<>b & M<>N and
A8: a,b // a9,b9 or b,a // b9,a9 and
A9: M is being_line and
A10: N is being_line and
A11: q=a9;
A12: not LIN q,a,b
proof
assume not thesis;
then consider A such that
A13: A is being_line & q in A and
A14: a in A and
A15: b in A by AFF_1:21;
M=A by A1,A3,A6,A9,A13,A14,AFF_1:18;
hence contradiction by A2,A4,A7,A10,A13,A15,AFF_1:18;
end;
LIN q,b,b9 & a,b // a9,b9 by A2,A4,A5,A8,A10,AFF_1:4,21;
hence thesis by A11,A12,AFF_1:55;
end;
theorem Th9:
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
proof
assume that
A1: q in M and
A2: q in N and
A3: a in M and
A4: a9 in M and
A5: b in N and
A6: b9 in N and
A7: q<>a and
A8: q<>b & M<>N and
A9: a,b // a9,b9 or b,a // b9,a9 and
A10: M is being_line and
A11: N is being_line and
A12: a=a9;
A13: a,b // a9,b & a,b // a9,b9 by A9,A12,AFF_1:2,4;
A14: not LIN q,a,b
proof
assume not thesis;
then consider A such that
A15: A is being_line & q in A and
A16: a in A and
A17: b in A by AFF_1:21;
M=A by A1,A3,A7,A10,A15,A16,AFF_1:18;
hence contradiction by A2,A5,A8,A11,A15,A17,AFF_1:18;
end;
A18: LIN q,b,b by AFF_1:7;
LIN q,a,a9 & LIN q,b,b9 by A1,A2,A3,A4,A5,A6,A10,A11,AFF_1:21;
hence thesis by A14,A18,A13,AFF_1:56;
end;
theorem Th10:
(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
proof
assume that
A1: M // N or N // M and
A2: a in M and
A3: b in N & b9 in N and
A4: M<>N and
A5: ( a,b // a9,b9 or b,a // b9,a9)& a=a9;
a,b // a,b9 by A5,AFF_1:4;
then LIN a,b,b9 by AFF_1:def 1;
then
A6: LIN b,b9,a by AFF_1:6;
assume
A7: b<>b9;
N is being_line by A1,AFF_1:36;
then a in N by A3,A6,A7,AFF_1:25;
hence contradiction by A1,A2,A4,AFF_1:45;
end;
theorem Th11:
ex A st a in A & b in A & A is being_line
proof
LIN a,b,b by AFF_1:7;
then ex A st A is being_line & a in A & b in A & b in A by AFF_1:21;
hence thesis;
end;
theorem Th12:
A is being_line implies ex q st not q in A
proof
assume
A1: A is being_line;
then consider a,b such that
A2: a in A & b in A and
A3: a<>b by AFF_1:19;
consider q such that
A4: not LIN a,b,q by A3,AFF_1:13;
not q in A by A1,A2,A4,AFF_1:21;
hence thesis;
end;
definition
let AS,K,P;
func Plane(K,P) -> Subset of AS equals
{a: ex b st a,b // K & b in P};
coherence
proof
set X = {a: ex b st a,b // K & b in P};
now
let x be object;
assume x in X;
then ex a st a=x & ex b st a,b // K & b in P;
hence x in the carrier of AS;
end;
hence thesis by TARSKI:def 3;
end;
end;
definition
let AS,X;
attr X is being_plane means
ex K,P st K is being_line & P is being_line & not K // P & X = Plane(K,P);
end;
Lm3: for q holds (q in Plane(K,P) iff ex b st q,b // K & b in P)
proof
let q;
now
assume q in Plane(K,P);
then ex a st a=q & ex b st a,b // K & b in P;
hence ex b st q,b // K & b in P;
end;
hence thesis;
end;
theorem
not K is being_line implies Plane(K,P) = {}
proof
assume
A1: not K is being_line;
set x = the Element of Plane(K,P);
assume Plane(K,P)<>{};
then x in Plane(K,P);
then ex a st x=a & ex b st a,b // K & b in P;
hence contradiction by A1,AFF_1:26;
end;
theorem Th14:
K is being_line implies P c= Plane(K,P)
proof
assume
A1: K is being_line;
let x be object;
assume
A2: x in P;
then reconsider a=x as Element of AS;
a,a // K by A1,AFF_1:33;
hence x in Plane(K,P) by A2;
end;
theorem
K // P implies Plane(K,P) = P
proof
set X=Plane(K,P);
assume
A1: K // P;
then
A2: P is being_line by AFF_1:36;
now
let x be object;
assume x in X;
then consider a such that
A3: x=a and
A4: ex b st a,b // K & b in P;
consider b such that
A5: a,b // K and
A6: b in P by A4;
a,b // P by A1,A5,AFF_1:43;
then b,a // P by AFF_1:34;
hence x in P by A2,A3,A6,AFF_1:23;
end;
then
A7: X c= P;
K is being_line by A1,AFF_1:36;
then P c= X by Th14;
hence thesis by A7,XBOOLE_0:def 10;
end;
theorem Th16:
K // M implies Plane(K,P) = Plane(M,P)
proof
assume
A1: K // M;
now
let x be object;
A2: now
assume x in Plane(M,P);
then consider a such that
A3: x=a and
A4: ex b st a,b // M & b in P;
consider b such that
A5: a,b // M and
A6: b in P by A4;
a,b // K by A1,A5,AFF_1:43;
hence x in Plane(K,P) by A3,A6;
end;
now
assume x in Plane(K,P);
then consider a such that
A7: x=a and
A8: ex b st a,b // K & b in P;
consider b such that
A9: a,b // K and
A10: b in P by A8;
a,b // M by A1,A9,AFF_1:43;
hence x in Plane(M,P) by A7,A10;
end;
hence x in Plane(K,P) iff x in Plane(M,P) by A2;
end;
hence thesis by TARSKI:2;
end;
theorem
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)
proof
assume that
A1: p in M and
A2: a in M and
A3: b in M and
A4: p in N and
A5: a9 in N and
A6: b9 in N and
A7: not p in P and
A8: not p in Q and
A9: M<>N and
A10: a in P and
A11: a9 in P and
A12: b in Q and
A13: b9 in Q and
A14: M is being_line and
A15: N is being_line and
A16: P is being_line and
A17: Q is being_line;
A18: a<>a9 by A1,A2,A4,A5,A7,A9,A10,A14,A15,AFF_1:18;
LIN p,a,b by A1,A2,A3,A14,AFF_1:21;
then consider c such that
A19: LIN p,a9,c and
A20: a,a9 // b,c by A7,A10,Th1;
set D=Line(b,c);
A21: b in D by AFF_1:15;
A22: c in D by AFF_1:15;
A23: b<>b9 by A1,A3,A4,A6,A8,A9,A12,A14,A15,AFF_1:18;
A24: c in N by A4,A5,A7,A11,A15,A19,AFF_1:25;
then
A25: b<>c by A1,A3,A4,A8,A9,A12,A14,A15,AFF_1:18;
then
A26: D is being_line by AFF_1:def 3;
now
assume D<>Q;
then
A27: c <>b9 by A12,A13,A17,A23,A26,A21,A22,AFF_1:18;
LIN b9,c,a9 by A5,A6,A15,A24,AFF_1:21;
then consider q such that
A28: LIN b9,b,q and
A29: c,b // a9,q by A27,Th1;
a9,a // c,b by A20,AFF_1:4;
then a9,a // a9,q by A25,A29,AFF_1:5;
then LIN a9,a,q by AFF_1:def 1;
then
A30: q in P by A10,A11,A16,A18,AFF_1:25;
q in Q by A12,A13,A17,A23,A28,AFF_1:25;
hence ex q st q in P & q in Q by A30;
end;
hence thesis by A10,A11,A12,A16,A17,A18,A20,A25,A22,AFF_1:38;
end;
theorem Th18:
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)
proof
assume that
A1: a in M and
A2: b in M and
A3: a9 in N and
A4: b9 in N and
A5: a in P and
A6: a9 in P and
A7: b in Q and
A8: b9 in Q and
A9: M<>N and
A10: M // N and
A11: P is being_line and
A12: Q is being_line;
A13: a<>a9 by A1,A3,A9,A10,AFF_1:45;
A14: N is being_line by A10,AFF_1:36;
A15: b<>b9 by A2,A4,A9,A10,AFF_1:45;
A16: M is being_line by A10,AFF_1:36;
now
assume
A17: a<>b;
consider c such that
A18: a,b // a9,c and
A19: a,a9 // b,c by DIRAF:40;
set D=Line(b,c);
A20: b in D by AFF_1:15;
A21: c in D by AFF_1:15;
a,b // N by A1,A2,A10,A16,AFF_1:43,52;
then a9,c // N by A17,A18,AFF_1:32;
then
A22: c in N by A3,A14,AFF_1:23;
then
A23: b<>c by A2,A9,A10,AFF_1:45;
then
A24: D is being_line by AFF_1:def 3;
now
assume D<>Q;
then
A25: c <>b9 by A7,A8,A12,A15,A24,A20,A21,AFF_1:18;
LIN b9,c,a9 by A3,A4,A14,A22,AFF_1:21;
then consider q such that
A26: LIN b9,b,q and
A27: c,b // a9,q by A25,Th1;
a9,a // c,b by A19,AFF_1:4;
then a9,a // a9,q by A23,A27,AFF_1:5;
then LIN a9,a,q by AFF_1:def 1;
then
A28: q in P by A5,A6,A11,A13,AFF_1:25;
q in Q by A7,A8,A12,A15,A26,AFF_1:25;
hence ex q st q in P & q in Q by A28;
end;
hence thesis by A5,A6,A7,A11,A12,A13,A19,A23,A21,AFF_1:38;
end;
hence thesis by A5,A7;
end;
Lm4: a in Q & a in Plane(K,P) & K // Q implies Q c= Plane(K,P)
proof
assume that
A1: a in Q and
A2: a in Plane(K,P) and
A3: K // Q;
A4: Plane(K,P) = Plane(Q,P) by A3,Th16;
let x be object such that
A5: x in Q;
reconsider c = x as Element of AS by A5;
A6: Q is being_line by A3,AFF_1:36;
consider b such that
A7: a,b // K and
A8: b in P by A2,Lm3;
a,b // Q by A3,A7,AFF_1:43;
then b in Q by A1,A6,AFF_1:23;
then c,b // Q by A5,A6,AFF_1:23;
hence x in Plane(K,P) by A8,A4;
end;
Lm5: 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 implies Q c= Plane(K,P)
proof
assume that
A1: K is being_line and
A2: P is being_line and
A3: Q is being_line and
A4: a in Plane(K,P) and
A5: b in Plane(K,P) and
A6: a<>b and
A7: a in Q and
A8: b in Q;
let x be object;
assume
A9: x in Q;
then reconsider c = x as Element of AS;
consider a9 such that
A10: a,a9 // K and
A11: a9 in P by A4,Lm3;
consider Y such that
A12: b in Y and
A13: K // Y by A1,AFF_1:49;
consider X such that
A14: a in X and
A15: K // X by A1,AFF_1:49;
consider b9 such that
A16: b,b9 // K and
A17: b9 in P by A5,Lm3;
b,b9 // Y by A16,A13,AFF_1:43;
then
A18: b9 in Y by A12,Th2;
a,a9 // X by A10,A15,AFF_1:43;
then
A19: a9 in X by A14,Th2;
A20: X // Y by A15,A13,AFF_1:44;
A21: now
A22: now
given q such that
A23: q in P and
A24: q in Q and
A25: not P // Q;
A26: P<>Q by A2,A25,AFF_1:41;
A27: now
assume
A28: q<>b;
then
A29: b<>b9 by A2,A3,A8,A17,A23,A24,A26,AFF_1:18;
A30: now
A31: q,b9 // P by A2,A17,A23,AFF_1:23;
LIN q,b,c by A3,A8,A9,A24,AFF_1:21;
then consider c9 such that
A32: LIN q,b9, c9 and
A33: b,b9 // c,c9 by A28,Th1;
assume
A34: q<>b9;
q,b9 // q,c9 by A32,AFF_1:def 1;
then q,c9 // P by A34,A31,AFF_1:32;
then
A35: c9 in P by A23,Th2;
c,c9 // K by A16,A29,A33,AFF_1:32;
hence x in Plane(K,P) by A35;
end;
now
assume
A36: q=b9;
b,q // Q by A3,A8,A24,AFF_1:23;
then Q c= Plane(K,P) by A4,A7,A16,A28,A36,Lm4,AFF_1:53;
hence x in Plane(K,P) by A9;
end;
hence x in Plane(K,P) by A30;
end;
now
assume
A37: q<>a;
then
A38: a<>a9 by A2,A3,A7,A11,A23,A24,A26,AFF_1:18;
A39: now
A40: q,a9 // P by A2,A11,A23,AFF_1:23;
LIN q,a,c by A3,A7,A9,A24,AFF_1:21;
then consider c9 such that
A41: LIN q,a9, c9 and
A42: a,a9 // c,c9 by A37,Th1;
assume
A43: q<>a9;
q,a9 // q,c9 by A41,AFF_1:def 1;
then q,c9 // P by A43,A40,AFF_1:32;
then
A44: c9 in P by A23,Th2;
c,c9 // K by A10,A38,A42,AFF_1:32;
hence x in Plane(K,P) by A44;
end;
now
assume
A45: q=a9;
a,q // Q by A3,A7,A24,AFF_1:23;
then Q c= Plane(K,P) by A4,A7,A10,A37,A45,Lm4,AFF_1:53;
hence x in Plane(K,P) by A9;
end;
hence x in Plane(K,P) by A39;
end;
hence x in Plane(K,P) by A6,A27;
end;
A46: now
assume
A47: P // Q;
A48: now
assume P<>Q;
then
A49: b<>b9 by A8,A17,A47,AFF_1:45;
now
assume
A50: c <>b;
consider c9 such that
A51: b,c // b9,c9 and
A52: b,b9 // c,c9 by DIRAF:40;
b,c // Q by A3,A8,A9,AFF_1:23;
then b9,c9 // Q by A50,A51,AFF_1:32;
then b9,c9 // P by A47,AFF_1:43;
then
A53: c9 in P by A17,Th2;
c,c9 // K by A16,A49,A52,AFF_1:32;
hence x in Plane(K,P) by A53;
end;
hence x in Plane(K,P) by A5;
end;
now
assume
A54: P=Q;
c,c // K by A1,AFF_1:33;
hence x in Plane(K,P) by A9,A54;
end;
hence x in Plane(K,P) by A48;
end;
assume X<>Y;
then P // Q or ex q st q in P & q in Q by A2,A3,A7,A8,A11,A17,A14,A12,A20
,A19,A18,Th18;
hence x in Plane(K,P) by A46,A22;
end;
A55: X is being_line by A10,A15,AFF_1:26,43;
now
assume X=Y;
then Q = X by A3,A6,A7,A8,A14,A12,A55,AFF_1:18;
then Q c= Plane(K,P) by A4,A7,A15,Lm4;
hence x in Plane(K,P) by A9;
end;
hence x in Plane(K,P) by A21;
end;
theorem Th19:
X is being_plane & a in X & b in X & a<>b implies Line(a,b) c= X
proof
assume that
A1: X is being_plane and
A2: a in X & b in X and
A3: a<>b;
set Q = Line(a,b);
A4: a in Q & b in Q by AFF_1:15;
Q is being_line & ex K,P st K is being_line & P is being_line & not K //
P & X=Plane(K,P) by A1,A3,AFF_1:def 3;
hence thesis by A2,A3,A4,Lm5;
end;
Lm6: K is being_line & Q c= Plane(K,P) implies Plane(K,Q) c= Plane(K,P)
proof
assume that
A1: K is being_line and
A2: Q c= Plane(K,P);
let x be object;
assume x in Plane(K,Q);
then consider a such that
A3: x=a and
A4: ex b st a,b // K & b in Q;
consider b such that
A5: a,b // K and
A6: b in Q by A4;
consider c such that
A7: b,c // K and
A8: c in P by A2,A6,Lm3;
consider M such that
A9: b in M and
A10: K // M by A1,AFF_1:49;
a,b // M by A5,A10,AFF_1:43;
then
A11: a in M by A9,Th2;
b,c // M by A7,A10,AFF_1:43;
then c in M by A9,Th2;
then a,c // K by A10,A11,AFF_1:40;
hence x in Plane(K,P) by A3,A8;
end;
theorem Th20:
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)
proof
assume that
A1: K is being_line and
A2: P is being_line and
A3: Q is being_line and
A4: not K // Q and
A5: Q c= Plane(K,P);
A6: Plane(K,Q) c= Plane(K,P) by A1,A5,Lm6;
consider a,b such that
A7: a in Q and
A8: b in Q and
A9: a<>b by A3,AFF_1:19;
consider b9 such that
A10: b,b9 // K and
A11: b9 in P by A5,A8,Lm3;
b9,b // K by A10,AFF_1:34;
then
A12: b9 in Plane(K,Q) by A8;
consider a9 such that
A13: a,a9 // K and
A14: a9 in P by A5,A7,Lm3;
A15: a9<>b9
proof
consider A such that
A16: a9 in A and
A17: K // A by A1,AFF_1:49;
a9,a // A by A13,A17,Th3;
then
A18: a in A by A16,Th2;
assume a9=b9;
then a9,b // A by A10,A17,Th3;
then
A19: b in A by A16,Th2;
A is being_line by A17,AFF_1:36;
hence contradiction by A3,A4,A7,A8,A9,A17,A19,A18,AFF_1:18;
end;
a9,a // K by A13,AFF_1:34;
then a9 in Plane(K,Q) by A7;
then Plane(K,P) c= Plane(K,Q) by A1,A2,A3,A14,A11,A15,A12,Lm5,Lm6;
hence thesis by A6,XBOOLE_0:def 10;
end;
theorem Th21:
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
proof
assume that
A1: K is being_line and
A2: P is being_line and
A3: Q is being_line and
A4: Q c= Plane(K,P);
consider a,b such that
A5: a in Q and
A6: b in Q and
A7: a<>b by A3,AFF_1:19;
consider a9 such that
A8: a,a9 // K and
A9: a9 in P by A4,A5,Lm3;
consider A such that
A10: a9 in A and
A11: K // A by A1,AFF_1:49;
A12: a9,a // A by A8,A11,Th3;
then
A13: a in A by A10,Th2;
consider b9 such that
A14: b,b9 // K and
A15: b9 in P by A4,A6,Lm3;
consider M such that
A16: b9 in M and
A17: K // M by A1,AFF_1:49;
A18: b9,b // M by A14,A17,Th3;
then
A19: b in M by A16,Th2;
A20: A is being_line by A11,AFF_1:36;
A21: now
assume A=M;
then
A22: b in A by A16,A18,Th2;
a in A by A10,A12,Th2;
then a9 in Q by A3,A5,A6,A7,A10,A20,A22,AFF_1:18;
hence ex q st q in P & q in Q by A9;
end;
A // M by A11,A17,AFF_1:44;
hence thesis by A2,A3,A5,A6,A9,A15,A10,A16,A13,A19,A21,Th18;
end;
theorem Th22:
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
proof
assume that
A1: X is being_plane and
A2: M is being_line and
A3: N is being_line and
A4: M c= X & N c= X;
consider K,P such that
A5: K is being_line and
A6: P is being_line and
not K // P and
A7: X = Plane(K,P) by A1;
A8: now
assume not K // N;
then M c= Plane(K,N) by A3,A4,A5,A6,A7,Th20;
then N // M or ex q st q in N & q in M by A2,A3,A5,Th21;
hence thesis;
end;
now
assume not K // M;
then N c= Plane(K,M) by A2,A4,A5,A6,A7,Th20;
hence thesis by A2,A3,A5,Th21;
end;
hence thesis by A8,AFF_1:44;
end;
theorem Th23:
X is being_plane & a in X & M c= X & a in N & (M // N or N // M)
implies N c= X
proof
assume that
A1: X is being_plane and
A2: a in X and
A3: M c= X and
A4: a in N and
A5: M // N or N // M;
A6: M is being_line by A5,AFF_1:36;
consider K,P such that
A7: K is being_line and
A8: P is being_line and
not K // P and
A9: X = Plane(K,P) by A1;
A10: N is being_line by A5,AFF_1:36;
A11: now
assume
A12: not K // M;
then
A13: X = Plane(K,M) by A3,A6,A7,A8,A9,Th20;
A14: a in Plane(K,M) by A2,A3,A6,A7,A8,A9,A12,Th20;
now
consider a9 such that
A15: a,a9 // K and
A16: a9 in M by A14,Lm3;
consider b9 such that
A17: a9<>b9 and
A18: b9 in M by A6,AFF_1:20;
consider b such that
A19: a9,a // b9,b and
A20: a9,b9 // a,b by DIRAF:40;
assume
A21: M<>N;
then a<>a9 by A4,A5,A16,AFF_1:45;
then b,b9 // K by A15,A19,Th4;
then
A22: b in Plane(K,M) by A18;
A23: a<>b
proof
assume a=b;
then a,a9 // a,b9 by A19,AFF_1:4;
then LIN a, a9,b9 by AFF_1:def 1;
then LIN a9,b9,a by AFF_1:6;
then a in M by A6,A16,A17,A18,AFF_1:25;
hence contradiction by A4,A5,A21,AFF_1:45;
end;
a,b // M by A6,A16,A17,A18,A20,AFF_1:32,52;
then a,b // N by A5,Th3;
then b in N by A4,Th2;
hence thesis by A2,A4,A6,A10,A7,A13,A23,A22,Lm5;
end;
hence thesis by A3;
end;
now
assume K // M;
then K // N by A5,AFF_1:44;
hence thesis by A2,A4,A9,Lm4;
end;
hence thesis by A11;
end;
theorem Th24:
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
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: a in X & b in X and
A4: a in Y & b in Y and
A5: X<>Y and
A6: a<>b;
set Z = X /\ Y;
set Q = Line(a,b);
A7: Q c= X by A1,A3,A6,Th19;
A8: Q c= Y by A2,A4,A6,Th19;
A9: Q is being_line by A6,AFF_1:def 3;
A10: Z c= Q
proof
assume not Z c= Q;
then consider x being object such that
A11: x in Z and
A12: not x in Q;
reconsider a9=x as Element of AS by A11;
A13: x in Y by A11,XBOOLE_0:def 4;
A14: x in X by A11,XBOOLE_0:def 4;
for y being object holds y in X iff y in Y
proof
let y be object;
A15: now
assume
A16: y in Y;
now
reconsider b9=y as Element of AS by A16;
set M = Line(a9,b9);
A17: a9 in M by AFF_1:15;
A18: b9 in M by AFF_1:15;
assume
A19: y<>x;
then
A20: M is being_line by AFF_1:def 3;
A21: M c= Y by A2,A13,A16,A19,Th19;
A22: now
assume not M // Q;
then consider q such that
A23: q in M and
A24: q in Q by A2,A9,A8,A20,A21,Th22;
M = Line(a9,q) by A12,A20,A17,A23,A24,AFF_1:57;
then M c= X by A1,A7,A12,A14,A24,Th19;
hence y in X by A18;
end;
now
assume M // Q;
then M c= X by A1,A7,A14,A17,Th23;
hence y in X by A18;
end;
hence y in X by A22;
end;
hence y in X by A11,XBOOLE_0:def 4;
end;
now
assume
A25: y in X;
now
reconsider b9=y as Element of AS by A25;
set M = Line(a9,b9);
A26: a9 in M by AFF_1:15;
A27: b9 in M by AFF_1:15;
assume
A28: y<>x;
then
A29: M is being_line by AFF_1:def 3;
A30: M c= X by A1,A14,A25,A28,Th19;
A31: now
assume not M // Q;
then consider q such that
A32: q in M and
A33: q in Q by A1,A9,A7,A29,A30,Th22;
M = Line(a9,q) by A12,A29,A26,A32,A33,AFF_1:57;
then M c= Y by A2,A8,A12,A13,A33,Th19;
hence y in Y by A27;
end;
now
assume M // Q;
then M c= Y by A2,A8,A13,A26,Th23;
hence y in Y by A27;
end;
hence y in Y by A31;
end;
hence y in Y by A11,XBOOLE_0:def 4;
end;
hence thesis by A15;
end;
hence contradiction by A5,TARSKI:2;
end;
Q c= Z by A7,A8,XBOOLE_1:19;
hence thesis by A9,A10,XBOOLE_0:def 10;
end;
theorem Th25:
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
proof
assume that
A1: X is being_plane & Y is being_plane and
A2: a in X & b in X and
A3: c in X and
A4: a in Y & b in Y and
A5: c in Y and
A6: not LIN a,b,c;
assume
A7: not thesis;
a<>b by A6,AFF_1:7;
then
A8: X /\ Y is being_line by A1,A2,A4,A7,Th24;
A9: c in X /\ Y by A3,A5,XBOOLE_0:def 4;
a in X /\ Y & b in X /\ Y by A2,A4,XBOOLE_0:def 4;
hence contradiction by A6,A8,A9,AFF_1:21;
end;
Lm7: M is being_line & a in M & b in M & a<>b & not c in M implies not LIN a,b
,c
proof
assume
A1: M is being_line & a in M & b in M & a<>b & not c in M;
assume not thesis;
then ex N st N is being_line & a in N & b in N & c in N by AFF_1:21;
hence contradiction by A1,AFF_1:18;
end;
theorem Th26:
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
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: M is being_line and
A4: N is being_line and
A5: M c= X & N c= X and
A6: M c= Y & N c= Y and
A7: M<>N;
consider a,b such that
A8: a in M and
A9: b in M and
A10: a<>b by A3,AFF_1:19;
A11: now
given q such that
A12: q in M and
A13: q in N;
consider p such that
A14: q<>p and
A15: p in N by A4,AFF_1:20;
A16: not p in M by A3,A4,A7,A12,A13,A14,A15,AFF_1:18;
A17: now
assume b<>q;
then not LIN b,q,p by A3,A9,A12,A16,Lm7;
hence thesis by A1,A2,A5,A6,A9,A12,A15,Th25;
end;
now
assume a<>q;
then not LIN a,q,p by A3,A8,A12,A16,Lm7;
hence thesis by A1,A2,A5,A6,A8,A12,A15,Th25;
end;
hence thesis by A10,A17;
end;
consider c,d such that
A18: c in N and
d in N and
c <>d by A4,AFF_1:19;
now
assume M // N;
then not c in M by A7,A18,AFF_1:45;
then not LIN a,b,c by A3,A8,A9,A10,Lm7;
hence thesis by A1,A2,A5,A6,A8,A9,A18,Th25;
end;
hence thesis by A1,A3,A4,A5,A11,Th22;
end;
definition
let AS,a,K such that
A1: K is being_line;
func a*K -> Subset of AS means
:Def3:
a in it & K // it;
existence by A1,AFF_1:49;
uniqueness by AFF_1:50;
end;
theorem Th27:
A is being_line implies a*A is being_line
proof
set M = a*A;
assume A is being_line;
then A // M by Def3;
hence thesis by AFF_1:36;
end;
theorem Th28:
X is being_plane & M is being_line & a in X & M c= X implies a*M c= X
proof
assume that
A1: X is being_plane and
A2: M is being_line and
A3: a in X & M c= X;
set N = a*M;
a in N & M // N by A2,Def3;
hence thesis by A1,A3,Th23;
end;
theorem Th29:
X is being_plane & a in X & b in X & c in X & a,b // c,d & a<>b
implies d in X
proof
assume that
A1: X is being_plane & a in X & b in X & c in X and
A2: a,b // c,d and
A3: a<>b;
set M=Line(a,b), N=c*M;
A4: M is being_line by A3,AFF_1:def 3;
then
A5: N c= X by A1,A3,Th19,Th28;
A6: a in M & b in M by AFF_1:15;
c in N & M // N by A4,Def3;
then d in N by A2,A3,A6,Th7;
hence thesis by A5;
end;
theorem
A is being_line implies ( a in A iff a*A = A )
proof
assume
A1: A is being_line;
now
assume
A2: a in A;
A // A by A1,AFF_1:41;
hence a*A = A by A1,A2,Def3;
end;
hence thesis by A1,Def3;
end;
theorem Th31:
A is being_line implies a*A = a*(q*A)
proof
assume
A1: A is being_line;
then A // q*A & A // a*A by Def3;
then
A2: a*A // q*A by AFF_1:44;
A3: q*A is being_line by A1,Th27;
then
A4: a in a*(q*A) by Def3;
q*A // a*(q*A) by A3,Def3;
then
A5: a*A // a*(q*A) by A2,AFF_1:44;
a in a*A by A1,Def3;
hence thesis by A4,A5,AFF_1:45;
end;
Lm8: A is being_line & a in A implies a*A=A
proof
assume that
A1: A is being_line and
A2: a in A;
A // A by A1,AFF_1:41;
hence thesis by A1,A2,Def3;
end;
theorem Th32:
K // M implies a*K=a*M
proof
assume
A1: K // M;
then
A2: K is being_line by AFF_1:36;
then K // a*K by Def3;
then
A3: a*K // M by A1,AFF_1:44;
A4: M is being_line by A1,AFF_1:36;
then
A5: a in a*M by Def3;
M // a*M by A4,Def3;
then
A6: a*K // a*M by A3,AFF_1:44;
a in a*K by A2,Def3;
hence thesis by A5,A6,AFF_1:45;
end;
definition
let AS,X,Y;
pred X '||' Y means
for a,A st a in Y & A is being_line & A c= X holds a*A c= Y;
end;
theorem Th33:
X c= Y & ( X is being_line & Y is being_line or X is being_plane
& Y is being_plane ) implies X=Y
proof
assume that
A1: X c= Y and
A2: X is being_line & Y is being_line or X is being_plane & Y is being_plane;
A3: now
assume that
A4: X is being_plane and
A5: Y is being_plane;
consider K,P such that
A6: K is being_line and
A7: P is being_line and
A8: not K // P and
A9: X=Plane(K,P) by A4;
consider a,b such that
A10: a in P and
b in P and
a<>b by A7,AFF_1:19;
set M=a*K;
A11: K // M by A6,Def3;
A12: P c= X by A6,A9,Th14;
then
A13: P c= Y by A1;
A14: M is being_line by A6,Th27;
a in M & P c= Plane(K,P) by A6,Def3,Th14;
then
A15: M c= X by A9,A10,A11,Lm4;
then M c= Y by A1;
hence thesis by A4,A5,A7,A8,A11,A14,A12,A13,A15,Th26;
end;
now
assume that
A16: X is being_line and
A17: Y is being_line;
consider a,b such that
A18: a<>b and
A19: X=Line(a,b) by A16,AFF_1:def 3;
a in X & b in X by A19,AFF_1:15;
hence thesis by A1,A17,A18,A19,AFF_1:57;
end;
hence thesis by A2,A3;
end;
theorem Th34:
X is being_plane implies ex a,b,c st a in X & b in X & c in X & not LIN a,b,c
proof
assume X is being_plane;
then consider K,P such that
A1: K is being_line and
A2: P is being_line and
A3: not K // P and
A4: X = Plane(K,P);
consider a,b such that
A5: a in P and
A6: b in P and
A7: a<>b by A2,AFF_1:19;
set Q = a*K;
consider c such that
A8: a<>c and
A9: c in Q by A1,Th27,AFF_1:20;
take a,b,c;
A10: P c= Plane(K,P) by A1,Th14;
hence a in X & b in X by A4,A5,A6;
A11: K // Q & a in Q by A1,Def3;
then Q c= Plane(K,P) by A5,A10,Lm4;
hence c in X by A4,A9;
A12: Q is being_line by A1,Th27;
thus not LIN a,b,c
proof
assume LIN a,b,c;
then c in P by A2,A5,A6,A7,AFF_1:25;
hence contradiction by A2,A3,A5,A11,A12,A8,A9,AFF_1:18;
end;
end;
Lm9: X is being_plane implies ex b,c st b in X & c in X & not LIN a,b,c
proof
assume X is being_plane;
then consider p,q,r such that
A1: p in X & q in X and
A2: r in X and
A3: not LIN p,q,r by Th34;
now
assume
A4: LIN a,r,p & LIN a,r,q;
take b=p,c =q;
thus b in X & c in X by A1;
LIN a,r,r by AFF_1:7;
then a=r by A3,A4,AFF_1:8;
hence not LIN a,b,c by A3,AFF_1:6;
end;
hence thesis by A1,A2;
end;
theorem
M is being_line & X is being_plane implies ex q st q in X & not q in M
proof
assume that
A1: M is being_line and
A2: X is being_plane;
consider a,b,c such that
A3: a in X & b in X and
A4: c in X and
A5: not LIN a,b,c by A2,Th34;
assume
A6: not ex q st q in X & not q in M;
then
A7: c in M by A4;
a in M & b in M by A6,A3;
hence contradiction by A1,A5,A7,AFF_1:21;
end;
theorem Th36:
for a,A st A is being_line ex X st a in X & A c= X & X is being_plane
proof
let a,A;
assume
A1: A is being_line;
then consider p,q such that
A2: p in A and
q in A and
p<>q by AFF_1:19;
A3: now
consider b such that
A4: not b in A by A1,Th12;
consider P such that
A5: a in P & b in P and
A6: P is being_line by Th11;
set X=Plane(P,A);
A7: A c= X by A6,Th14;
assume
A8: a in A;
then not P // A by A4,A5,AFF_1:45;
then X is being_plane by A1,A6;
hence thesis by A8,A7;
end;
now
consider P such that
A9: a in P and
A10: p in P and
A11: P is being_line by Th11;
set X=Plane(P,A);
A c= X by A11,Th14;
then
A12: P c= X by A2,A10,A11,Lm4,AFF_1:41;
assume not a in A;
then not P // A by A2,A9,A10,AFF_1:45;
then X is being_plane by A1,A11;
hence thesis by A9,A11,A12,Th14;
end;
hence thesis by A3;
end;
theorem Th37:
ex X st a in X & b in X & c in X & X is being_plane
proof
consider A such that
A1: a in A & b in A and
A2: A is being_line by Th11;
ex X st c in X & A c= X & X is being_plane by A2,Th36;
hence thesis by A1;
end;
theorem Th38:
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
proof
assume that
A1: q in M and
A2: q in N and
A3: M is being_line and
A4: N is being_line;
consider a such that
A5: a<>q and
A6: a in N by A4,AFF_1:20;
A7: ex X st a in X & M c= X & X is being_plane by A3,Th36;
N=Line(q,a) by A2,A4,A5,A6,AFF_1:24;
hence thesis by A1,A5,A7,Th19;
end;
theorem Th39:
M // N implies ex X st M c= X & N c= X & X is being_plane
proof
assume
A1: M // N;
then N is being_line by AFF_1:36;
then consider a,b such that
A2: a in N and
b in N and
a<>b by AFF_1:19;
A3: M is being_line by A1,AFF_1:36;
then
A4: ex X st a in X & M c= X & X is being_plane by Th36;
N=a*M by A1,A3,A2,Def3;
hence thesis by A3,A4,Th28;
end;
theorem
M is being_line & N is being_line implies (M // N iff M '||' N)
proof
assume that
A1: M is being_line and
A2: N is being_line;
A3: now
assume
A4: M // N;
now
let a,A;
assume that
A5: a in N and
A6: A is being_line & A c= M;
N=a*M by A1,A4,A5,Def3;
hence a*A c= N by A1,A6,Th33;
end;
hence M '||' N;
end;
now
consider a,b such that
A7: a in N and
b in N and
a<>b by A2,AFF_1:19;
A8: a*M is being_line by A1,Th27;
assume M '||' N;
then a*M c= N by A1,A7;
then a*M=N by A2,A8,Th33;
hence M // N by A1,Def3;
end;
hence thesis by A3;
end;
theorem Th41:
M is being_line & X is being_plane implies (M '||' X iff ex N st
N c= X & (M // N or N // M) )
proof
assume that
A1: M is being_line and
A2: X is being_plane;
A3: now
given N such that
A4: N c= X and
A5: M // N or N // M;
now
let a,A;
assume that
A6: a in X and
A7: A is being_line and
A8: A c= M;
A=M by A1,A7,A8,Th33;
then M // a*A by A7,Def3;
then
A9: N // a*A by A5,AFF_1:44;
a in a*A by A7,Def3;
hence a*A c= X by A2,A4,A6,A9,Th23;
end;
hence M '||' X;
end;
now
consider a,b,c such that
A10: a in X and
b in X and
c in X and
not LIN a,b,c by A2,Th34;
assume
A11: M '||' X;
take N=a*M;
thus N c= X by A1,A11,A10;
thus M // N or N // M by A1,Def3;
end;
hence thesis by A3;
end;
theorem
M is being_line & X is being_plane & M c= X implies M '||' X
proof
assume that
A1: M is being_line and
A2: X is being_plane & M c= X;
M // M by A1,AFF_1:41;
hence thesis by A1,A2,Th41;
end;
theorem
A is being_line & X is being_plane & a in A & a in X & A '||' X
implies A c= X
proof
assume that
A1: A is being_line and
A2: X is being_plane and
A3: a in A and
A4: a in X and
A5: A '||' X;
consider N such that
A6: N c= X and
A7: A // N or N // A by A1,A2,A5,Th41;
A8: N is being_line by A7,AFF_1:36;
A=a*A by A1,A3,Lm8
.= a*N by A7,Th32;
hence thesis by A2,A4,A6,A8,Th28;
end;
definition
let AS,K,M,N;
pred K,M,N is_coplanar means
ex X st K c= X & M c= X & N c= X & X is being_plane;
end;
theorem
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
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
proof
assume that
A1: M is being_line & N is being_line and
A2: M,N,K is_coplanar and
A3: M,N,A is_coplanar and
A4: M<>N;
consider X such that
A5: M c= X and
A6: N c= X and
A7: K c= X and
A8: X is being_plane by A2;
ex Y st M c= Y & N c= Y & A c= Y & Y is being_plane by A3;
then A c= X by A1,A4,A5,A6,A8,Th26;
hence thesis by A5,A7,A8;
end;
theorem Th46:
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)
by Th26;
theorem Th47:
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
proof
assume q in K & q in M & K is being_line & M is being_line;
then ex X st K c= X & M c= X & X is being_plane by Th38;
hence thesis;
end;
theorem Th48:
AS is not AffinPlane & X is being_plane implies ex q st not q in X
proof
assume that
A1: AS is not AffinPlane and
A2: X is being_plane;
assume
A3: not ex q st not q in X;
for a,b,c,d st not a,b // c,d ex q st a,b // a,q & c,d // c,q
proof
let a,b,c,d;
set M=Line(a,b),N=Line(c,d);
A4: a in M & b in M by AFF_1:15;
A5: c in N & d in N by AFF_1:15;
assume
A6: not a,b // c,d;
then
A7: a<>b by AFF_1:3;
then
A8: M is being_line by AFF_1:def 3;
A9: c <>d by A6,AFF_1:3;
then
A10: N is being_line by AFF_1:def 3;
c in X & d in X by A3;
then
A11: N c= X by A2,A9,Th19;
a in X & b in X by A3;
then M c= X by A2,A7,Th19;
then consider q such that
A12: q in M and
A13: q in N by A2,A6,A11,A8,A10,A4,A5,Th22,AFF_1:39;
LIN c,d,q by A10,A5,A13,AFF_1:21;
then
A14: c,d // c, q by AFF_1:def 1;
LIN a,b,q by A8,A4,A12,AFF_1:21;
then a,b // a,q by AFF_1:def 1;
hence thesis by A14;
end;
hence contradiction by A1,DIRAF:def 7;
end;
Lm10: 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
implies b,c // b9,c9
proof
assume that
A1: q in A and
A2: q in P and
A3: q in C and
A4: not A,P,C is_coplanar and
A5: q<>a and
A6: q<>b and
A7: q<>c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A<>P and
A18: A<>C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9;
A21: c <>a by A1,A3,A5,A8,A12,A14,A16,A18,AFF_1:18;
A22: P<>C by A1,A2,A4,A14,A15,Th47;
then
A23: b<>c by A2,A3,A6,A10,A12,A15,A16,AFF_1:18;
consider X such that
A24: P c= X & C c= X and
A25: X is being_plane by A2,A3,A15,A16,Th38;
consider Y such that
A26: A c= Y and
A27: C c= Y and
A28: Y is being_plane by A1,A3,A14,A16,Th38;
A29: a<>b by A1,A2,A5,A8,A10,A14,A15,A17,AFF_1:18;
A30: now
assume
A31: q<>a9;
then
A32: q<>c9 by A1,A3,A5,A7,A8,A9,A12,A14,A16,A18,A20,Th8;
A33: now
set BC=Line(b,c),BC9=Line(b9,c9),AB=Line(a,b),AB9=Line(a9,b9), AC=Line(a
,c),AC9=Line(a9,c9);
assume
A34: a<>a9;
assume
A35: not b,c // b9,c9;
A36: b9 in BC9 & c9 in BC9 by AFF_1:15;
A37: BC c= X by A10,A12,A24,A25,A23,Th19;
A38: c in BC by AFF_1:15;
A39: BC is being_line & b in BC by A23,AFF_1:15,def 3;
A40: c9<>b9 by A2,A3,A11,A13,A15,A16,A22,A32,AFF_1:18;
then
A41: BC9 is being_line by AFF_1:def 3;
BC9 c= X by A11,A13,A24,A25,A40,Th19;
then consider p such that
A42: p in BC and
A43: p in BC9 by A25,A35,A41,A39,A38,A36,A37,Th22,AFF_1:39;
A44: a9 in AC9 by AFF_1:15;
LIN c9,b9,p by A41,A36,A43,AFF_1:21;
then consider y such that
A45: LIN c9,a9,y and
A46: b9,a9 // p,y by A40,Th1;
A47: c in AC by AFF_1:15;
LIN c,b,p by A39,A38,A42,AFF_1:21;
then consider x such that
A48: LIN c,a,x and
A49: b,a // p,x by A23,Th1;
A50: a in AB by AFF_1:15;
A51: AC is being_line & a in AC by A21,AFF_1:15,def 3;
then
A52: x in AC by A21,A47,A48,AFF_1:25;
set K = p*AB;
A53: b in AB by AFF_1:15;
A54: AB is being_line by A29,AFF_1:def 3;
then
A55: AB // K by Def3;
A56: p in K by A54,Def3;
p,x // a,b by A49,AFF_1:4;
then p,x // AB by A29,AFF_1:def 4;
then p,x // K by A55,Th3;
then
A57: x in K by A56,Th2;
A58: a9<>b9 by A1,A2,A9,A11,A14,A15,A17,A31,AFF_1:18;
p,y // a9,b9 by A46,AFF_1:4;
then
A59: p,y // AB9 by A58,AFF_1:def 4;
AB // AB9 by A19,A29,A58,AFF_1:37;
then AB9 // K by A55,AFF_1:44;
then p,y // K by A59,Th3;
then
A60: y in K by A56,Th2;
A61: AC c= Y by A8,A12,A26,A27,A28,A21,Th19;
A62: c9 in AC9 by AFF_1:15;
A63: a9<>c9 by A1,A3,A9,A13,A14,A16,A18,A31,AFF_1:18;
then AC9 is being_line by AFF_1:def 3;
then
A64: y in AC9 by A63,A44,A62,A45,AFF_1:25;
A65: AC9 c= Y by A9,A13,A26,A27,A28,A63,Th19;
A66: now
assume
A67: x<>y;
then K=Line(x,y) by A54,A57,A60,Th27,AFF_1:57;
then K c= Y by A28,A61,A65,A52,A64,A67,Th19;
then
A68: AB c= Y by A8,A26,A28,A50,A55,Th23;
P=Line(q,b) by A2,A6,A10,A15,AFF_1:57;
then P c= Y by A1,A6,A26,A28,A53,A68,Th19;
hence contradiction by A4,A26,A27,A28;
end;
A69: AC // AC9 by A20,A21,A63,AFF_1:37;
now
assume x=y;
then a9 in AC by A44,A69,A52,A64,AFF_1:45;
then c in A by A8,A9,A14,A34,A51,A47,AFF_1:18;
hence contradiction by A1,A3,A7,A12,A14,A16,A18,AFF_1:18;
end;
hence contradiction by A66;
end;
now
assume a=a9;
then b=b9 & c =c9 by A1,A2,A3,A5,A6,A7,A8,A10,A11,A12,A13,A14,A15,A16,A17
,A18,A19,A20,Th9;
hence thesis by AFF_1:2;
end;
hence thesis by A33;
end;
now
assume q=a9;
then q=b9 & q=c9 by A1,A2,A3,A5,A6,A7,A8,A10,A11,A12,A13,A14,A15,A16,A17
,A18,A19,A20,Th8;
hence thesis by AFF_1:3;
end;
hence thesis by A30;
end;
theorem Th49:
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
proof
assume that
A1: AS is not AffinPlane and
A2: q in A and
A3: q in P and
A4: q in C and
A5: q<>a and
A6: q<>b and
A7: q<>c and
A8: a in A & a9 in A and
A9: b in P & b9 in P and
A10: c in C & c9 in C and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A<>P and
A15: A<>C and
A16: a,b // a9,b9 and
A17: a,c // a9,c9;
now
assume A,P,C is_coplanar;
then consider X such that
A18: A c= X and
A19: P c= X and
A20: C c= X and
A21: X is being_plane;
consider d such that
A22: not d in X by A1,A21,Th48;
LIN q,a,a9 by A2,A8,A11,AFF_1:21;
then consider d9 such that
A23: LIN q,d,d9 and
A24: a,d // a9,d9 by A5,Th1;
set K=Line(q,d);
A25: d in K by AFF_1:15;
then
A26: not K c= X by A22;
A27: q<>d by A2,A18,A22;
then
A28: q in K & K is being_line by AFF_1:15,def 3;
then
A29: d9 in K by A25,A27,A23,AFF_1:25;
now
assume
A30: P<>C;
A31: not K,P,C is_coplanar
proof
assume K,P,C is_coplanar;
then P,C,K is_coplanar;
hence contradiction by A12,A13,A19,A20,A21,A26,A30,Th46;
end;
A32: K<>A by A18,A22,A25;
not A,K,P is_coplanar
proof
assume A,K,P is_coplanar;
then A,P,K is_coplanar;
hence contradiction by A11,A12,A14,A18,A19,A21,A26,Th46;
end;
then
A33: d,b // d9,b9 by A2,A3,A5,A6,A8,A9,A11,A12,A14,A16,A25,A27,A28,A24,A29,A32
,Lm10;
A34: K<>P & K<>C by A19,A20,A22,A25;
not A,K,C is_coplanar
proof
assume A,K,C is_coplanar;
then A,C,K is_coplanar;
hence contradiction by A11,A13,A15,A18,A20,A21,A26,Th46;
end;
then
d,c // d9,c9 by A2,A4,A5,A7,A8,A10,A11,A13,A15,A17,A25,A27,A28,A24,A29
,A32,Lm10;
hence thesis by A3,A4,A6,A7,A9,A10,A12,A13,A25,A27,A28,A29,A34,A31,A33
,Lm10;
end;
hence thesis by A9,A10,A12,AFF_1:51;
end;
hence thesis by A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,Lm10;
end;
theorem
AS is not AffinPlane implies AS is Desarguesian
proof
assume AS is not AffinPlane;
then
for A,P,C,q,a,b,c,a9,b9,c9 holds 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 by Th49;
hence thesis by AFF_2:def 4;
end;
Lm11: 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 implies b,c // b9,c9
proof
assume that
A1: A // P and
A2: A // C and
A3: not A,P,C is_coplanar and
A4: a in A and
A5: a9 in A and
A6: b in P and
A7: b9 in P and
A8: c in C and
A9: c9 in C and
A10: A is being_line and
A11: A<>P and
A12: A<>C and
A13: a,b // a9,b9 and
A14: a,c // a9,c9;
A15: c <>a by A2,A4,A8,A12,AFF_1:45;
A16: P // C by A1,A2,AFF_1:44;
then consider X such that
A17: P c= X & C c= X and
A18: X is being_plane by Th39;
consider Y such that
A19: A c= Y and
A20: C c= Y and
A21: Y is being_plane by A2,Th39;
A22: P<>C by A3,A19,A20,A21;
then
A23: b<>c by A6,A8,A16,AFF_1:45;
A24: a<>b by A1,A4,A6,A11,AFF_1:45;
A25: now
set BC=Line(b,c),BC9=Line(b9,c9),AB=Line(a,b),AB9=Line(a9,b9), AC=Line(a,c
),AC9=Line(a9,c9);
assume
A26: a<>a9;
assume
A27: not b,c // b9,c9;
A28: b9 in BC9 & c9 in BC9 by AFF_1:15;
A29: BC c= X by A6,A8,A17,A18,A23,Th19;
A30: c in BC by AFF_1:15;
A31: BC is being_line & b in BC by A23,AFF_1:15,def 3;
A32: c9<>b9 by A7,A9,A16,A22,AFF_1:45;
then
A33: BC9 is being_line by AFF_1:def 3;
BC9 c= X by A7,A9,A17,A18,A32,Th19;
then consider p such that
A34: p in BC and
A35: p in BC9 by A18,A27,A33,A31,A30,A28,A29,Th22,AFF_1:39;
A36: a9 in AC9 by AFF_1:15;
LIN c9,b9,p by A33,A28,A35,AFF_1:21;
then consider y such that
A37: LIN c9,a9,y and
A38: b9,a9 // p,y by A32,Th1;
A39: c in AC by AFF_1:15;
LIN c,b,p by A31,A30,A34,AFF_1:21;
then consider x such that
A40: LIN c,a,x and
A41: b,a // p,x by A23,Th1;
A42: a in AB by AFF_1:15;
A43: AC is being_line & a in AC by A15,AFF_1:15,def 3;
then
A44: x in AC by A15,A39,A40,AFF_1:25;
set K = p*AB;
A45: b in AB by AFF_1:15;
A46: AB is being_line by A24,AFF_1:def 3;
then
A47: AB // K by Def3;
A48: p in K by A46,Def3;
p,x // a,b by A41,AFF_1:4;
then p,x // AB by A24,AFF_1:def 4;
then p,x // K by A47,Th3;
then
A49: x in K by A48,Th2;
A50: a9<>b9 by A1,A5,A7,A11,AFF_1:45;
p,y // a9,b9 by A38,AFF_1:4;
then
A51: p,y // AB9 by A50,AFF_1:def 4;
AB // AB9 by A13,A24,A50,AFF_1:37;
then AB9 // K by A47,AFF_1:44;
then p,y // K by A51,Th3;
then
A52: y in K by A48,Th2;
A53: AC c= Y by A4,A8,A19,A20,A21,A15,Th19;
A54: c9 in AC9 by AFF_1:15;
A55: a9<>c9 by A2,A5,A9,A12,AFF_1:45;
then AC9 is being_line by AFF_1:def 3;
then
A56: y in AC9 by A55,A36,A54,A37,AFF_1:25;
A57: AC9 c= Y by A5,A9,A19,A20,A21,A55,Th19;
A58: now
assume
A59: x<>y;
then K=Line(x,y) by A46,A49,A52,Th27,AFF_1:57;
then K c= Y by A21,A53,A57,A44,A56,A59,Th19;
then
A60: AB c= Y by A4,A19,A21,A42,A47,Th23;
P=b*A by A1,A6,A10,Def3;
then P c= Y by A10,A19,A21,A45,A60,Th28;
hence contradiction by A3,A19,A20,A21;
end;
A61: AC // AC9 by A14,A15,A55,AFF_1:37;
now
assume x=y;
then a9 in AC by A36,A61,A44,A56,AFF_1:45;
then c in A by A4,A5,A10,A26,A43,A39,AFF_1:18;
hence contradiction by A2,A8,A12,AFF_1:45;
end;
hence contradiction by A58;
end;
now
assume a=a9;
then b=b9 & c =c9 by A1,A2,A4,A6,A7,A8,A9,A11,A12,A13,A14,Th10;
hence thesis by AFF_1:2;
end;
hence thesis by A25;
end;
theorem Th51:
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
proof
assume that
A1: AS is not AffinPlane and
A2: A // P and
A3: A // C and
A4: a in A & a9 in A and
A5: b in P & b9 in P and
A6: c in C & c9 in C and
A7: A is being_line and
A8: P is being_line and
A9: C is being_line and
A10: A<>P and
A11: A<>C and
A12: a,b // a9,b9 and
A13: a,c // a9,c9;
now
assume A,P,C is_coplanar;
then consider X such that
A14: A c= X and
A15: P c= X and
A16: C c= X and
A17: X is being_plane;
consider d such that
A18: not d in X by A1,A17,Th48;
set K=d*A;
A19: d in K by A7,Def3;
then
A20: not K c= X by A18;
A21: A // K by A7,Def3;
ex d9 st d9 in K & a,d // a9,d9
proof
A22: now
assume
A23: a<>a9;
consider d9 such that
A24: a,a9 // d,d9 and
A25: a,d // a9,d9 by DIRAF:40;
d,d9 // a,a9 by A24,AFF_1:4;
then d,d9 // A by A4,A7,A23,AFF_1:27;
then d,d9 // K by A21,Th3;
then d9 in K by A19,Th2;
hence thesis by A25;
end;
now
assume
A26: a=a9;
take d9=d;
thus d9 in K by A7,Def3;
thus a,d // a9,d9 by A26,AFF_1:2;
end;
hence thesis by A22;
end;
then consider d9 such that
A27: d9 in K and
A28: a,d // a9,d9;
A29: K // P & K // C by A2,A3,A21,AFF_1:44;
now
assume
A30: P<>C;
A31: not K,P,C is_coplanar
proof
assume K,P,C is_coplanar;
then P,C,K is_coplanar;
hence contradiction by A8,A9,A15,A16,A17,A20,A30,Th46;
end;
A32: K<>A by A14,A18,A19;
not A,K,P is_coplanar
proof
assume A,K,P is_coplanar;
then A,P,K is_coplanar;
hence contradiction by A7,A8,A10,A14,A15,A17,A20,Th46;
end;
then
A33: d,b // d9,b9 by A2,A4,A5,A7,A10,A12,A19,A21,A27,A28,A32,Lm11;
A34: K<>P & K<>C by A15,A16,A18,A19;
not A,K,C is_coplanar
proof
assume A,K,C is_coplanar;
then A,C,K is_coplanar;
hence contradiction by A7,A9,A11,A14,A16,A17,A20,Th46;
end;
then d,c // d9,c9 by A3,A4,A6,A7,A11,A13,A19,A21,A27,A28,A32,Lm11;
hence thesis by A5,A6,A7,A19,A29,A27,A34,A31,A33,Lm11,Th27;
end;
hence thesis by A5,A6,A8,AFF_1:51;
end;
hence thesis by A2,A3,A4,A5,A6,A7,A10,A11,A12,A13,Lm11;
end;
theorem
AS is not AffinPlane implies AS is translational
proof
assume AS is not AffinPlane;
then
for A,P,C,a,b,c,a9,b9,c9 holds 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 by
Th51;
hence thesis by AFF_2:def 11;
end;
theorem Th53:
AS is AffinPlane & not LIN a,b,c implies ex c9 st a,c // a9,c9 & b,c // b9,c9
proof
assume that
A1: AS is AffinPlane and
A2: not LIN a,b,c;
consider C such that
A3: b in C & c in C and
A4: C is being_line by Th11;
consider N such that
A5: b9 in N and
A6: C // N by A4,AFF_1:49;
A7: N is being_line by A6,AFF_1:36;
consider P such that
A8: a in P and
A9: c in P and
A10: P is being_line by Th11;
consider M such that
A11: a9 in M and
A12: P // M by A10,AFF_1:49;
A13: not M // N
proof
assume M // N;
then N // P by A12,AFF_1:44;
then C // P by A6,AFF_1:44;
then b in P by A3,A9,AFF_1:45;
hence contradiction by A2,A8,A9,A10,AFF_1:21;
end;
M is being_line by A12,AFF_1:36;
then consider c9 such that
A14: c9 in M and
A15: c9 in N by A1,A7,A13,AFF_1:58;
A16: b,c // b9,c9 by A3,A5,A6,A15,AFF_1:39;
a,c // a9,c9 by A8,A9,A11,A12,A14,AFF_1:39;
hence thesis by A16;
end;
Lm12: 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 implies ex c9 st a,c // a9,c9 & b,c // b9,c9
proof
assume that
A1: not LIN a,b,c and
A2: a,b // a9,b9 and
A3: a in X and
A4: b in X and
A5: c in X and
A6: X is being_plane and
A7: a9 in X;
set C=Line(b,c),P=Line(a,c),P9=a9*P,C9=b9*C;
A8: b<>c by A1,AFF_1:7;
then
A9: C is being_line by AFF_1:def 3;
then
A10: C // C9 by Def3;
a<>b by A1,AFF_1:7;
then b9 in X by A2,A3,A4,A6,A7,Th29;
then
A11: C9 c= X by A4,A5,A6,A8,A9,Th19,Th28;
A12: c in P by AFF_1:15;
A13: C9 is being_line by A9,Th27;
A14: a in P by AFF_1:15;
A15: c <>a by A1,AFF_1:7;
then
A16: P is being_line by AFF_1:def 3;
then
A17: P9 is being_line by Th27;
A18: b in C & c in C by AFF_1:15;
A19: P // P9 by A16,Def3;
A20: not C9 // P9
proof
assume C9 // P9;
then C9 // P by A19,AFF_1:44;
then C // P by A10,AFF_1:44;
then b in P by A12,A18,AFF_1:45;
hence contradiction by A1,A14,A12,A16,AFF_1:21;
end;
P9 c= X by A3,A5,A6,A7,A15,A16,Th19,Th28;
then consider c9 such that
A21: c9 in C9 and
A22: c9 in P9 by A6,A17,A13,A20,A11,Th22;
b9 in C9 by A9,Def3;
then
A23: b,c // b9,c9 by A18,A10,A21,AFF_1:39;
a9 in P9 by A16,Def3;
then a,c // a9,c9 by A14,A12,A19,A22,AFF_1:39;
hence thesis by A23;
end;
theorem Th54:
not LIN a,b,c & a9<>b9 & a,b // a9,b9 implies ex c9 st a,c // a9
,c9 & b,c // b9,c9
proof
assume that
A1: not LIN a,b,c and
A2: a9<>b9 and
A3: a,b // a9,b9;
now
consider X such that
A4: a in X and
A5: b in X and
A6: c in X and
A7: X is being_plane by Th37;
assume
A8: AS is not AffinPlane;
now
set A=Line(a,a9),P=Line(b,b9);
set AB=Line(a,b),AB9=Line(a9,b9);
A9: a in AB by AFF_1:15;
assume
A10: not a9 in X;
then
A11: A is being_line by A4,AFF_1:def 3;
A12: a<>b by A1,AFF_1:7;
then
A13: AB c= X by A4,A5,A7,Th19;
A14: AB // AB9 by A2,A3,A12,AFF_1:37;
then consider Y such that
A15: AB c= Y and
A16: AB9 c= Y and
A17: Y is being_plane by Th39;
A18: b in AB by AFF_1:15;
A19: a9 in AB9 by AFF_1:15;
then
A20: A c= Y by A4,A10,A9,A15,A16,A17,Th19;
A21: b9 in AB9 by AFF_1:15;
A22: not b9 in X
proof
assume b9 in X;
then AB9 c= X by A7,A21,A14,A13,Th23;
hence contradiction by A10,A19;
end;
then
A23: P is being_line by A5,AFF_1:def 3;
A24: b9 in P by AFF_1:15;
A25: a in A by AFF_1:15;
A26: a<>c by A1,AFF_1:7;
A27: b in P by AFF_1:15;
A28: a9 in A by AFF_1:15;
A29: AB is being_line by A12,AFF_1:def 3;
A30: A<>P
proof
assume A=P;
then A=AB by A12,A9,A18,A29,A11,A25,A27,AFF_1:18;
hence contradiction by A10,A13,A28;
end;
A31: now
set C=c*A;
assume
A32: A // P;
A33: c in C by A11,Def3;
A34: A<>C
proof
assume A=C;
then A=Line(a,c) by A26,A11,A25,A33,AFF_1:57;
then A c= X by A4,A6,A7,A26,Th19;
hence contradiction by A10,A28;
end;
A35: A // C by A11,Def3;
then consider c9 such that
A36: c9 in C and
A37: a,c // a9,c9 by A25,A28,A33,Lm2;
C is being_line by A11,Th27;
then b,c // b9,c9 by A3,A8,A11,A23,A25,A28,A27,A24,A30,A32,A33,A35,A36
,A37,A34,Th51;
hence thesis by A37;
end;
A38: a9 in Y by A19,A16;
A39: now
given q such that
A40: q in A and
A41: q in P;
A42: q<>a
proof
assume q=a;
then AB=P by A12,A9,A18,A29,A23,A27,A41,AFF_1:18;
hence contradiction by A13,A22,A24;
end;
A43: q<>b
proof
assume q=b;
then AB=A by A12,A9,A18,A29,A11,A25,A40,AFF_1:18;
hence contradiction by A10,A13,A28;
end;
set C=Line(q,c);
A44: c in C by AFF_1:15;
A45: A<>C
proof
assume A=C;
then A=Line(a,c) by A26,A11,A25,A44,AFF_1:57;
then A c= X by A4,A6,A7,A26,Th19;
hence contradiction by A10,A28;
end;
LIN q,a,a9 by A11,A25,A28,A40,AFF_1:21;
then consider c9 such that
A46: LIN q,c,c9 and
A47: a,c // a9,c9 by A42,Th1;
A48: q<>c by A1,A4,A5,A6,A7,A10,A9,A18,A15,A17,A38,A20,A40,Th25;
then
A49: q in C & C is being_line by AFF_1:15,def 3;
then c9 in C by A48,A44,A46,AFF_1:25;
then
b,c // b9,c9 by A3,A8,A11,A23,A25,A28,A27,A24,A30,A40,A41,A42,A43,A48
,A44,A49,A47,A45,Th49;
hence thesis by A47;
end;
P c= Y by A5,A18,A21,A22,A15,A16,A17,Th19;
hence thesis by A17,A11,A23,A20,A31,A39,Th22;
end;
hence thesis by A1,A3,A4,A5,A6,A7,Lm12;
end;
hence thesis by A1,Th53;
end;
theorem Th55:
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) )
proof
assume that
A1: X is being_plane and
A2: Y is being_plane;
A3: now
given A,P,M,N such that
A4: not A // P and
A5: A c= X and
A6: P c= X and
A7: M c= Y and
A8: N c= Y and
A9: A // M or M // A and
A10: P // N or N // P;
A11: M is being_line by A9,AFF_1:36;
A12: not M // N
proof
assume M // N;
then P // M by A10,AFF_1:44;
hence contradiction by A4,A9,AFF_1:44;
end;
N is being_line by A10,AFF_1:36;
then consider q such that
A13: q in M and
A14: q in N by A2,A7,A8,A11,A12,Th22;
A15: A is being_line by A9,AFF_1:36;
A16: P is being_line by A10,AFF_1:36;
then consider p such that
A17: p in A and
A18: p in P by A1,A4,A5,A6,A15,Th22;
now
let a,Z;
assume that
A19: a in Y and
A20: Z is being_line and
A21: Z c= X;
A22: a in a*Z by A20,Def3;
A23: Z // a*Z by A20,Def3;
A24: now
assume Z // P;
then Z // N by A10,AFF_1:44;
then a*Z // N by A23,AFF_1:44;
hence a*Z c= Y by A2,A8,A19,A22,Th23;
end;
A25: now
assume that
A26: not Z // A and
A27: not Z // P;
consider b such that
A28: p<>b and
A29: b in A by A15,AFF_1:20;
set Z1= b*Z;
A30: Z1 is being_line by A20,Th27;
A31: not Z1 // P
proof
assume
A32: Z1 // P;
Z // b*Z by A20,Def3;
hence contradiction by A27,A32,AFF_1:44;
end;
A33: Z // Z1 by A20,Def3;
Z1 c= X by A1,A5,A20,A21,A29,Th28;
then consider c such that
A34: c in Z1 and
A35: c in P by A1,A6,A16,A30,A31,Th22;
A36: b in Z1 by A20,Def3;
then
A37: p<>c by A15,A17,A26,A28,A29,A30,A33,A34,AFF_1:18;
A38: A<>P by A4,A15,AFF_1:41;
A39: not LIN p,b,c
proof
assume LIN p,b,c;
then c in A by A15,A17,A28,A29,AFF_1:25;
hence contradiction by A15,A16,A17,A18,A35,A37,A38,AFF_1:18;
end;
then
A40: b<>c by AFF_1:7;
consider b9 such that
A41: q<>b9 and
A42: b9 in M by A11,AFF_1:20;
p,b // q,b9 by A9,A17,A13,A29,A42,AFF_1:39;
then consider c9 such that
A43: p,c // q,c9 and
A44: b,c // b9,c9 by A41,A39,Th54;
set Z2=Line(b9,c9);
A45: b9 in Z2 & c9 in Z2 by AFF_1:15;
A46: b9<>c9
proof
assume
A47: b9=c9;
q,b9 // M by A11,A13,A42,AFF_1:52;
then p,c // M by A41,A43,A47,Th4;
then p,c // A by A9,Th3;
then c in A by A17,Th2;
hence contradiction by A15,A16,A17,A18,A35,A37,A38,AFF_1:18;
end;
then Z2 is being_line by AFF_1:def 3;
then Z1 // Z2 by A30,A36,A34,A44,A40,A46,A45,AFF_1:38;
then Z // Z2 by A33,AFF_1:44;
then
A48: a*Z // Z2 by A23,AFF_1:44;
c9 in N by A10,A18,A14,A35,A37,A43,Th7;
then Z2 c= Y by A2,A7,A8,A42,A46,Th19;
hence a*Z c= Y by A2,A19,A22,A48,Th23;
end;
now
assume Z // A;
then Z // M by A9,AFF_1:44;
then a*Z // M by A23,AFF_1:44;
hence a*Z c= Y by A2,A7,A19,A22,Th23;
end;
hence a*Z c= Y by A24,A25;
end;
hence X '||' Y;
end;
now
consider a9,b9,c9 such that
A49: a9 in Y and
b9 in Y and
c9 in Y and
not LIN a9,b9,c9 by A2,Th34;
assume
A50: X '||' Y;
consider a,b,c such that
A51: a in X and
A52: b in X and
A53: c in X and
A54: not LIN a,b,c by A1,Th34;
set A=Line(a,b),P=Line(a,c);
A55: b in A & c in P by AFF_1:15;
A56: a<>c by A54,AFF_1:7;
then
A57: P c= X by A1,A51,A53,Th19;
take A,P,M=a9*A,N=a9*P;
A58: a in A by AFF_1:15;
A59: a<>b by A54,AFF_1:7;
then
A60: A is being_line by AFF_1:def 3;
A61: a in P by AFF_1:15;
A62: not A // P
proof
assume A // P;
then A=P by A58,A61,AFF_1:45;
hence contradiction by A54,A58,A55,A60,AFF_1:21;
end;
A63: P is being_line by A56,AFF_1:def 3;
A c= X by A1,A51,A52,A59,Th19;
hence
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) by A50,A60,A63,A49,A62,A57,Def3;
end;
hence thesis by A3;
end;
theorem
A // M & M '||' X implies A '||' X
proof
assume that
A1: A // M and
A2: M '||' X;
A3: M is being_line by A1,AFF_1:36;
A4: A is being_line by A1,AFF_1:36;
now
consider q,p such that
A5: q in A and
p in A and
q<>p by A4,AFF_1:19;
let a,C;
assume that
A6: a in X and
A7: C is being_line & C c= A;
A8: a*A = a*(q*M) by A1,A3,A5,Def3
.= a*M by A3,Th31;
C = A by A4,A7,Th33;
hence a*C c= X by A2,A3,A6,A8;
end;
hence thesis;
end;
theorem Th57:
X is being_plane implies X '||' X
by Th28;
theorem Th58:
X is being_plane & Y is being_plane & X '||' Y implies Y '||' X
proof
assume that
A1: X is being_plane & Y is being_plane and
A2: X '||' Y;
consider A,P,M,N such that
A3: not A // P and
A4: A c= X & P c= X & M c= Y & N c= Y and
A5: A // M or M // A and
A6: P // N or N // P by A1,A2,Th55;
not M // N
proof
assume M // N;
then A // N by A5,AFF_1:44;
hence contradiction by A3,A6,AFF_1:44;
end;
hence thesis by A1,A4,A5,A6,Th55;
end;
theorem Th59:
X is being_plane implies X <> {}
proof
assume X is being_plane;
then ex a,b,c st a in X & b in X & c in X & not LIN a,b,c by Th34;
hence thesis;
end;
theorem Th60:
X '||' Y & Y '||' Z & Y <> {} implies X '||' Z
proof
assume that
A1: X '||' Y and
A2: Y '||' Z and
A3: Y <> {};
set x = the Element of Y;
reconsider p=x as Element of AS by A3,Lm1;
now
let a,A;
assume that
A4: a in Z and
A5: A is being_line and
A6: A c= X;
p*A c= Y & p*A is being_line by A1,A3,A5,A6,Th27;
then a*(p*A) c= Z by A2,A4;
hence a*A c= Z by A5,Th31;
end;
hence thesis;
end;
theorem Th61:
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
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: Z is being_plane &( X '||' Y & Y '||' Z or X '||' Y & Z '||' Y or Y
'||' X & Y '||' Z or Y '||' X & Z '||' Y);
X '||' Y & Y '||' Z by A1,A2,A3,Th58;
hence thesis by A2,Th59,Th60;
end;
Lm13: X is being_plane & Y is being_plane & X '||' Y & X<>Y implies not ex a
st a in X & a in Y
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: X '||' Y and
A4: X<>Y;
assume not thesis;
then consider a such that
A5: a in X and
A6: a in Y;
consider b,c such that
A7: b in X and
A8: c in X and
A9: not LIN a,b,c by A1,Lm9;
set M=Line(a,b),N=Line(a,c);
A10: a<>c by A9,AFF_1:7;
then
A11: N c= X by A1,A5,A8,Th19;
A12: a<>b by A9,AFF_1:7;
then
A13: M is being_line by AFF_1:def 3;
A14: M<>N
proof
assume M=N;
then
A15: c in M by AFF_1:15;
a in M & b in M by AFF_1:15;
hence contradiction by A9,A13,A15,AFF_1:21;
end;
A16: N is being_line by A10,AFF_1:def 3;
then a in N & a*N c= Y by A3,A6,A11,AFF_1:15;
then
A17: N c= Y by A16,Lm8;
A18: M c= X by A1,A5,A7,A12,Th19;
then a in M & a*M c= Y by A3,A6,A13,AFF_1:15;
then M c= Y by A13,Lm8;
hence contradiction by A1,A2,A4,A13,A16,A18,A11,A17,A14,Th26;
end;
theorem
X is being_plane & Y is being_plane & a in X & a in Y & X '||' Y
implies X=Y by Lm13;
theorem Th63:
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
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: Z is being_plane and
A4: X '||' Y and
A5: X<>Y and
A6: a in X /\ Z and
A7: b in X /\ Z and
A8: c in Y /\ Z and
A9: d in Y /\ Z;
A10: c in Z by A8,XBOOLE_0:def 4;
A11: a in X & a in Z by A6,XBOOLE_0:def 4;
then
A12: Z<>Y by A1,A2,A4,A5,Lm13;
A13: c in Y by A8,XBOOLE_0:def 4;
then
A14: Z<>X by A1,A2,A4,A5,A10,Lm13;
set A = X /\ Z, C = Y /\ Z;
A15: b in X & b in Z by A7,XBOOLE_0:def 4;
A16: d in Y & d in Z by A9,XBOOLE_0:def 4;
now
A17: C c= Y & C c= Z by XBOOLE_1:17;
set K=c*A;
assume that
A18: a<>b and
A19: c <>d;
A20: A is being_line by A1,A3,A11,A15,A14,A18,Th24;
then
A21: A // K by Def3;
A c= X by XBOOLE_1:17;
then
A22: K c= Y by A4,A13,A20;
A23: K c= Z by A3,A10,A20,Th28,XBOOLE_1:17;
C is being_line & K is being_line by A1,A2,A3,A11,A15,A13,A10,A16,A12,A14
,A18,A19,Th24,Th27;
then K=C by A2,A3,A12,A17,A23,A22,Th26;
hence thesis by A6,A7,A8,A9,A21,AFF_1:39;
end;
hence thesis by AFF_1:3;
end;
theorem
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
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: Z is being_plane and
A4: X '||' Y and
A5: a in X /\ Z and
A6: b in X /\ Z and
A7: c in Y /\ Z and
A8: d in Y /\ Z and
A9: X<>Y and
A10: a<>b and
A11: c <>d;
A12: d in Y & d in Z by A8,XBOOLE_0:def 4;
set A = X /\ Z, C = Y /\ Z;
A13: c in Y & c in Z by A7,XBOOLE_0:def 4;
A14: a in X & a in Z by A5,XBOOLE_0:def 4;
then Z<>Y by A1,A2,A4,A9,Lm13;
then
A15: C is being_line by A2,A3,A11,A13,A12,Th24;
A16: b in X & b in Z by A6,XBOOLE_0:def 4;
Z<>X by A1,A2,A4,A9,A13,Lm13;
then
A17: A is being_line by A1,A3,A10,A14,A16,Th24;
a,b // c,d by A1,A2,A3,A4,A5,A6,A7,A8,A9,Th63;
hence thesis by A5,A6,A7,A8,A10,A11,A17,A15,AFF_1:38;
end;
theorem Th65:
for a,X st X is being_plane ex Y st a in Y & X '||' Y & Y is being_plane
proof
let a,X;
assume
A1: X is being_plane;
then consider p,q,r such that
A2: p in X and
A3: q in X and
A4: r in X and
A5: not LIN p,q,r by Th34;
set M=Line(p,q),N=Line(p,r);
A6: p<>r by A5,AFF_1:7;
then
A7: N c= X by A1,A2,A4,Th19;
set M9=a*M,N9=a*N;
A8: p<>q by A5,AFF_1:7;
then
A9: M is being_line by AFF_1:def 3;
then
A10: M9 is being_line by Th27;
A11: p in N & r in N by AFF_1:15;
A12: p in M by AFF_1:15;
A13: q in M by AFF_1:15;
A14: not M // N
proof
assume M // N;
then r in M by A12,A11,AFF_1:45;
hence contradiction by A5,A12,A13,A9,AFF_1:21;
end;
A15: N is being_line by A6,AFF_1:def 3;
then
A16: N // N9 by Def3;
A17: M // M9 by A9,Def3;
A18: a in M9 by A9,Def3;
N9 is being_line & a in N9 by A15,Def3,Th27;
then consider Y such that
A19: M9 c= Y and
A20: N9 c= Y and
A21: Y is being_plane by A10,A18,Th38;
M c= X by A1,A2,A3,A8,Th19;
then X '||' Y by A1,A17,A16,A19,A20,A21,A7,A14,Th55;
hence thesis by A18,A19,A21;
end;
definition
let AS,a,X such that
A1: X is being_plane;
func a+X -> Subset of AS means
:Def6:
a in it & X '||' it & it is being_plane;
existence by A1,Th65;
uniqueness
proof
let Y1,Y2 be Subset of AS such that
A2: a in Y1 and
A3: X '||' Y1 and
A4: Y1 is being_plane and
A5: a in Y2 and
A6: X '||' Y2 and
A7: Y2 is being_plane;
Y1 '||' Y2 by A1,A3,A4,A6,A7,Th61;
hence thesis by A2,A4,A5,A7,Lm13;
end;
end;
theorem
X is being_plane implies ( a in X iff a+X = X )
proof
assume
A1: X is being_plane;
now
assume
A2: a in X;
X '||' X by A1,Th57;
hence a+X = X by A1,A2,Def6;
end;
hence thesis by A1,Def6;
end;
theorem
X is being_plane implies a+X = a+(q+X)
proof
assume
A1: X is being_plane;
then
A2: a in a+X by Def6;
A3: a+X is being_plane by A1,Def6;
A4: q+X is being_plane by A1,Def6;
then
A5: q+X '||' a+(q+X) by Def6;
A6: a in a+(q+X) by A4,Def6;
A7: a+(q+X) is being_plane by A4,Def6;
X '||' q+X & X '||' a+X by A1,Def6;
then a+X '||' q+X by A1,A4,A3,Th61;
then a+X '||' a+(q+X) by A4,A5,A3,A7,Th61;
hence thesis by A2,A6,A3,A7,Lm13;
end;
theorem
A is being_line & X is being_plane & A '||' X implies a*A c= a+X
proof
assume that
A1: A is being_line and
A2: X is being_plane and
A3: A '||' X;
A4: X '||' a+X & a in a+ X by A2,Def6;
consider N such that
A5: N c= X and
A6: A // N or N // A by A1,A2,A3,Th41;
a*A = a*N & N is being_line by A6,Th32,AFF_1:36;
hence thesis by A5,A4;
end;
theorem
X is being_plane & Y is being_plane & X '||' Y implies a+X = a+Y
proof
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: X '||' Y;
A4: a+X is being_plane by A1,Def6;
A5: a in a+X & a in a+Y by A1,A2,Def6;
A6: a+Y is being_plane by A2,Def6;
X '||' a+X by A1,Def6;
then
A7: a+X '||' Y by A1,A2,A3,A4,Th61;
Y '||' a+Y by A2,Def6;
then a+X '||' a+Y by A2,A4,A6,A7,Th61;
hence thesis by A5,A4,A6,Lm13;
end;