let AP be AffinPlane; :: thesis: ( AP is translational iff AP is satisfying_des_1 )
hereby :: thesis: ( AP is satisfying_des_1 implies AP is translational )
assume A55: AP is translational ; :: thesis: AP is satisfying_des_1
thus AP is satisfying_des_1 :: thesis: verum
proof
let A be Subset of AP; :: according to AFF_2:def 12 :: thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & 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 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let P, C be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st A // P & 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 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( A // P & 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 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies A // C )
assume that
A56: A // P and
A57: a in A and
A58: a9 in A and
A59: b in P and
A60: b9 in P and
A61: ( c in C & c9 in C ) and
A62: A is being_line and
A63: P is being_line and
A64: C is being_line and
A65: A <> P and
A66: A <> C and
A67: a,b // a9,b9 and
A68: a,c // a9,c9 and
A69: b,c // b9,c9 and
A70: not LIN a,b,c and
A71: c <> c9 ; :: thesis: A // C
assume A72: not A // C ; :: thesis: contradiction
consider K being Subset of AP such that
A73: c9 in K and
A74: A // K by A62, AFF_1:63;
A75: a <> c by A70, AFF_1:16;
A76: not a,c // K A78: A <> K
proof
assume A79: A = K ; :: thesis: contradiction
a9,c9 // a,c by A68, AFF_1:13;
then a9 = c9 by A58, A73, A74, A76, A79, AFF_1:46, AFF_1:54;
then a9,b9 // b,c by A69, AFF_1:13;
then ( a9 = b9 or a,b // b,c ) by A67, AFF_1:14;
then ( b9 in A or b,a // b,c ) by A58, AFF_1:13;
then LIN b,a,c by A56, A60, A65, AFF_1:59, AFF_1:def 1;
hence contradiction by A70, AFF_1:15; :: thesis: verum
end;
A80: now
assume b9 = c9 ; :: thesis: contradiction
then ( a,b // a,c or a9 = b9 ) by A67, A68, AFF_1:14;
hence contradiction by A56, A58, A60, A65, A70, AFF_1:59, AFF_1:def 1; :: thesis: verum
end;
A81: K is being_line by A74, AFF_1:50;
then consider x being Element of AP such that
A82: x in K and
A83: LIN a,c,x by A76, AFF_1:73;
a,c // a,x by A83, AFF_1:def 1;
then a,x // a9,c9 by A68, A75, AFF_1:14;
then b,x // b9,c9 by A55, A56, A57, A58, A59, A60, A62, A63, A65, A67, A73, A74, A81, A82, A78, Def11;
then ( b,x // b,c or b9 = c9 ) by A69, AFF_1:14;
then LIN b,x,c by A80, AFF_1:def 1;
then A84: LIN x,c,b by AFF_1:15;
A85: LIN x,c,c by AFF_1:16;
LIN x,c,a by A83, AFF_1:15;
then c in K by A70, A82, A84, A85, AFF_1:17;
hence contradiction by A61, A64, A71, A72, A73, A74, A81, AFF_1:30; :: thesis: verum
end;
end;
assume A2: AP is satisfying_des_1 ; :: thesis: AP is translational
let A be Subset of AP; :: according to AFF_2:def 11 :: thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st 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 holds
b,c // b9,c9
let P, C be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st 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 holds
b,c // b9,c9
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( 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 )
assume that
A3: A // P and
A4: A // C and
A5: a in A and
A6: a9 in A and
A7: b in P and
A8: b9 in P and
A9: c in C and
A10: 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 ; :: thesis: b,c // b9,c9
A18: a <> b by A3, A5, A7, A14, AFF_1:59;
A19: a9 <> b9 by A3, A6, A8, A14, AFF_1:59;
set K = Line (a,c);
set N = Line (b9,c9);
A20: a <> c by A4, A5, A9, A15, AFF_1:59;
then A21: a in Line (a,c) by AFF_1:38;
assume A22: not b,c // b9,c9 ; :: thesis: contradiction
then A23: b9 <> c9 by AFF_1:12;
then A24: b9 in Line (b9,c9) by AFF_1:38;
A25: b <> c by A22, AFF_1:12;
A26: not LIN a,b,c
proof
assume A27: LIN a,b,c ; :: thesis: contradiction
then LIN b,c,a by AFF_1:15;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:13;
then A28: b,c // a9,b9 by A16, A18, AFF_1:14;
LIN c,b,a by A27, AFF_1:15;
then c,b // c,a by AFF_1:def 1;
then b,c // a,c by AFF_1:13;
then b,c // a9,c9 by A17, A20, AFF_1:14;
then a9,c9 // a9,b9 by A25, A28, AFF_1:14;
then LIN a9,c9,b9 by AFF_1:def 1;
then LIN b9,c9,a9 by AFF_1:15;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:13;
hence contradiction by A22, A19, A28, AFF_1:14; :: thesis: verum
end;
A29: c in Line (a,c) by A20, AFF_1:38;
A30: Line (b9,c9) is being_line by A23, AFF_1:38;
then consider M being Subset of AP such that
A31: b in M and
A32: Line (b9,c9) // M by AFF_1:63;
A33: c9 in Line (b9,c9) by A23, AFF_1:38;
A34: a9 <> c9 by A4, A6, A10, A15, AFF_1:59;
A35: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9 ; :: thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b // a9,c9 by A16, A19, AFF_1:14;
then a,b // a,c by A17, A34, AFF_1:14;
hence contradiction by A26, AFF_1:def 1; :: thesis: verum
end;
A36: not Line (a,c) // M
proof
assume Line (a,c) // M ; :: thesis: contradiction
then Line (a,c) // Line (b9,c9) by A32, AFF_1:58;
then a,c // b9,c9 by A21, A29, A24, A33, AFF_1:53;
then a9,c9 // b9,c9 by A17, A20, AFF_1:14;
then c9,a9 // c9,b9 by AFF_1:13;
then LIN c9,a9,b9 by AFF_1:def 1;
hence contradiction by A35, AFF_1:15; :: thesis: verum
end;
A37: Line (a,c) is being_line by A20, AFF_1:38;
A38: M is being_line by A32, AFF_1:50;
then consider x being Element of AP such that
A39: x in Line (a,c) and
A40: x in M by A37, A36, AFF_1:72;
A41: b,x // b9,c9 by A24, A33, A31, A32, A40, AFF_1:53;
set D = Line (x,c9);
A42: A <> Line (x,c9)
proof
assume A = Line (x,c9) ; :: thesis: contradiction
then c9 in A by AFF_1:26;
hence contradiction by A4, A10, A15, AFF_1:59; :: thesis: verum
end;
A43: x in Line (x,c9) by AFF_1:26;
LIN a,c,x by A37, A21, A29, A39, AFF_1:33;
then a,c // a,x by AFF_1:def 1;
then A44: a,x // a9,c9 by A17, A20, AFF_1:14;
A45: c9 in Line (x,c9) by AFF_1:26;
A46: not LIN a,b,x
proof
A47: a <> x
proof
assume a = x ; :: thesis: contradiction
then a,b // b9,c9 by A24, A33, A31, A32, A40, AFF_1:53;
then a9,b9 // b9,c9 by A16, A18, AFF_1:14;
then b9,a9 // b9,c9 by AFF_1:13;
then LIN b9,a9,c9 by AFF_1:def 1;
hence contradiction by A35, AFF_1:15; :: thesis: verum
end;
assume LIN a,b,x ; :: thesis: contradiction
then LIN x,b,a by AFF_1:15;
then A48: x,b // x,a by AFF_1:def 1;
x <> b by A37, A21, A29, A26, A39, AFF_1:33;
hence contradiction by A37, A21, A31, A38, A36, A39, A40, A48, A47, AFF_1:52; :: thesis: verum
end;
A49: P // C by A3, A4, AFF_1:58;
A50: x <> c9
proof
A51: now
A52: P // P by A3, AFF_1:58;
assume A53: P = Line (b9,c9) ; :: thesis: contradiction
then c in P by A9, A10, A49, A33, AFF_1:59;
hence contradiction by A7, A8, A22, A33, A53, A52, AFF_1:53; :: thesis: verum
end;
assume x = c9 ; :: thesis: contradiction
then M = Line (b9,c9) by A33, A32, A40, AFF_1:59;
then A54: ( P = Line (b9,c9) or b = b9 ) by A7, A8, A12, A30, A24, A31, AFF_1:30;
then b,a // b,a9 by A16, A51, AFF_1:13;
then LIN b,a,a9 by AFF_1:def 1;
then LIN a,a9,b by AFF_1:15;
then ( b in A or a = a9 ) by A5, A6, A11, AFF_1:39;
then LIN a9,c,c9 by A3, A7, A14, A17, AFF_1:59, AFF_1:def 1;
then LIN c,c9,a9 by AFF_1:15;
then ( c = c9 or a9 in C ) by A9, A10, A13, AFF_1:39;
hence contradiction by A4, A6, A15, A22, A54, A51, AFF_1:11, AFF_1:59; :: thesis: verum
end;
then Line (x,c9) is being_line by AFF_1:38;
then A // Line (x,c9) by A2, A3, A5, A6, A7, A8, A11, A12, A14, A16, A41, A44, A43, A45, A50, A46, A42, Def12;
then Line (x,c9) // C by A4, AFF_1:58;
then C = Line (x,c9) by A10, A45, AFF_1:59;
then C = Line (a,c) by A9, A13, A22, A37, A29, A39, A41, A43, AFF_1:30;
hence contradiction by A4, A5, A15, A21, AFF_1:59; :: thesis: verum