let AFP be AffinPlane; :: thesis: for a, b, p, p9, q, q9, x, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 holds
y = y9
let a, b, p, p9, q, q9, x, y, y9 be Element of AFP; :: thesis: ( AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 implies y = y9 )
assume that
A1: AFP is translational and
A2: a <> b and
A3: LIN a,b,x and
A4: a,b // p,q and
A5: a,b // p9,q9 and
A6: a,p // b,q and
A7: a,p9 // b,q9 and
A8: p,q // x,y and
A9: p9,q9 // x,y9 and
A10: p,x // q,y and
A11: p9,x // q9,y9 and
A12: not LIN a,b,p and
A13: not LIN a,b,p9 ; :: thesis: y = y9
A14: p <> q
proof
assume p = q ; :: thesis: contradiction
then p,a // p,b by A6, AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A12, AFF_1:6; :: thesis: verum
end;
then a,b // x,y by A4, A8, AFF_1:5;
then A15: LIN a,b,y by A2, A3, AFF_1:9;
A16: not LIN p,q,x
proof
assume LIN p,q,x ; :: thesis: contradiction
then p,q // p,x by AFF_1:def 1;
then a,b // p,x by A4, A14, AFF_1:5;
then a,b // x,p by AFF_1:4;
hence contradiction by A2, A3, A12, AFF_1:9; :: thesis: verum
end;
A17: now :: thesis: not x = y
assume x = y ; :: thesis: contradiction
then x,p // x,q by A10, AFF_1:4;
then LIN x,p,q by AFF_1:def 1;
hence contradiction by A16, AFF_1:6; :: thesis: verum
end;
A18: p9 <> q9
proof
assume p9 = q9 ; :: thesis: contradiction
then p9,a // p9,b by A7, AFF_1:4;
then LIN p9,a,b by AFF_1:def 1;
hence contradiction by A13, AFF_1:6; :: thesis: verum
end;
A19: not LIN q,p,b
proof
A20: LIN q,p,p by AFF_1:7;
assume A21: LIN q,p,b ; :: thesis: contradiction
q,p // b,a by A4, AFF_1:4;
then LIN q,p,a by A14, A21, AFF_1:9;
hence contradiction by A12, A14, A21, A20, AFF_1:8; :: thesis: verum
end;
now :: thesis: ( LIN p,q,p9 implies y = y9 )
assume A22: LIN p,q,p9 ; :: thesis: y = y9
p,q // p9,q9 by A2, A4, A5, AFF_1:5;
then A23: LIN p,q,q9 by A14, A22, AFF_1:9;
A24: now :: thesis: ( ( for x being Element of AFP holds
( not LIN a,p,x or x = a or x = p ) ) implies y = y9 )
assume A25: for x being Element of AFP holds
( not LIN a,p,x or x = a or x = p ) ; :: thesis: y = y9
then A26: for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds
r = q by Th1;
A27: now :: thesis: ( q = p9 implies y = y9 )
assume A28: q = p9 ; :: thesis: y = y9
A29: now :: thesis: ( a = x implies y = y9 )
a,q // b,p by A4, A6, A12, A26, Th6;
then A30: q,a // p,b by AFF_1:4;
A31: q,p // a,b by A4, AFF_1:4;
assume A32: a = x ; :: thesis: y = y9
then A33: ( q,a // p,y9 & not LIN q,p,a ) by A11, A14, A18, A16, A23, A25, A28, Th1, AFF_1:6;
( b = y & q,p // a,y9 ) by A2, A9, A14, A18, A17, A15, A23, A25, A28, A32, Th1;
hence y = y9 by A31, A30, A33, TRANSGEO:80; :: thesis: verum
end;
now :: thesis: ( b = x implies y = y9 )
A34: ( q,p // b,a & q,b // p,a ) by A4, A6, AFF_1:4;
assume A35: b = x ; :: thesis: y = y9
then A36: q,b // p,y9 by A11, A14, A18, A23, A25, A28, Th1;
( a = y & q,p // b,y9 ) by A2, A9, A14, A18, A17, A15, A23, A25, A28, A35, Th1;
hence y = y9 by A19, A34, A36, TRANSGEO:80; :: thesis: verum
end;
hence y = y9 by A2, A3, A25, A29, Th1; :: thesis: verum
end;
now :: thesis: ( p = p9 implies y = y9 )
assume A37: p = p9 ; :: thesis: y = y9
then q = q9 by A14, A18, A23, A25, Th1;
hence y = y9 by A8, A9, A10, A11, A16, A37, TRANSGEO:80; :: thesis: verum
end;
hence y = y9 by A14, A22, A25, A27, Th1; :: thesis: verum
end;
now :: thesis: ( ex p99 being Element of AFP st
( LIN a,p,p99 & p99 <> a & p99 <> p ) implies y = y9 )
given p99 being Element of AFP such that A38: LIN a,p,p99 and
A39: p99 <> a and
A40: p99 <> p ; :: thesis: y = y9
A41: not LIN p,q,p99
proof
assume LIN p,q,p99 ; :: thesis: contradiction
then A42: LIN p,p99,q by AFF_1:6;
( LIN p,p99,p & LIN p,p99,a ) by A38, AFF_1:6, AFF_1:7;
then LIN p,q,a by A40, A42, AFF_1:8;
hence contradiction by A4, A6, A12, Lm5; :: thesis: verum
end;
A43: not LIN p9,q9,p99
proof
p,q // p9,q9 by A2, A4, A5, AFF_1:5;
then A44: LIN p,q,q9 by A14, A22, AFF_1:9;
assume LIN p9,q9,p99 ; :: thesis: contradiction
hence contradiction by A18, A22, A41, A44, AFF_1:11; :: thesis: verum
end;
consider q99 being Element of AFP such that
A45: ( a,b // p99,q99 & a,p99 // b,q99 ) by DIRAF:40;
consider y99 being Element of AFP such that
A46: ( p99,q99 // x,y99 & p99,x // q99,y99 ) by DIRAF:40;
A47: not LIN a,b,p99
proof
assume LIN a,b,p99 ; :: thesis: contradiction
then A48: LIN a,p99,b by AFF_1:6;
( LIN a,p99,a & LIN a,p99,p ) by A38, AFF_1:6, AFF_1:7;
hence contradiction by A12, A39, A48, AFF_1:8; :: thesis: verum
end;
then y = y99 by A1, A2, A3, A4, A6, A8, A10, A12, A45, A46, A41, Lm8;
hence y = y9 by A1, A2, A3, A5, A7, A9, A11, A13, A45, A46, A43, A47, Lm8; :: thesis: verum
end;
hence y = y9 by A24; :: thesis: verum
end;
hence y = y9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm8; :: thesis: verum