Copyright (c) 1990 Association of Mizar Users
environ
vocabulary DIRAF, AFF_2, ANALOAF, AFF_1, INCSP_1, VECTSP_1;
notation SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, PAPDESAF;
constructors TRANSLAC, AFF_1, AFF_2, XBOOLE_0;
clusters PAPDESAF, ZFMISC_1, XBOOLE_0;
theorems AFF_1, AFF_2, PAPDESAF, DIRAF;
begin
reserve SAS for AffinPlane;
theorem Th1: SAS satisfies_PAP implies
(for a1,a2,a3,b1,b2,b3 being Element of SAS holds
( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
implies a3,b1 // a1,b3 ))
proof assume A1: SAS satisfies_PAP;
then A2:SAS satisfies_pap by AFF_2:23;
let a1,a2,a3,b1,b2,b3 be Element of SAS such that
A3: a1,a2 // a1,a3 & b1,b2 // b1,b3 and A4: a1,b2 // a2,b1 & a2,b3 // a3,b2;
A5: LIN a1,a2,a3 & LIN b1,b2,b3 by A3,AFF_1:def 1;
then consider M being Subset of SAS such that
A6: M is_line and A7: a1 in M & a2 in M & a3 in M by AFF_1:33;
consider N being Subset of SAS such that
A8: N is_line and A9: b1 in N & b2 in N & b3 in N by A5,AFF_1:33;
A10: now assume M<>N & M // N; then a1,b3 // a3,b1 by A2,A4,A6,A7,A8,A9,AFF_2:
def 13;
hence a3,b1 // a1,b3 by AFF_1:13; end;
now assume A11: M<>N & not M // N; then consider o being Element of the
carrier of SAS such that A12: o in M & o in N by A6,A8,AFF_1:72;
A13: now assume A14: o=a1;
then A15: o,b2 // b1,a2 by A4,AFF_1:13;
A16: now assume b2<>o; then a2 in N by A8,A9,A12,A15,AFF_1:62;
then a2=o by A6,A7,A8,A11,A12,AFF_1:30;
then A17: o,b3 // b2,a3 by A4,AFF_1:13;
now assume o<>b3; then a3 in N by A8,A9,A12,A17,AFF_1:62;
hence a3,b1 // a1,b3 by A8,A9,A12,A14,AFF_1:65; end;
hence a3,b1 // a1,b3 by A14,AFF_1:12; end;
now assume A18: b2=o;
now assume A19: a3<>o; o,a3 // a2,b3
by A4,A18,AFF_1:13; then b3 in M by A6,A7,A12,A19,AFF_1:62;
then a1=b3 by A6,A8,A9,A11,A12,A14,AFF_1:30;
hence a3,b1 // a1,b3 by AFF_1:12; end;
hence a3,b1 // a1,b3 by A8,A9,A12,A14,AFF_1:65; end;
hence a3,b1 // a1,b3 by A16; end;
A20: now assume A21: o<>a1 & b1=o;
then A22: o,a2 // a1,b2 by A4,AFF_1:13;
A23: now assume a2<>o; then b2 in M by A6,A7,A12,A22,AFF_1:62;
then b2=o by A6,A8,A9,A11,A12,AFF_1:30;
then A24: o,a3 // a2,b3 by A4,AFF_1:13;
now assume o<>a3; then b3 in M by A6,A7,A12,A24,AFF_1:62;
hence a3,b1 // a1,b3 by A6,A7,A12,A21,AFF_1:65; end;
hence a3,b1 // a1,b3 by A21,AFF_1:12; end;
now assume A25: a2=o;
now assume A26: b3<>o; o,b3 // b2,a3
by A4,A25,AFF_1:13; then a3 in N by A8,A9,A12,A26,AFF_1:62;
then b1=a3 by A6,A7,A8,A11,A12,A21,AFF_1:30;
hence a3,b1 // a1,b3 by AFF_1:12; end;
hence a3,b1 // a1,b3 by A6,A7,A12,A21,AFF_1:65; end;
hence a3,b1 // a1,b3 by A23; end;
A27: now assume A28: o<>a1 & b1<>o & o=b3;
A29: now assume a2<>o; then b2 in M by A4,A6,A7,A12,A28,AFF_1:62;
then b2=o by A6,A8,A9,A11,A12,AFF_1:30; then b1 in M by A4,A6,A7,A12,A28,AFF_1
:62;
hence a3,b1 // a1,b3 by A6,A7,A12,A28,AFF_1:65; end;
now assume a2=o; then o,b1 // b2,a1
by A4,AFF_1:13; then a1 in N by A8,A9,A28,AFF_1:62;
hence a3,b1 // a1,b3 by A6,A7,A8,A11,A12,A28,AFF_1:30; end;
hence a3,b1 // a1,b3 by A29; end;
A30: now assume A31: o<>a1 & b1<>o & o<>b3 & o=a3;
then A32: o,b2 // b3,a2 by A4,AFF_1:13;
A33: now assume b2<>o; then a2 in N by A8,A9,A12,A32,AFF_1:62;
then a2=o by A6,A7,A8,A11,A12,AFF_1:30;
then o,b1 // b2,a1 by A4,AFF_1:13;
then a1 in N by A8,A9,A12,A31,AFF_1:62;
hence a3,b1 // a1,b3 by A8,A9,A12,A31,AFF_1:65; end;
now assume b2=o;
then b1 in M by A4,A6,A7,A31,AFF_1:62;
hence a3,b1 // a1,b3 by A6,A8,A9,A11,A12,A31,AFF_1:30; end;
hence a3,b1 // a1,b3 by A33; end;
now assume A34: o<>a1 & o<>b1 & o<>b3 & o<>a3;
A35: o<>a2 proof assume o=a2; then o,b3 // b2,a3
by A4,AFF_1:13; then a3 in
N by A8,A9,A12,A34,AFF_1:62;hence contradiction by A6,A7,A8,A11,A12,A34,AFF_1:
30; end;
o<>b2 proof assume o=b2; then o,a3 // a2,b3
by A4,AFF_1:13; then b3 in
M by A6,A7,A12,A34,AFF_1:62;hence contradiction by A6,A8,A9,A11,A12,A34,AFF_1:
30; end;
then a1,b3 // a3,b1 by A1,A4,A6,A7,A8,A9,A11,A12,A34,A35,AFF_2:def 2;
hence a3,b1 // a1,b3 by AFF_1:13; end;
hence a3,b1 // a1,b3 by A13,A20,A27,A30; end;
hence a3,b1 // a1,b3 by A6,A7,A9,A10,AFF_1:65; end;
theorem Th2: SAS satisfies_DES implies
(for o,a,a',b,b',c,c' being Element of SAS holds
( not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' &
o,c // o,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' ))
proof assume A1: SAS satisfies_DES;
let o,a,a',b,b',c,c' be Element of SAS such that
A2: not o,a // o,b & not o,a // o,c and A3: o,a // o,a' & o,b // o,b' &
o,c // o,c' and A4: a,b // a',b' & a,c // a',c';
A5: LIN o,a,a' & LIN o,b,b' & LIN o,c,c' by A3,AFF_1:def 1;
then consider A being Subset of SAS such that
A6: A is_line and A7: o in A & a in A & a' in A by AFF_1:33;
consider P being Subset of SAS such that
A8: P is_line and A9: o in P & b in P & b' in P by A5,AFF_1:33;
consider C being Subset of SAS such that
A10: C is_line and A11: o in C & c in C & c' in C by A5,AFF_1:33;
A12: o<>a & o<>b & o<>c by A2,AFF_1:12;
A13: A<>P by A2,A6,A7,A9,AFF_1:65;
A<>C by A2,A6,A7,A11,AFF_1:65;
hence b,c // b',c' by A1,A4,A6,A7,A8,A9,A10,A11,A12,A13,AFF_2:def 4; end;
theorem Th3: SAS satisfies_des implies
(for a,a',b,b',c,c' being Element of SAS holds
( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' &
a,b // a',b' & a,c // a',c' implies b,c // b',c' ))
proof assume A1: SAS satisfies_des;
let a,a',b,b',c,c' be Element of SAS such that
A2: not a,a' // a,b & not a,a' // a,c and A3: a,a' // b,b' & a,a' // c,c' and
A4: a,b // a',b' & a,c // a',c';
A5: a<>a' by A2,AFF_1:12; set A=Line(a,a');
A6: A is_line & a in A & a' in A by A5,AFF_1:26,def 3;
then A7: a,a' // A by AFF_1:37;
consider P being Subset of SAS such that
A8: b in P and A9: A // P by A6,AFF_1:63;
consider C being Subset of SAS such that
A10: c in C and A11: A // C by A6,AFF_1:63;
A12: P is_line & C is_line by A9,A11,AFF_1:50;
a,a' // P & a,a' // C by A7,A9,A11,AFF_1:57;
then b,b' // P & c,c' // C by A3,A5,AFF_1:46;
then A13: b' in P & c' in C by A8,A10,A12,AFF_1:37;
A14: A<>P by A2,A6,A8,AFF_1:65;
A<>C by A2,A6,A10,AFF_1:65;
hence b,c // b',c' by A1,A4,A6,A8,A9,A10,A11,A12,A13,A14,AFF_2:def 11; end;
canceled;
theorem ex SAS st
(for o,a,a',b,b',c,c' being Element of SAS holds
( not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' &
o,c // o,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' )) &
(for a,a',b,b',c,c' being Element of SAS holds
( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' &
a,b // a',b' & a,c // a',c' implies b,c // b',c' )) &
(for a1,a2,a3,b1,b2,b3 being Element of SAS holds
( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
implies a3,b1 // a1,b3 )) &
(for a,b,c,d being Element of SAS holds
( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c ))
proof consider PAS being Fanoian Pappian Desarguesian translational AffinPlane;
reconsider SAS=PAS as AffinPlane;
take SAS; thus thesis by Th1,Th2,Th3,PAPDESAF:def 5; end;
theorem for o,a being Element of SAS holds
(ex p being Element of SAS st
(for b,c being Element of SAS holds (o,a // o,p &
ex d being Element of SAS st
( o,p // o,b implies o,c // o,d & p,c // b,d ))))
proof let o,a be Element of SAS;
ex p being Element of SAS st o<>p & o,a // o,p
proof consider x,y being Element of SAS such that
A1: x<>y by DIRAF:47;
A2: now assume A3: a<>o; take p=a; o,a // o,p by AFF_1:11;
hence thesis by A3; end;
now assume A4: a=o; A5: o<>x or o<>y by A1;
o,a // o,x & o,a // o,y by A4,AFF_1:12; hence thesis by A5; end;
hence thesis by A2; end;
then consider p being Element of SAS such that
A6: o<>p & o,a // o,p; take p;
thus for b,c being Element of SAS holds (o,a // o,p &
ex d being Element of SAS st
( o,p // o,b implies o,c // o,d & p,c // b,d ))
proof let b,c be Element of SAS;
ex d being Element of SAS st (o,p // o,b implies
o,c // o,d & p,c // b,d) proof
now assume o,p // o,b; then p,o // o,b by AFF_1:13;
then consider d being Element of SAS such that
A7: c,o // o,d & c,p // b,d by A6,DIRAF:47;
o,c // o,d & p,c // b,d by A7,AFF_1:13;
hence ex d being Element of SAS
st (o,p // o,b implies o,c // o,d & p,c // b,d); end;
hence thesis; end; hence thesis by A6; end; end;