aff_4.miz
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 be
set st x
in X holds x is
Element of AS;
theorem ::
AFF_4:1
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 ::
AFF_4:2
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,
AFF_1: 34;
hence thesis by
A2,
AFF_1: 23;
end;
theorem ::
AFF_4:3
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 ::
AFF_4:4
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,
AFF_1: 34;
hence (c,d)
// A by
A2,
AFF_1: 32;
hence thesis by
AFF_1: 34;
end;
theorem ::
AFF_4:5
((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 ::
AFF_4:6
((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 ::
AFF_4:7
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 ::
AFF_4:8
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,
AFF_1: 21;
hence thesis by
A11,
A12,
AFF_1: 55;
end;
theorem ::
AFF_4:9
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,
AFF_1: 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 ::
AFF_4:10
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 ::
AFF_4:11
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 ::
AFF_4:12
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;
::
AFF_4:def1
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;
::
AFF_4:def2
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 ::
AFF_4:13
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 ::
AFF_4:14
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 ::
AFF_4:15
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 ::
AFF_4:16
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 ::
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)
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 ::
AFF_4:18
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,
AFF_1: 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,
AFF_1: 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 ::
AFF_4:19
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 ::
AFF_4:20
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 ::
AFF_4:21
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 ::
AFF_4:22
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 ::
AFF_4:23
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,
AFF_1: 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 ::
AFF_4:24
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 be
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 be
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 ::
AFF_4:25
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 ::
AFF_4:26
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;
::
AFF_4:def3
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 ::
AFF_4:27
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 ::
AFF_4:28
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 ::
AFF_4:29
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 ::
AFF_4:30
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 ::
AFF_4:31
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 ::
AFF_4:32
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;
::
AFF_4:def4
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 ::
AFF_4:33
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 ::
AFF_4:34
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 ::
AFF_4:35
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 ::
AFF_4:36
Th36: for a, A st A is
being_line holds 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 ::
AFF_4:37
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 ::
AFF_4:38
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 ::
AFF_4:39
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 ::
AFF_4:40
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 ::
AFF_4:41
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 ::
AFF_4:42
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 ::
AFF_4:43
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;
::
AFF_4:def5
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 ::
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
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 ::
AFF_4:46
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 ::
AFF_4:47
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 ::
AFF_4:48
Th48: not AS is
AffinPlane & X is
being_plane implies ex q st not q
in X
proof
assume that
A1: not AS is
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) holds 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,
AFF_1: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,
AFF_1: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 ::
AFF_4:49
Th49: not AS is
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: not AS is
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,
AFF_1: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 ::
AFF_4:50
not AS is
AffinPlane implies AS is
Desarguesian
proof
assume not AS is
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,
AFF_1: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,
AFF_1: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 ::
AFF_4:51
Th51: not AS is
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: not AS is
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 ::
AFF_4:52
not AS is
AffinPlane implies AS is
translational
proof
assume not AS is
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 ::
AFF_4:53
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 ::
AFF_4:54
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: not AS is
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,
AFF_1: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 ::
AFF_4:55
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 ::
AFF_4:56
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 ::
AFF_4:57
Th57: X is
being_plane implies X
'||' X by
Th28;
theorem ::
AFF_4:58
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 ::
AFF_4:59
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 ::
AFF_4:60
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 ::
AFF_4:61
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 ::
AFF_4:62
X is
being_plane & Y is
being_plane & a
in X & a
in Y & X
'||' Y implies X
= Y by
Lm13;
theorem ::
AFF_4:63
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 ::
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)
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 ::
AFF_4:65
Th65: for a, X st X is
being_plane holds 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;
::
AFF_4:def6
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 ::
AFF_4:66
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 ::
AFF_4:67
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 ::
AFF_4:68
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 ::
AFF_4:69
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;