:: Translations in Affine Planes :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received June 12, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let AS be AffinSpace; attrAS is Fanoian means :Def1: :: TRANSLAC:def 1 for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,c; end; :: deftheorem Def1 defines Fanoian TRANSLAC:def_1_:_ for AS being AffinSpace holds ( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,c ); Lm1: for AS being AffinSpace for a, b, c, p being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p holds ex x being Element of AS st ( LIN p,a,x & p <> x & a <> x ) proofend; Lm2: for AS being AffinSpace for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q holds ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) proofend; Lm3: for AS being AffinSpace for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & p,q // a,b holds ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) proofend; theorem Th1: :: TRANSLAC:1 for AS being AffinSpace st ex a, b, c being Element of AS st ( LIN a,b,c & a <> b & a <> c & b <> c ) holds for p, q being Element of AS ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) proofend; theorem Th2: :: TRANSLAC:2 for AFP being AffinPlane for a, b, c, d being Element of AFP st AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c holds ex p being Element of AFP st ( LIN b,c,p & LIN a,d,p ) proofend; Lm4: for AFP being AffinPlane for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & x <> y holds ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) proofend; Lm5: for AFP being AffinPlane for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & a,x // b,y holds ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) proofend; theorem Th3: :: TRANSLAC:3 for AFP being AffinPlane for a, x, y being Element of AFP for f being Permutation of the carrier of AFP st f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y holds y = f . x proofend; theorem Th4: :: TRANSLAC:4 for AFP being AffinPlane holds ( AFP is translational iff for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 ) proofend; theorem Th5: :: TRANSLAC:5 for AFP being AffinPlane for a being Element of AFP ex f being Permutation of the carrier of AFP st ( f is translation & f . a = a ) proofend; Lm6: for AFP being AffinPlane for a, b, x being Element of AFP st a <> b holds ex y being Element of AFP st ( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st ( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) proofend; Lm7: for AFP being AffinPlane for a, b, y being Element of AFP st a <> b holds ex x being Element of AFP st ( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st ( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) proofend; Lm8: for AFP being AffinPlane for a, b, x, p, q, p9, q9, 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 & not LIN p,q,p9 holds y = y9 proofend; theorem Th6: :: TRANSLAC:6 for AFP being AffinPlane for a, b, p, q being Element of AFP st ( for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds r = q ) & a,b // p,q & a,p // b,q & not LIN a,b,p holds a,q // b,p proofend; Lm9: for AFP being AffinPlane for a, b, x, p, q, p9, q9, 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 proofend; Lm10: for AFP being AffinPlane for a, b, x, p, q, y being Element of AFP st a <> b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p holds ( p <> q & LIN a,b,y ) proofend; Lm11: for AFP being AffinPlane for a, b, x, p, q, p9, q9, y, x9 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 & p,x // q,y & p9,q9 // x9,y & p9,x9 // q9,y & not LIN a,b,p & not LIN a,b,p9 holds x = x9 proofend; Lm12: for AFP being AffinPlane for a, b being Element of AFP st AFP is translational & a <> b holds ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) proofend; theorem Th7: :: TRANSLAC:7 for AFP being AffinPlane for a, b being Element of AFP st AFP is translational holds ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) proofend; theorem :: TRANSLAC:8 for AFP being AffinPlane st ( for a, b being Element of AFP ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ) holds AFP is translational proofend; theorem Th9: :: TRANSLAC:9 for AFP being AffinPlane for a being Element of AFP for f, g being Permutation of the carrier of AFP st f is translation & g is translation & not LIN a,f . a,g . a holds f * g = g * f proofend; theorem Th10: :: TRANSLAC:10 for AFP being AffinPlane for f, g being Permutation of the carrier of AFP st AFP is translational & f is translation & g is translation holds f * g = g * f proofend; theorem Th11: :: TRANSLAC:11 for AFP being AffinPlane for p being Element of AFP for f, g being Permutation of the carrier of AFP st f is translation & g is translation & p,f . p // p,g . p holds p,f . p // p,(f * g) . p proofend; theorem :: TRANSLAC:12 for AFP being AffinPlane for f being Permutation of the carrier of AFP st AFP is Fanoian & AFP is translational & f is translation holds ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) proofend; theorem Th13: :: TRANSLAC:13 for AFP being AffinPlane for f being Permutation of the carrier of AFP st AFP is Fanoian & f is translation & f * f = id the carrier of AFP holds f = id the carrier of AFP proofend; theorem :: TRANSLAC:14 for AFP being AffinPlane for f1, f2, g being Permutation of the carrier of AFP st AFP is translational & AFP is Fanoian & f1 is translation & f2 is translation & g = f1 * f1 & g = f2 * f2 holds f1 = f2 proofend;