:: PARDEPAP semantic presentation

begin

theorem Th1: :: PARDEPAP:1
for SAS being AffinPlane st SAS is Pappian holds
for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3
proof
let SAS be AffinPlane; ::_thesis: ( SAS is Pappian implies for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 )
assume A1: SAS is Pappian ; ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3
let a1, a2, a3, b1, b2, b3 be Element of SAS; ::_thesis: ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 implies a3,b1 // a1,b3 )
assume that
A2: a1,a2 // a1,a3 and
A3: b1,b2 // b1,b3 and
A4: a1,b2 // a2,b1 and
A5: a2,b3 // a3,b2 ; ::_thesis: a3,b1 // a1,b3
 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__::_thesis:_(_M_<>_N_&_not_M_//_N_implies_a3,b1_//_a1,b3_)
assume that
A15: M <> N and
A16: not M // N ; ::_thesis: a3,b1 // a1,b3
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__::_thesis:_(_o_<>_a1_&_b1_<>_o_&_o_=_b3_implies_a3,b1_//_a1,b3_)
assume that
A20: o <> a1 and
A21: b1 <> o and
A22: o = b3 ; ::_thesis: a3,b1 // a1,b3
A23: now__::_thesis:_(_a2_<>_o_implies_a3,b1_//_a1,b3_)
assume  a2 <> o ; ::_thesis: a3,b1 // a1,b3
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  a3,b1 // a1,b3 by A6, A7, A9, A17, A22, AFF_1:51; ::_thesis: verum
end;
now__::_thesis:_(_a2_=_o_implies_a3,b1_//_a1,b3_)
assume  a2 = o ; ::_thesis: a3,b1 // a1,b3
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  a3,b1 // a1,b3 by A6, A7, A10, A15, A17, A18, A20, AFF_1:18; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A23; ::_thesis: verum
end;
A24: now__::_thesis:_(_o_<>_a1_&_b1_=_o_implies_a3,b1_//_a1,b3_)
assume that
 o <> a1 and
A25: b1 = o ; ::_thesis: a3,b1 // a1,b3
A26: o,a2 // a1,b2 by A4, A25, AFF_1:4;
A27: now__::_thesis:_(_a2_<>_o_implies_a3,b1_//_a1,b3_)
assume  a2 <> o ; ::_thesis: a3,b1 // a1,b3
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__::_thesis:_(_o_<>_a3_implies_a3,b1_//_a1,b3_)
assume  o <> a3 ; ::_thesis: a3,b1 // a1,b3
then  b3 in M by A6, A8, A9, A17, A28, AFF_1:48;
hence  a3,b1 // a1,b3 by A6, A7, A9, A17, A25, AFF_1:51; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A25, AFF_1:3; ::_thesis: verum
end;
now__::_thesis:_(_a2_=_o_implies_a3,b1_//_a1,b3_)
assume A29: a2 = o ; ::_thesis: a3,b1 // a1,b3
now__::_thesis:_(_b3_<>_o_implies_a3,b1_//_a1,b3_)
assume A30: b3 <> o ; ::_thesis: a3,b1 // a1,b3
 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  a3,b1 // a1,b3 by AFF_1:3; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A6, A7, A9, A17, A25, AFF_1:51; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A27; ::_thesis: verum
end;
A31: now__::_thesis:_(_o_=_a1_implies_a3,b1_//_a1,b3_)
assume A32: o = a1 ; ::_thesis: a3,b1 // a1,b3
then A33: o,b2 // b1,a2 by A4, AFF_1:4;
A34: now__::_thesis:_(_b2_<>_o_implies_a3,b1_//_a1,b3_)
assume  b2 <> o ; ::_thesis: a3,b1 // a1,b3
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__::_thesis:_(_o_<>_b3_implies_a3,b1_//_a1,b3_)
assume  o <> b3 ; ::_thesis: a3,b1 // a1,b3
then  a3 in N by A10, A12, A13, A18, A35, AFF_1:48;
hence  a3,b1 // a1,b3 by A10, A11, A13, A18, A32, AFF_1:51; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A32, AFF_1:3; ::_thesis: verum
end;
now__::_thesis:_(_b2_=_o_implies_a3,b1_//_a1,b3_)
assume A36: b2 = o ; ::_thesis: a3,b1 // a1,b3
now__::_thesis:_(_a3_<>_o_implies_a3,b1_//_a1,b3_)
assume A37: a3 <> o ; ::_thesis: a3,b1 // a1,b3
 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  a3,b1 // a1,b3 by AFF_1:3; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A10, A11, A13, A18, A32, AFF_1:51; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A34; ::_thesis: verum
end;
A38: now__::_thesis:_(_o_<>_a1_&_b1_<>_o_&_o_<>_b3_&_o_=_a3_implies_a3,b1_//_a1,b3_)
assume that
A39: o <> a1 and
A40: b1 <> o and
 o <> b3 and
A41: o = a3 ; ::_thesis: a3,b1 // a1,b3
A42: o,b2 // b3,a2 by A5, A41, AFF_1:4;
A43: now__::_thesis:_(_b2_<>_o_implies_a3,b1_//_a1,b3_)
assume  b2 <> o ; ::_thesis: a3,b1 // a1,b3
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  a3,b1 // a1,b3 by A10, A11, A13, A18, A41, AFF_1:51; ::_thesis: verum
end;
now__::_thesis:_(_b2_=_o_implies_a3,b1_//_a1,b3_)
assume  b2 = o ; ::_thesis: a3,b1 // a1,b3
then  b1 in M by A4, A6, A7, A8, A9, A39, A41, AFF_1:48;
hence  a3,b1 // a1,b3 by A6, A10, A11, A15, A17, A18, A40, AFF_1:18; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A43; ::_thesis: verum
end;
now__::_thesis:_(_o_<>_a1_&_o_<>_b1_&_o_<>_b3_&_o_<>_a3_implies_a3,b1_//_a1,b3_)
assume that
A44: ( o <> a1 & o <> b1 ) and
A45: o <> b3 and
A46: o <> a3 ; ::_thesis: a3,b1 // a1,b3
A47: o <> b2
proof
assume  o = b2 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
 o <> a2
proof
assume  o = a2 ; ::_thesis: contradiction
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; ::_thesis: verum
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  a3,b1 // a1,b3 by AFF_1:4; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A31, A24, A19, A38; ::_thesis: verum
end;
A48: SAS is satisfying_pap by A1, AFF_2:9;
now__::_thesis:_(_M_<>_N_&_M_//_N_implies_a3,b1_//_a1,b3_)
assume  ( M <> N & M // N ) ; ::_thesis: a3,b1 // a1,b3
then  a1,b3 // a3,b1 by A48, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, AFF_2:def_13;
hence  a3,b1 // a1,b3 by AFF_1:4; ::_thesis: verum
end;
hence  a3,b1 // a1,b3 by A6, A7, A9, A11, A13, A14, AFF_1:51; ::_thesis: verum
end;

theorem Th2: :: PARDEPAP:2
for SAS being AffinPlane st SAS is Desarguesian holds
for o, a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9
proof
let SAS be AffinPlane; ::_thesis: ( SAS is Desarguesian implies for o, a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 )
assume A1: SAS is Desarguesian ; ::_thesis: for o, a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9
let o, a, a9, b, b9, c, c9 be Element of SAS; ::_thesis: ( 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 )
assume 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 ) ; ::_thesis: b,c // b9,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  b,c // b9,c9 by A1, A7, A13, A14, A10, A11, A12, A15, A16, A17, A8, A9, A18, AFF_2:def_4; ::_thesis: verum
end;

theorem Th3: :: PARDEPAP:3
for SAS being AffinPlane st SAS is translational holds
for a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9
proof
let SAS be AffinPlane; ::_thesis: ( SAS is translational implies for a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 )
assume A1: SAS is translational ; ::_thesis: for a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9
let a, a9, b, b9, c, c9 be Element of SAS; ::_thesis: ( 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 )
assume 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 ) ; ::_thesis: b,c // b9,c9
set A = Line (a,a9);
A7: a <> a9 by A2, AFF_1:3;
then A8: Line (a,a9) is being_line by AFF_1:def_3;
then consider C being Subset of SAS such that
A9: c in C and
A10: Line (a,a9) // C by AFF_1:49;
A11: C is being_line by A10, AFF_1:36;
A12: ( a in Line (a,a9) & a9 in Line (a,a9) ) by AFF_1:15;
then A13: Line (a,a9) <> C by A3, A8, A9, AFF_1:51;
A14: a,a9 // Line (a,a9) 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: Line (a,a9) // 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;
 Line (a,a9) <> P by A2, A8, A12, A16, AFF_1:51;
hence  b,c // b9,c9 by A1, A6, A8, A12, A16, A17, A9, A10, A18, A11, A19, A15, A13, AFF_2:def_11; ::_thesis: verum
end;

theorem :: PARDEPAP:4
ex SAS being AffinPlane st
( ( for o, a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) )
proof
set PAS = the Pappian Desarguesian translational Fanoian AffinPlane;
reconsider SAS = the Pappian Desarguesian translational Fanoian AffinPlane as AffinPlane ;
take  SAS ; ::_thesis: ( ( for o, a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) )
thus  ( ( for o, a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 ) & ( for a, a9, b, b9, c, c9 being Element of SAS st 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 holds
b,c // b9,c9 ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) ) by Th1, Th2, Th3, PAPDESAF:def_1; ::_thesis: verum
end;

theorem :: PARDEPAP:5
for SAS being AffinPlane
for o, a being Element of SAS 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 SAS be AffinPlane; ::_thesis: for o, a being Element of SAS 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 ) ) )
let o, a be Element of SAS; ::_thesis: 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 ) ) )
 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__::_thesis:_(_a_=_o_implies_ex_p_being_Element_of_SAS_st_
(_o_<>_p_&_o,a_//_o,p_)_)
assume  a = o ; ::_thesis: ex p being Element of SAS st
( o <> p & o,a // o,p )
then A2: ( o,a // o,x & o,a // o,y ) by AFF_1:3;
 ( o <> x or o <> y ) by A1;
hence  ex p being Element of SAS st
( o <> p & o,a // o,p ) by A2; ::_thesis: verum
end;
hence  ex p being Element of SAS st
( o <> p & o,a // o,p ) by AFF_1:2; ::_thesis: verum
end;
then consider p being Element of SAS such that
A3: o <> p and
A4: o,a // o,p ;
take  p ; ::_thesis: 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 ) ) )
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 ) ) ) ::_thesis: verum
proof
let b, c be Element of SAS; ::_thesis: ( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )
 ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) )
proof
now__::_thesis:_(_o,p_//_o,b_implies_ex_d_being_Element_of_SAS_st_
(_o,p_//_o,b_implies_(_o,c_//_o,d_&_p,c_//_b,d_)_)_)
assume  o,p // o,b ; ::_thesis: ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) )
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  ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ; ::_thesis: verum
end;
hence  ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ; ::_thesis: verum
end;
hence  ( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) by A4; ::_thesis: verum
end;
end;