:: Elementary Variants of Affine Configurational Theorems
:: by Krzysztof Pra\.zmowski and Krzysztof Radziszewski
::
:: Received November 30, 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, AFF_2, SUBSET_1, ANALOAF, AFF_1, INCSP_1, VECTSP_1;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, PAPDESAF;
constructors AFF_1, AFF_2, TRANSLAC;
registrations STRUCT_0, PAPDESAF;
theorems AFF_1, AFF_2, PAPDESAF, DIRAF;
begin
reserve SAS for AffinPlane;
theorem Th1:
SAS is Pappian 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 is Pappian;
let a1,a2,a3,b1,b2,b3 be Element of SAS such that
A2: a1,a2 // a1,a3 and
A3: b1,b2 // b1,b3 and
A4: a1,b2 // a2,b1 and
A5: a2,b3 // a3,b2;
LIN a1,a2,a3 by A2,AFF_1:def 1;
then consider M being Subset of SAS such that
A6: M is being_line and
A7: a1 in M and
A8: a2 in M and
A9: a3 in M by AFF_1:21;
LIN b1,b2,b3 by A3,AFF_1:def 1;
then consider N being Subset of SAS such that
A10: N is being_line and
A11: b1 in N and
A12: b2 in N and
A13: b3 in N by AFF_1:21;
A14: now
assume that
A15: M<>N and
A16: not M // N;
consider o being Element of SAS such that
A17: o in M and
A18: o in N by A6,A10,A16,AFF_1:58;
A19: now
assume that
A20: o<>a1 and
A21: b1<>o and
A22: o=b3;
A23: now
assume a2<>o;
then b2 in M by A5,A6,A8,A9,A17,A22,AFF_1:48;
then b2=o by A6,A10,A12,A15,A17,A18,AFF_1:18;
then b1 in M by A4,A6,A7,A8,A17,A20,AFF_1:48;
hence thesis by A6,A7,A9,A17,A22,AFF_1:51;
end;
now
assume a2=o;
then o,b1 // b2,a1 by A4,AFF_1:4;
then a1 in N by A10,A11,A12,A13,A21,A22,AFF_1:48;
hence thesis by A6,A7,A10,A15,A17,A18,A20,AFF_1:18;
end;
hence thesis by A23;
end;
A24: now
assume that
o<>a1 and
A25: b1=o;
A26: o,a2 // a1,b2 by A4,A25,AFF_1:4;
A27: now
assume a2<>o;
then b2 in M by A6,A7,A8,A17,A26,AFF_1:48;
then b2=o by A6,A10,A12,A15,A17,A18,AFF_1:18;
then
A28: o,a3 // a2,b3 by A5,AFF_1:4;
now
assume o<>a3;
then b3 in M by A6,A8,A9,A17,A28,AFF_1:48;
hence thesis by A6,A7,A9,A17,A25,AFF_1:51;
end;
hence thesis by A25,AFF_1:3;
end;
now
assume
A29: a2=o;
now
assume
A30: b3<>o;
o,b3 // b2,a3 by A5,A29,AFF_1:4;
then a3 in N by A10,A12,A13,A18,A30,AFF_1:48;
then b1=a3 by A6,A9,A10,A15,A17,A18,A25,AFF_1:18;
hence thesis by AFF_1:3;
end;
hence thesis by A6,A7,A9,A17,A25,AFF_1:51;
end;
hence thesis by A27;
end;
A31: now
assume
A32: o=a1;
then
A33: o,b2 // b1,a2 by A4,AFF_1:4;
A34: now
assume b2<>o;
then a2 in N by A10,A11,A12,A18,A33,AFF_1:48;
then a2=o by A6,A8,A10,A15,A17,A18,AFF_1:18;
then
A35: o,b3 // b2,a3 by A5,AFF_1:4;
now
assume o<>b3;
then a3 in N by A10,A12,A13,A18,A35,AFF_1:48;
hence thesis by A10,A11,A13,A18,A32,AFF_1:51;
end;
hence thesis by A32,AFF_1:3;
end;
now
assume
A36: b2=o;
now
assume
A37: a3<>o;
o,a3 // a2,b3 by A5,A36,AFF_1:4;
then b3 in M by A6,A8,A9,A17,A37,AFF_1:48;
then a1=b3 by A6,A10,A13,A15,A17,A18,A32,AFF_1:18;
hence thesis by AFF_1:3;
end;
hence thesis by A10,A11,A13,A18,A32,AFF_1:51;
end;
hence thesis by A34;
end;
A38: now
assume that
A39: o<>a1 and
A40: b1<>o and
o<>b3 and
A41: o=a3;
A42: o,b2 // b3,a2 by A5,A41,AFF_1:4;
A43: now
assume b2<>o;
then a2 in N by A10,A12,A13,A18,A42,AFF_1:48;
then a2=o by A6,A8,A10,A15,A17,A18,AFF_1:18;
then o,b1 // b2,a1 by A4,AFF_1:4;
then a1 in N by A10,A11,A12,A18,A40,AFF_1:48;
hence thesis by A10,A11,A13,A18,A41,AFF_1:51;
end;
now
assume b2=o;
then b1 in M by A4,A6,A7,A8,A9,A39,A41,AFF_1:48;
hence thesis by A6,A10,A11,A15,A17,A18,A40,AFF_1:18;
end;
hence thesis by A43;
end;
now
assume that
A44: o<>a1 & o<>b1 and
A45: o<>b3 and
A46: o<>a3;
A47: o<>b2
proof
assume o=b2;
then o,a3 // a2,b3 by A5,AFF_1:4;
then b3 in M by A6,A8,A9,A17,A46,AFF_1:48;
hence contradiction by A6,A10,A13,A15,A17,A18,A45,AFF_1:18;
end;
o<>a2
proof
assume o=a2;
then o,b3 // b2,a3 by A5,AFF_1:4;
then a3 in N by A10,A12,A13,A18,A45,AFF_1:48;
hence contradiction by A6,A9,A10,A15,A17,A18,A46,AFF_1:18;
end;
then a1,b3 // a3,b1 by A1,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A15,A17,A18
,A44,A45,A46,A47,AFF_2:def 2;
hence thesis by AFF_1:4;
end;
hence thesis by A31,A24,A19,A38;
end;
A48: SAS is satisfying_pap by A1,AFF_2:9;
now
assume M<>N & M // N;
then a1,b3 // a3,b1 by A48,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,AFF_2:def 13;
hence thesis by AFF_1:4;
end;
hence thesis by A6,A7,A9,A11,A13,A14,AFF_1:51;
end;
theorem Th2:
SAS is Desarguesian implies for o,a,a9,b,b9,c,c9 being Element of
SAS holds ( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c
// o,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
proof
assume
A1: SAS is Desarguesian;
let o,a,a9,b,b9,c,c9 be Element of SAS such that
A2: not o,a // o,b and
A3: not o,a // o,c and
A4: o,a // o,a9 and
A5: o,b // o,b9 and
A6: o,c // o,c9 and
A7: a,b // a9,b9 & a,c // a9,c9;
A8: o<>a & o<>b by A2,AFF_1:3;
A9: o<>c by A3,AFF_1:3;
LIN o,b,b9 by A5,AFF_1:def 1;
then consider P being Subset of SAS such that
A10: P is being_line & o in P and
A11: b in P and
A12: b9 in P by AFF_1:21;
LIN o,a,a9 by A4,AFF_1:def 1;
then consider A being Subset of SAS such that
A13: A is being_line & o in A & a in A and
A14: a9 in A by AFF_1:21;
LIN o,c,c9 by A6,AFF_1:def 1;
then consider C being Subset of SAS such that
A15: C is being_line & o in C and
A16: c in C and
A17: c9 in C by AFF_1:21;
A18: A<>C by A3,A13,A16,AFF_1:51;
A<>P by A2,A13,A11,AFF_1:51;
hence thesis by A1,A7,A13,A14,A10,A11,A12,A15,A16,A17,A8,A9,A18,AFF_2:def 4;
end;
theorem Th3:
SAS is translational implies for a,a9,b,b9,c,c9 being Element of
SAS holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a
,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
proof
assume
A1: SAS is translational;
let a,a9,b,b9,c,c9 be Element of SAS such that
A2: not a,a9 // a,b and
A3: not a,a9 // a,c and
A4: a,a9 // b,b9 and
A5: a,a9 // c,c9 and
A6: a,b // a9,b9 & a,c // a9,c9;
set A=Line(a,a9);
A7: a<>a9 by A2,AFF_1:3;
then
A8: A is being_line by AFF_1:def 3;
then consider C being Subset of SAS such that
A9: c in C and
A10: A // C by AFF_1:49;
A11: C is being_line by A10,AFF_1:36;
A12: a in A & a9 in A by AFF_1:15;
then
A13: A<>C by A3,A8,A9,AFF_1:51;
A14: a,a9 // A by A8,A12,AFF_1:23;
then a,a9 // C by A10,AFF_1:43;
then c,c9 // C by A5,A7,AFF_1:32;
then
A15: c9 in C by A9,A11,AFF_1:23;
consider P being Subset of SAS such that
A16: b in P and
A17: A // P by A8,AFF_1:49;
A18: P is being_line by A17,AFF_1:36;
a,a9 // P by A14,A17,AFF_1:43;
then b,b9 // P by A4,A7,AFF_1:32;
then
A19: b9 in P by A16,A18,AFF_1:23;
A<>P by A2,A8,A12,A16,AFF_1:51;
hence thesis by A1,A6,A8,A12,A16,A17,A9,A10,A18,A11,A19,A15,A13,AFF_2:def 11;
end;
theorem
ex SAS st (for o,a,a9,b,b9,c,c9 being Element of SAS holds ( not o,a
// o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,
b9 & a,c // a9,c9 implies b,c // b9,c9 )) & (for a,a9,b,b9,c,c9 being Element
of SAS holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9
& a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) & (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
set PAS = the Fanoian Pappian Desarguesian translational AffinPlane;
reconsider SAS=PAS as AffinPlane;
take SAS;
thus thesis by Th1,Th2,Th3,PAPDESAF:def 1;
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:40;
now
assume a=o;
then
A2: o,a // o,x & o,a // o,y by AFF_1:3;
o<>x or o<>y by A1;
hence thesis by A2;
end;
hence thesis by AFF_1:2;
end;
then consider p being Element of SAS such that
A3: o<>p and
A4: 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:4;
then consider d being Element of SAS such that
A5: c,o // o,d & c,p // b,d by A3,DIRAF:40;
o,c // o,d & p,c // b,d by A5,AFF_1:4;
hence thesis;
end;
hence thesis;
end;
hence thesis by A4;
end;
end;