:: TRANSLAC semantic presentation 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, p be Element of AS; ::_thesis: ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p implies ex x being Element of AS st ( LIN p,a,x & p <> x & a <> x ) ) assume that A1: LIN a,b,c and A2: a <> b and A3: a <> c and A4: b <> c and A5: not LIN a,b,p ; ::_thesis: ex x being Element of AS st ( LIN p,a,x & p <> x & a <> x ) a,b // a,c by A1, AFF_1:def_1; then b,a // a,c by AFF_1:4; then consider x being Element of AS such that A6: p,a // a,x and A7: p,b // c,x by A2, DIRAF:40; A8: now__::_thesis:_not_p_=_x assume p = x ; ::_thesis: contradiction then p,b // p,c by A7, AFF_1:4; then LIN p,b,c by AFF_1:def_1; then A9: LIN b,c,p by AFF_1:6; ( LIN b,c,a & LIN b,c,b ) by A1, AFF_1:6, AFF_1:7; hence contradiction by A4, A5, A9, AFF_1:8; ::_thesis: verum end; A10: now__::_thesis:_not_a_=_x assume a = x ; ::_thesis: contradiction then A11: p,b // a,c by A7, AFF_1:4; a,b // a,c by A1, AFF_1:def_1; then a,b // p,b by A3, A11, AFF_1:5; then b,a // b,p by AFF_1:4; then LIN b,a,p by AFF_1:def_1; hence contradiction by A5, AFF_1:6; ::_thesis: verum end; a,p // a,x by A6, AFF_1:4; then LIN a,p,x by AFF_1:def_1; then LIN p,a,x by AFF_1:6; hence ex x being Element of AS st ( LIN p,a,x & p <> x & a <> x ) by A8, A10; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, p, q be Element of AS; ::_thesis: ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q implies ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) ) assume that A1: LIN a,b,c and A2: a <> b and A3: a <> c and A4: b <> c and A5: not LIN a,b,p and A6: LIN a,b,q ; ::_thesis: ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) A7: now__::_thesis:_(_q_=_c_&_q_<>_a_&_q_<>_b_implies_ex_x_being_Element_of_AS_st_ (_LIN_p,q,x_&_p_<>_x_&_q_<>_x_)_) assume that A8: q = c and q <> a and q <> b ; ::_thesis: ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) A9: now__::_thesis:_not_LIN_q,a,p assume A10: LIN q,a,p ; ::_thesis: contradiction ( LIN c,a,b & LIN c,a,a ) by A1, AFF_1:6, AFF_1:7; hence contradiction by A3, A5, A8, A10, AFF_1:8; ::_thesis: verum end; LIN q,a,b by A6, AFF_1:6; hence ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) by A2, A3, A4, A8, A9, Lm1; ::_thesis: verum end; A11: now__::_thesis:_(_q_<>_a_&_q_<>_b_&_q_<>_c_implies_ex_x_being_Element_of_AS_st_ (_LIN_p,q,x_&_p_<>_x_&_q_<>_x_)_) assume that A12: q <> a and A13: q <> b and q <> c ; ::_thesis: ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) A14: now__::_thesis:_not_LIN_q,a,p assume LIN q,a,p ; ::_thesis: contradiction then LIN a,q,p by AFF_1:6; then A15: a,q // a,p by AFF_1:def_1; LIN a,q,b by A6, AFF_1:6; then a,q // a,b by AFF_1:def_1; then a,b // a,p by A12, A15, AFF_1:5; hence contradiction by A5, AFF_1:def_1; ::_thesis: verum end; LIN q,a,b by A6, AFF_1:6; hence ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) by A2, A12, A13, A14, Lm1; ::_thesis: verum end; now__::_thesis:_(_q_=_b_&_q_<>_a_&_q_<>_c_implies_ex_x_being_Element_of_AS_st_ (_LIN_p,q,x_&_p_<>_x_&_q_<>_x_)_) assume that A16: q = b and q <> a and q <> c ; ::_thesis: ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) ( LIN q,a,c & not LIN q,a,p ) by A1, A5, A16, AFF_1:6; hence ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) by A2, A3, A4, A16, Lm1; ::_thesis: verum end; hence ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) by A1, A2, A3, A4, A5, A7, A11, Lm1; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: 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 ) let a, b, c, p, q be Element of AS; ::_thesis: ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & p,q // a,b implies ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) ) assume that A1: LIN a,b,c and A2: a <> b and A3: a <> c and A4: b <> c and A5: not LIN a,b,p and A6: p,q // a,b ; ::_thesis: ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) A7: b <> q proof assume b = q ; ::_thesis: contradiction then b,p // b,a by A6, AFF_1:4; then LIN b,p,a by AFF_1:def_1; hence contradiction by A5, AFF_1:6; ::_thesis: verum end; A8: a <> q proof assume a = q ; ::_thesis: contradiction then a,p // a,b by A6, AFF_1:4; then LIN a,p,b by AFF_1:def_1; hence contradiction by A5, AFF_1:6; ::_thesis: verum end; A9: not LIN a,b,q proof assume A10: LIN a,b,q ; ::_thesis: contradiction then a,b // a,q by AFF_1:def_1; then p,q // a,q by A2, A6, AFF_1:5; then q,p // q,a by AFF_1:4; then LIN q,p,a by AFF_1:def_1; then A11: LIN q,a,p by AFF_1:6; A12: LIN q,a,a by AFF_1:7; LIN q,a,b by A10, AFF_1:6; hence contradiction by A5, A8, A11, A12, AFF_1:8; ::_thesis: verum end; consider r being Element of AS such that A13: b,c // q,r and A14: b,q // c,r by DIRAF:40; LIN b,a,c by A1, AFF_1:6; then b,a // b,c by AFF_1:def_1; then b,a // q,r by A4, A13, AFF_1:5; then a,b // q,r by AFF_1:4; then p,q // q,r by A2, A6, AFF_1:5; then q,p // q,r by AFF_1:4; then LIN q,p,r by AFF_1:def_1; then A15: LIN p,q,r by AFF_1:6; A16: not LIN a,c,p proof assume A17: LIN a,c,p ; ::_thesis: contradiction ( LIN a,c,b & LIN a,c,a ) by A1, AFF_1:6, AFF_1:7; hence contradiction by A3, A5, A17, AFF_1:8; ::_thesis: verum end; A18: now__::_thesis:_(_p_=_r_implies_ex_x_being_Element_of_AS_st_ (_LIN_p,q,x_&_p_<>_x_&_q_<>_x_)_) consider s being Element of AS such that A19: b,a // q,s and A20: b,q // a,s by DIRAF:40; A21: q <> s proof assume q = s ; ::_thesis: contradiction then q,b // q,a by A20, AFF_1:4; then LIN q,b,a by AFF_1:def_1; hence contradiction by A9, AFF_1:6; ::_thesis: verum end; assume A22: p = r ; ::_thesis: ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) A23: now__::_thesis:_not_p_=_s assume p = s ; ::_thesis: contradiction then a,p // c,p by A7, A14, A22, A20, AFF_1:5; then p,a // p,c by AFF_1:4; then LIN p,a,c by AFF_1:def_1; hence contradiction by A16, AFF_1:6; ::_thesis: verum end; a,b // q,s by A19, AFF_1:4; then p,q // q,s by A2, A6, AFF_1:5; then q,p // q,s by AFF_1:4; then LIN q,p,s by AFF_1:def_1; then LIN p,q,s by AFF_1:6; hence ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) by A23, A21; ::_thesis: verum end; q <> r proof assume q = r ; ::_thesis: contradiction then q,b // q,c by A14, AFF_1:4; then LIN q,b,c by AFF_1:def_1; then A24: LIN b,c,q by AFF_1:6; ( LIN b,c,a & LIN b,c,b ) by A1, AFF_1:6, AFF_1:7; hence contradiction by A4, A9, A24, AFF_1:8; ::_thesis: verum end; hence ex x being Element of AS st ( LIN p,q,x & p <> x & q <> x ) by A15, A18; ::_thesis: verum end; 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 ) proof let AS be AffinSpace; ::_thesis: ( ex a, b, c being Element of AS st ( LIN a,b,c & a <> b & a <> c & b <> c ) implies for p, q being Element of AS ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) ) given a, b, c being Element of AS such that A1: LIN a,b,c and A2: a <> b and A3: a <> c and A4: b <> c ; ::_thesis: for p, q being Element of AS ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) let p, q be Element of AS; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) A5: now__::_thesis:_(_LIN_a,b,p_&_LIN_a,b,q_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume that A6: LIN a,b,p and A7: LIN a,b,q ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) A8: LIN a,b,b by AFF_1:7; A9: LIN a,b,a by AFF_1:7; now__::_thesis:_(_(_p_=_c_or_q_=_c_)_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume A10: ( p = c or q = c ) ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) now__::_thesis:_(_(_p_<>_a_or_q_<>_b_)_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume ( p <> a or q <> b ) ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) A11: now__::_thesis:_(_p_=_c_&_p_<>_a_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume that A12: p = c and A13: p <> a ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) ( q = b implies ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) ) by A1, A2, A9, A8, A12, A13, AFF_1:8; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A1, A2, A4, A7, A8, A12, AFF_1:8; ::_thesis: verum end; now__::_thesis:_(_q_=_c_&_q_<>_b_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume that A14: q = c and q <> b ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) ( p = b implies ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) ) by A1, A2, A3, A9, A8, A14, AFF_1:8; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A1, A2, A4, A6, A8, A14, AFF_1:8; ::_thesis: verum end; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A3, A4, A10, A11; ::_thesis: verum end; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A1, A3, A4; ::_thesis: verum end; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A1, A2, A6, A7, AFF_1:8; ::_thesis: verum end; A15: now__::_thesis:_(_not_LIN_a,b,p_&_not_LIN_a,b,q_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume that A16: not LIN a,b,p and not LIN a,b,q ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) now__::_thesis:_(_not_p,q_//_a,b_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) consider p9 being Element of AS such that A17: a,b // p,p9 and A18: p <> p9 by DIRAF:40; assume A19: not p,q // a,b ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) A20: not LIN p,p9,q proof assume LIN p,p9,q ; ::_thesis: contradiction then p,p9 // p,q by AFF_1:def_1; hence contradiction by A19, A17, A18, AFF_1:5; ::_thesis: verum end; p,p9 // a,b by A17, AFF_1:4; then ex p99 being Element of AS st ( LIN p,p9,p99 & p <> p99 & p9 <> p99 ) by A1, A2, A3, A4, A16, Lm3; then consider r being Element of AS such that A21: LIN q,p,r and A22: ( q <> r & p <> r ) by A18, A20, Lm1; LIN p,q,r by A21, AFF_1:6; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A22; ::_thesis: verum end; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A16, Lm3; ::_thesis: verum end; now__::_thesis:_(_not_LIN_a,b,q_&_LIN_a,b,p_implies_ex_r_being_Element_of_AS_st_ (_LIN_p,q,r_&_p_<>_r_&_q_<>_r_)_) assume ( not LIN a,b,q & LIN a,b,p ) ; ::_thesis: ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) then consider x being Element of AS such that A23: LIN q,p,x and A24: ( q <> x & p <> x ) by A1, A2, A3, A4, Lm2; LIN p,q,x by A23, AFF_1:6; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A24; ::_thesis: verum end; hence ex r being Element of AS st ( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A5, A15, Lm2; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let a, b, c, d be Element of AFP; ::_thesis: ( AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c implies ex p being Element of AFP st ( LIN b,c,p & LIN a,d,p ) ) assume ( ( for a, b, c, d being Element of AFP st a,b // c,d & a,c // b,d & a,d // b,c holds LIN a,b,c ) & a,b // c,d & a,c // b,d & not LIN a,b,c ) ; :: according to TRANSLAC:def_1 ::_thesis: ex p being Element of AFP st ( LIN b,c,p & LIN a,d,p ) then not a,d // b,c ; then ex p being Element of AFP st ( LIN a,d,p & LIN b,c,p ) by AFF_1:60; hence ex p being Element of AFP st ( LIN b,c,p & LIN a,d,p ) ; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let a, b, x, y be Element of AFP; ::_thesis: ( not LIN a,b,x & a,b // x,y & x <> y implies ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) ) assume that A1: not LIN a,b,x and A2: a,b // x,y and A3: x <> y ; ::_thesis: ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) thus not LIN x,y,a ::_thesis: ( not LIN b,a,y & not LIN y,x,b ) proof A4: LIN x,y,x by AFF_1:7; assume A5: LIN x,y,a ; ::_thesis: contradiction x,y // a,b by A2, AFF_1:4; then LIN x,y,b by A3, A5, AFF_1:9; hence contradiction by A1, A3, A5, A4, AFF_1:8; ::_thesis: verum end; thus not LIN b,a,y ::_thesis: not LIN y,x,b proof assume A6: LIN b,a,y ; ::_thesis: contradiction ( b,a // y,x & b <> a ) by A1, A2, AFF_1:4, AFF_1:7; then LIN b,a,x by A6, AFF_1:9; hence contradiction by A1, AFF_1:6; ::_thesis: verum end; thus not LIN y,x,b ::_thesis: verum proof A7: LIN y,x,x by AFF_1:7; assume A8: LIN y,x,b ; ::_thesis: contradiction y,x // b,a by A2, AFF_1:4; then LIN y,x,a by A3, A8, AFF_1:9; hence contradiction by A1, A3, A8, A7, AFF_1:8; ::_thesis: verum end; end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let a, b, x, y be Element of AFP; ::_thesis: ( not LIN a,b,x & a,b // x,y & a,x // b,y implies ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) ) assume that A1: not LIN a,b,x and A2: a,b // x,y and A3: a,x // b,y ; ::_thesis: ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) x <> y proof assume x = y ; ::_thesis: contradiction then x,a // x,b by A3, AFF_1:4; then LIN x,a,b by AFF_1:def_1; hence contradiction by A1, AFF_1:6; ::_thesis: verum end; hence ( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b ) by A1, A2, Lm4; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let a, x, y be Element of AFP; ::_thesis: 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 let f be Permutation of the carrier of AFP; ::_thesis: ( f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y implies y = f . x ) assume A1: f is translation ; ::_thesis: ( LIN a,f . a,x or not a,f . a // x,y or not a,x // f . a,y or y = f . x ) then A2: f is dilatation by TRANSGEO:def_11; then A3: a,x // f . a,f . x by TRANSGEO:64; assume A4: ( not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y ) ; ::_thesis: y = f . x a,f . a // x,f . x by A1, A2, TRANSGEO:78; hence y = f . x by A4, A3, TRANSGEO:76; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: ( 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 ) thus ( AFP is translational implies 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 ) ::_thesis: ( ( 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 ) implies AFP is translational ) proof assume A1: AFP is translational ; ::_thesis: 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 let a, a9, b, c, b9, c9 be Element of AFP; ::_thesis: ( 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 implies b,c // b9,c9 ) assume that A2: not LIN a,a9,b and A3: not LIN a,a9,c and A4: a,a9 // b,b9 and A5: a,a9 // c,c9 and A6: a,b // a9,b9 and A7: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 set A = Line (a,a9); set P = Line (b,b9); set C = Line (c,c9); A8: ( a in Line (a,a9) & a9 in Line (a,a9) ) by AFF_1:15; A9: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then c,a // c,a9 by A7, AFF_1:4; then LIN c,a,a9 by AFF_1:def_1; hence contradiction by A3, AFF_1:6; ::_thesis: verum end; then A10: Line (c,c9) is being_line by AFF_1:def_3; A11: b <> b9 proof assume b = b9 ; ::_thesis: contradiction then b,a // b,a9 by A6, AFF_1:4; then LIN b,a,a9 by AFF_1:def_1; hence contradiction by A2, AFF_1:6; ::_thesis: verum end; then A12: Line (b,b9) is being_line by AFF_1:def_3; A13: a <> a9 by A2, AFF_1:7; then A14: Line (a,a9) is being_line by AFF_1:def_3; A15: c in Line (c,c9) by AFF_1:15; then A16: Line (a,a9) <> Line (c,c9) by A3, A8, A14, AFF_1:21; A17: Line (a,a9) // Line (b,b9) by A4, A13, A11, AFF_1:37; A18: ( b9 in Line (b,b9) & c9 in Line (c,c9) ) by AFF_1:15; A19: Line (a,a9) // Line (c,c9) by A5, A13, A9, AFF_1:37; A20: b in Line (b,b9) by AFF_1:15; then Line (a,a9) <> Line (b,b9) by A2, A8, A14, AFF_1:21; hence b,c // b9,c9 by A1, A6, A7, A8, A20, A15, A18, A14, A12, A10, A17, A19, A16, AFF_2:def_11; ::_thesis: verum end; assume A21: 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 ; ::_thesis: AFP is translational now__::_thesis:_for_A,_P,_C_being_Subset_of_AFP for_a,_b,_c,_a9,_b9,_c9_being_Element_of_AFP_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, P, C be Subset of AFP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AFP 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 AFP; ::_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 A22: A // P and A23: A // C and A24: a in A and A25: a9 in A and A26: b in P and A27: b9 in P and A28: c in C and A29: c9 in C and A30: A is being_line and A31: P is being_line and A32: C is being_line and A33: A <> P and A34: A <> C and A35: a,b // a9,b9 and A36: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 A37: ( a,a9 // b,b9 & a,a9 // c,c9 ) by A22, A23, A24, A25, A26, A27, A28, A29, AFF_1:39; A38: now__::_thesis:_(_a_<>_a9_implies_b,c_//_b9,c9_) assume A39: a <> a9 ; ::_thesis: b,c // b9,c9 A40: not LIN a,a9,c proof assume LIN a,a9,c ; ::_thesis: contradiction then c in A by A24, A25, A30, A39, AFF_1:25; hence contradiction by A23, A28, A34, AFF_1:45; ::_thesis: verum end; not LIN a,a9,b proof assume LIN a,a9,b ; ::_thesis: contradiction then b in A by A24, A25, A30, A39, AFF_1:25; hence contradiction by A22, A26, A33, AFF_1:45; ::_thesis: verum end; hence b,c // b9,c9 by A21, A35, A36, A37, A40; ::_thesis: verum end; now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_) assume A41: a = a9 ; ::_thesis: b,c // b9,c9 then LIN a,c,c9 by A36, AFF_1:def_1; then LIN c,c9,a by AFF_1:6; then A42: ( c = c9 or a in C ) by A28, A29, A32, AFF_1:25; LIN a,b,b9 by A35, A41, AFF_1:def_1; then LIN b,b9,a by AFF_1:6; then ( b = b9 or a in P ) by A26, A27, A31, AFF_1:25; hence b,c // b9,c9 by A22, A23, A24, A33, A34, A42, AFF_1:2, AFF_1:45; ::_thesis: verum end; hence b,c // b9,c9 by A38; ::_thesis: verum end; hence AFP is translational by AFF_2:def_11; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: for a being Element of AFP ex f being Permutation of the carrier of AFP st ( f is translation & f . a = a ) let a be Element of AFP; ::_thesis: ex f being Permutation of the carrier of AFP st ( f is translation & f . a = a ) take id the carrier of AFP ; ::_thesis: ( id the carrier of AFP is translation & (id the carrier of AFP) . a = a ) thus ( id the carrier of AFP is translation & (id the carrier of AFP) . a = a ) by FUNCT_1:18, TRANSGEO:77; ::_thesis: verum end; 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 ) ) ) proof let AFP be AffinPlane; ::_thesis: 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 ) ) ) let a, b, x be Element of AFP; ::_thesis: ( a <> b implies 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 ) ) ) ) assume A1: a <> b ; ::_thesis: 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 ) ) ) A2: now__::_thesis:_(_LIN_a,b,x_implies_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_)_)_)_) assume A3: LIN a,b,x ; ::_thesis: 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 ) ) ) consider p being Element of AFP such that A4: not LIN a,b,p by A1, AFF_1:13; consider q being Element of AFP such that A5: ( a,b // p,q & a,p // b,q ) by DIRAF:40; ex y being Element of AFP st ( p,q // x,y & p,x // q,y ) by DIRAF:40; hence 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 ) ) ) by A3, A4, A5; ::_thesis: verum end; now__::_thesis:_(_not_LIN_a,b,x_implies_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_)_)_)_) A6: ex y being Element of AFP st ( a,b // x,y & a,x // b,y ) by DIRAF:40; assume not LIN a,b,x ; ::_thesis: 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 ) ) ) hence 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 ) ) ) by A6; ::_thesis: verum end; hence 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 ) ) ) by A2; ::_thesis: verum end; 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 ) ) ) proof let AFP be AffinPlane; ::_thesis: 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 ) ) ) let a, b, y be Element of AFP; ::_thesis: ( a <> b implies 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 ) ) ) ) assume A1: a <> b ; ::_thesis: 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 ) ) ) A2: now__::_thesis:_(_LIN_a,b,y_implies_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_)_)_)_) assume A3: LIN a,b,y ; ::_thesis: 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 ) ) ) consider p being Element of AFP such that A4: not LIN a,b,p by A1, AFF_1:13; consider q being Element of AFP such that A5: a,b // p,q and A6: a,p // b,q by DIRAF:40; A7: now__::_thesis:_not_p_=_q 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 A4, AFF_1:6; ::_thesis: verum end; consider x being Element of AFP such that A8: q,p // y,x and A9: q,y // p,x by DIRAF:40; A10: p,x // q,y by A9, AFF_1:4; A11: p,q // x,y by A8, AFF_1:4; then ( a,b // x,y or p = q ) by A5, AFF_1:5; then a,b // y,x by A7, AFF_1:4; then LIN a,b,x by A1, A3, AFF_1:9; hence 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 ) ) ) by A4, A5, A6, A11, A10; ::_thesis: verum end; now__::_thesis:_(_not_LIN_a,b,y_implies_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_)_)_)_) consider x being Element of AFP such that A12: ( b,a // y,x & b,y // a,x ) by DIRAF:40; A13: ( a,b // x,y & a,x // b,y ) by A12, AFF_1:4; assume not LIN a,b,y ; ::_thesis: 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 ) ) ) then not LIN b,a,y by AFF_1:6; then not LIN a,b,x by A12, Lm5; hence 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 ) ) ) by A13; ::_thesis: verum end; hence 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 ) ) ) by A2; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let a, b, x, p, q, p9, q9, 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 & not LIN p,q,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 and A14: not LIN p,q,p9 ; ::_thesis: y = y9 A15: 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; A16: not LIN p,q,x proof assume A17: LIN p,q,x ; ::_thesis: contradiction then p,q // p,x by AFF_1:def_1; then A18: p,x // a,b by A4, A15, AFF_1:5; a,b // a,x by A3, AFF_1:def_1; then p,x // a,x by A2, A18, AFF_1:5; then x,p // x,a by AFF_1:4; then A19: LIN x,p,a by AFF_1:def_1; A20: ( LIN x,p,x & LIN a,x,b ) by A3, AFF_1:6, AFF_1:7; A21: LIN x,p,p by AFF_1:7; x <> a by A4, A6, A12, A17, Lm5; then LIN x,p,b by A19, A20, AFF_1:11; hence contradiction by A3, A12, A19, A21, AFF_1:8; ::_thesis: verum end; A22: p,q // p9,q9 by A2, A4, A5, AFF_1:5; then A23: p9,q9 // x,y by A8, A15, AFF_1:5; A24: 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; A25: not LIN p9,q9,x proof assume A26: LIN p9,q9,x ; ::_thesis: contradiction then p9,q9 // p9,x by AFF_1:def_1; then A27: p9,x // a,b by A5, A24, AFF_1:5; a,b // a,x by A3, AFF_1:def_1; then p9,x // a,x by A2, A27, AFF_1:5; then x,p9 // x,a by AFF_1:4; then A28: LIN x,p9,a by AFF_1:def_1; A29: ( LIN x,p9,x & LIN a,x,b ) by A3, AFF_1:6, AFF_1:7; A30: LIN x,p9,p9 by AFF_1:7; x <> a by A5, A7, A13, A26, Lm5; then LIN x,p9,b by A28, A29, AFF_1:11; hence contradiction by A3, A13, A28, A30, AFF_1:8; ::_thesis: verum end; p,p9 // q,q9 by A1, A4, A5, A6, A7, A12, A13, Th4; then p9,x // q9,y by A1, A8, A10, A14, A22, A16, Th4; hence y = y9 by A9, A11, A25, A23, TRANSGEO:76; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let a, b, p, q be Element of AFP; ::_thesis: ( ( 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 implies a,q // b,p ) assume that A1: for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds r = q and A2: a,b // p,q and A3: a,p // b,q and A4: not LIN a,b,p ; ::_thesis: a,q // b,p consider z being Element of AFP such that A5: q,p // a,z and A6: q,a // p,z by DIRAF:40; A7: p <> q proof assume p = q ; ::_thesis: contradiction then p,a // p,b by A3, AFF_1:4; then LIN p,a,b by AFF_1:def_1; hence contradiction by A4, AFF_1:6; ::_thesis: verum end; A8: not LIN a,p,q proof A9: LIN p,q,p by AFF_1:7; assume LIN a,p,q ; ::_thesis: contradiction then A10: LIN p,q,a by AFF_1:6; p,q // a,b by A2, AFF_1:4; then LIN p,q,b by A7, A10, AFF_1:9; hence contradiction by A4, A7, A10, A9, AFF_1:8; ::_thesis: verum end; A11: now__::_thesis:_not_a_=_z assume a = z ; ::_thesis: contradiction then a,p // a,q by A6, AFF_1:4; hence contradiction by A8, AFF_1:def_1; ::_thesis: verum end; p,q // a,z by A5, AFF_1:4; then a,b // a,z by A2, A7, AFF_1:5; then A12: LIN a,b,z by AFF_1:def_1; a <> b by A4, AFF_1:7; then ( a = z or b = z ) by A1, A12; hence a,q // b,p by A6, A11, AFF_1:4; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let a, b, x, p, q, p9, q9, 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:76; ::_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:76; ::_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:76; ::_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 end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let a, b, x, p, q, y be Element of AFP; ::_thesis: ( a <> b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p implies ( p <> q & LIN a,b,y ) ) assume that A1: ( a <> b & LIN a,b,x ) and A2: a,b // p,q and A3: a,p // b,q and A4: p,q // x,y and A5: not LIN a,b,p ; ::_thesis: ( p <> q & LIN a,b,y ) thus p <> q ::_thesis: LIN a,b,y proof assume p = q ; ::_thesis: contradiction then p,a // p,b by A3, AFF_1:4; then LIN p,a,b by AFF_1:def_1; hence contradiction by A5, AFF_1:6; ::_thesis: verum end; then a,b // x,y by A2, A4, AFF_1:5; hence LIN a,b,y by A1, AFF_1:9; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let a, b, x, p, q, p9, q9, y, x9 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 & p,x // q,y & p9,q9 // x9,y & p9,x9 // q9,y & not LIN a,b,p & not LIN a,b,p9 implies x = x9 ) 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: p,x // q,y and A10: ( p9,q9 // x9,y & p9,x9 // q9,y ) and A11: not LIN a,b,p and A12: not LIN a,b,p9 ; ::_thesis: x = x9 A13: ( b,a // q,p & b,a // q9,p9 ) by A4, A5, AFF_1:4; A14: ( b,q // a,p & b,q9 // a,p9 ) by A6, A7, AFF_1:4; A15: ( q9,p9 // y,x9 & q9,y // p9,x9 ) by A10, AFF_1:4; LIN a,b,y by A2, A3, A4, A6, A8, A11, Lm10; then A16: LIN b,a,y by AFF_1:6; A17: ( q,p // y,x & q,y // p,x ) by A8, A9, AFF_1:4; ( not LIN b,a,q & not LIN b,a,q9 ) by A4, A5, A6, A7, A11, A12, Lm5; hence x = x9 by A1, A2, A16, A13, A14, A17, A15, Lm9; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let a, b be Element of AFP; ::_thesis: ( AFP is translational & a <> b implies ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ) defpred S1[ Element of AFP, Element of AFP] means ( ( not LIN a,b,$1 & a,b // $1,$2 & a,$1 // b,$2 ) or ( LIN a,b,$1 & ex p, q being Element of AFP st ( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // $1,$2 & p,$1 // q,$2 ) ) ); assume that A1: AFP is translational and A2: a <> b ; ::_thesis: ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) A3: for x being Element of AFP ex y being Element of AFP st S1[x,y] by A2, Lm6; A4: for x, y, x9 being Element of AFP st S1[x,y] & S1[x9,y] holds x = x9 proof let x, y, x9 be Element of AFP; ::_thesis: ( S1[x,y] & S1[x9,y] implies x = x9 ) assume that A5: ( ( 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 ) ) ) and A6: ( ( not LIN a,b,x9 & a,b // x9,y & a,x9 // b,y ) or ( LIN a,b,x9 & ex p, q being Element of AFP st ( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x9,y & p,x9 // q,y ) ) ) ; ::_thesis: x = x9 A7: now__::_thesis:_(_LIN_a,b,y_implies_x_=_x9_) assume A8: LIN a,b,y ; ::_thesis: x = x9 A9: ( LIN a,b,x9 or not a,b // x9,y or not a,x9 // b,y ) proof assume that A10: not LIN a,b,x9 and A11: a,b // x9,y and a,x9 // b,y ; ::_thesis: contradiction a,b // y,x9 by A11, AFF_1:4; hence contradiction by A2, A8, A10, AFF_1:9; ::_thesis: verum end; ( LIN a,b,x or not a,b // x,y or not a,x // b,y ) proof assume that A12: not LIN a,b,x and A13: a,b // x,y and a,x // b,y ; ::_thesis: contradiction a,b // y,x by A13, AFF_1:4; hence contradiction by A2, A8, A12, AFF_1:9; ::_thesis: verum end; hence x = x9 by A1, A2, A5, A6, A9, Lm11; ::_thesis: verum end; now__::_thesis:_(_not_LIN_a,b,y_implies_x_=_x9_) assume A14: not LIN a,b,y ; ::_thesis: x = x9 then A15: b,y // a,x9 by A2, A6, Lm10, AFF_1:4; A16: ( b,y // a,x & b,a // y,x9 ) by A2, A5, A6, A14, Lm10, AFF_1:4; ( not LIN b,a,y & b,a // y,x ) by A2, A5, A14, Lm5, Lm10, AFF_1:4; hence x = x9 by A16, A15, TRANSGEO:76; ::_thesis: verum end; hence x = x9 by A7; ::_thesis: verum end; A17: for y being Element of AFP ex x being Element of AFP st S1[x,y] by A2, Lm7; A18: for x, y, y9 being Element of AFP st S1[x,y] & S1[x,y9] holds y = y9 by A1, A2, Lm9, TRANSGEO:76; ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A3, A17, A4, A18); then consider f being Permutation of the carrier of AFP such that A19: for x, y being Element of AFP holds ( f . x = y iff ( ( 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 ) ) ) ) ; A20: for x being Element of AFP holds a,b // x,f . x proof let x be Element of AFP; ::_thesis: a,b // x,f . x set y = f . x; now__::_thesis:_(_LIN_a,b,x_implies_a,b_//_x,f_._x_) assume A21: LIN a,b,x ; ::_thesis: a,b // x,f . x then consider p, q being Element of AFP such that A22: not LIN a,b,p and A23: a,b // p,q and A24: a,p // b,q and A25: p,q // x,f . x and p,x // q,f . x by A19; p <> q by A2, A21, A22, A23, A24, A25, Lm10; hence a,b // x,f . x by A23, A25, AFF_1:5; ::_thesis: verum end; hence a,b // x,f . x by A19; ::_thesis: verum end; for x, y being Element of AFP holds x,y // f . x,f . y proof let x, y be Element of AFP; ::_thesis: x,y // f . x,f . y A26: now__::_thesis:_(_LIN_a,b,x_&_not_LIN_a,b,y_implies_x,y_//_f_._x,f_._y_) A27: ex x9 being Element of AFP st ( y,f . y // x,x9 & y,x // f . y,x9 ) by DIRAF:40; assume that A28: LIN a,b,x and A29: not LIN a,b,y ; ::_thesis: x,y // f . x,f . y ( a,b // y,f . y & a,y // b,f . y ) by A19, A29; then y,x // f . y,f . x by A19, A28, A29, A27; hence x,y // f . x,f . y by AFF_1:4; ::_thesis: verum end; A30: now__::_thesis:_(_not_LIN_a,b,x_&_LIN_a,b,y_implies_x,y_//_f_._x,f_._y_) A31: ex y9 being Element of AFP st ( x,f . x // y,y9 & x,y // f . x,y9 ) by DIRAF:40; assume that A32: not LIN a,b,x and A33: LIN a,b,y ; ::_thesis: x,y // f . x,f . y ( a,b // x,f . x & a,x // b,f . x ) by A19, A32; hence x,y // f . x,f . y by A19, A32, A33, A31; ::_thesis: verum end; A34: now__::_thesis:_(_LIN_a,b,x_&_LIN_a,b,y_implies_x,y_//_f_._x,f_._y_) assume A35: ( LIN a,b,x & LIN a,b,y ) ; ::_thesis: x,y // f . x,f . y then ( LIN a,b,f . x & LIN a,b,f . y ) by A2, A20, AFF_1:9; then A36: a,b // f . x,f . y by AFF_1:10; a,b // x,y by A35, AFF_1:10; hence x,y // f . x,f . y by A2, A36, AFF_1:5; ::_thesis: verum end; now__::_thesis:_(_not_LIN_a,b,x_&_not_LIN_a,b,y_implies_x,y_//_f_._x,f_._y_) assume A37: ( not LIN a,b,x & not LIN a,b,y ) ; ::_thesis: x,y // f . x,f . y then A38: ( a,b // x,f . x & a,b // y,f . y ) by A19; ( a,x // b,f . x & a,y // b,f . y ) by A19, A37; hence x,y // f . x,f . y by A1, A37, A38, Th4; ::_thesis: verum end; hence x,y // f . x,f . y by A34, A26, A30; ::_thesis: verum end; then A39: f is dilatation by TRANSGEO:64; A40: f . a = b proof A41: LIN a,b,a by AFF_1:7; consider p being Element of AFP such that A42: not LIN a,b,p by A2, AFF_1:13; consider q being Element of AFP such that A43: ( a,b // p,q & a,p // b,q ) by DIRAF:40; ( p,a // q,b & p,q // a,b ) by A43, AFF_1:4; hence f . a = b by A19, A42, A43, A41; ::_thesis: verum end; for x, y being Element of AFP holds x,f . x // y,f . y proof let x, y be Element of AFP; ::_thesis: x,f . x // y,f . y ( a,b // x,f . x & a,b // y,f . y ) by A20; hence x,f . x // y,f . y by A2, AFF_1:5; ::_thesis: verum end; then f is translation by A39, TRANSGEO:78; hence ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) by A40; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let a, b be Element of AFP; ::_thesis: ( AFP is translational implies ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ) assume A1: AFP is translational ; ::_thesis: ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ( a = b implies ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ) by Th5; hence ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) by A1, Lm12; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: ( ( for a, b being Element of AFP ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ) implies AFP is translational ) assume A1: for a, b being Element of AFP ex f being Permutation of the carrier of AFP st ( f is translation & f . a = b ) ; ::_thesis: AFP is translational now__::_thesis:_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 let a, a9, b, c, b9, c9 be Element of AFP; ::_thesis: ( 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 implies b,c // b9,c9 ) consider f being Permutation of the carrier of AFP such that A2: f is translation and A3: f . a = a9 by A1; A4: f is dilatation by A2, TRANSGEO:def_11; assume ( 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 ) ; ::_thesis: b,c // b9,c9 then ( b9 = f . b & c9 = f . c ) by A2, A3, Th3; hence b,c // b9,c9 by A4, TRANSGEO:64; ::_thesis: verum end; hence AFP is translational by Th4; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let a be Element of AFP; ::_thesis: 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 let f, g be Permutation of the carrier of AFP; ::_thesis: ( f is translation & g is translation & not LIN a,f . a,g . a implies f * g = g * f ) assume that A1: f is translation and A2: g is translation ; ::_thesis: ( LIN a,f . a,g . a or f * g = g * f ) A3: g is dilatation by A2, TRANSGEO:def_11; then A4: a,f . a // g . a,g . (f . a) by TRANSGEO:64; assume A5: not LIN a,f . a,g . a ; ::_thesis: f * g = g * f a,g . a // f . a,g . (f . a) by A2, A3, TRANSGEO:78; then f . (g . a) = g . (f . a) by A1, A5, A4, Th3; then (f * g) . a = g . (f . a) by FUNCT_2:15; then A6: (f * g) . a = (g * f) . a by FUNCT_2:15; ( f * g is translation & g * f is translation ) by A1, A2, TRANSGEO:82; hence f * g = g * f by A6, TRANSGEO:80; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let f, g be Permutation of the carrier of AFP; ::_thesis: ( AFP is translational & f is translation & g is translation implies f * g = g * f ) assume that A1: AFP is translational and A2: f is translation and A3: g is translation ; ::_thesis: f * g = g * f A4: g is dilatation by A3, TRANSGEO:def_11; now__::_thesis:_(_f_<>_id_the_carrier_of_AFP_&_g_<>_id_the_carrier_of_AFP_implies_f_*_g_=_g_*_f_) set a = the Element of AFP; assume that A5: f <> id the carrier of AFP and A6: g <> id the carrier of AFP ; ::_thesis: f * g = g * f A7: the Element of AFP <> f . the Element of AFP by A2, A5, TRANSGEO:def_11; A8: the Element of AFP <> g . the Element of AFP by A3, A6, TRANSGEO:def_11; now__::_thesis:_(_LIN_the_Element_of_AFP,f_._the_Element_of_AFP,g_._the_Element_of_AFP_implies_f_*_g_=_g_*_f_) consider b being Element of AFP such that A9: not LIN the Element of AFP,f . the Element of AFP,b by A7, AFF_1:13; consider h being Permutation of the carrier of AFP such that A10: h is translation and A11: h . the Element of AFP = b by A1, Th7; A12: h * g is translation by A3, A10, TRANSGEO:82; assume A13: LIN the Element of AFP,f . the Element of AFP,g . the Element of AFP ; ::_thesis: f * g = g * f not LIN the Element of AFP,f . the Element of AFP,h . (g . the Element of AFP) proof A14: not LIN the Element of AFP,g . the Element of AFP,b proof assume A15: LIN the Element of AFP,g . the Element of AFP,b ; ::_thesis: contradiction ( LIN the Element of AFP,g . the Element of AFP,f . the Element of AFP & LIN the Element of AFP,g . the Element of AFP, the Element of AFP ) by A13, AFF_1:6, AFF_1:7; hence contradiction by A8, A9, A15, AFF_1:8; ::_thesis: verum end; then (g * h) . the Element of AFP = (h * g) . the Element of AFP by A3, A10, A11, Th9; then (g * h) . the Element of AFP = h . (g . the Element of AFP) by FUNCT_2:15; then A16: g . b = h . (g . the Element of AFP) by A11, FUNCT_2:15; assume A17: LIN the Element of AFP,f . the Element of AFP,h . (g . the Element of AFP) ; ::_thesis: contradiction ( the Element of AFP,g . the Element of AFP // b,g . b & the Element of AFP,b // g . the Element of AFP,g . b ) by A3, A4, TRANSGEO:64, TRANSGEO:78; then ( LIN the Element of AFP,f . the Element of AFP, the Element of AFP & not LIN g . the Element of AFP, the Element of AFP,h . (g . the Element of AFP) ) by A14, A16, Lm5, AFF_1:7; hence contradiction by A7, A13, A17, AFF_1:8; ::_thesis: verum end; then A18: not LIN the Element of AFP,f . the Element of AFP,(h * g) . the Element of AFP by FUNCT_2:15; h * (f * g) = (h * f) * g by RELAT_1:36 .= (f * h) * g by A2, A9, A10, A11, Th9 .= f * (h * g) by RELAT_1:36 .= (h * g) * f by A2, A12, A18, Th9 .= h * (g * f) by RELAT_1:36 ; hence f * g = g * f by TRANSGEO:5; ::_thesis: verum end; hence f * g = g * f by A2, A3, Th9; ::_thesis: verum end; hence f * g = g * f by TRANSGEO:4; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let p be Element of AFP; ::_thesis: 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 let f, g be Permutation of the carrier of AFP; ::_thesis: ( f is translation & g is translation & p,f . p // p,g . p implies p,f . p // p,(f * g) . p ) assume that A1: f is translation and A2: g is translation and A3: p,f . p // p,g . p ; ::_thesis: p,f . p // p,(f * g) . p A4: f is dilatation by A1, TRANSGEO:def_11; A5: now__::_thesis:_(_g_<>_id_the_carrier_of_AFP_implies_p,f_._p_//_p,(f_*_g)_._p_) assume g <> id the carrier of AFP ; ::_thesis: p,f . p // p,(f * g) . p then A6: g . p <> p by A2, TRANSGEO:def_11; p,g . p // f . p,f . (g . p) by A4, TRANSGEO:64; then p,f . p // f . p,f . (g . p) by A3, A6, AFF_1:5; then f . p,p // f . p,f . (g . p) by AFF_1:4; then LIN f . p,p,f . (g . p) by AFF_1:def_1; then LIN p,f . p,f . (g . p) by AFF_1:6; then p,f . p // p,f . (g . p) by AFF_1:def_1; hence p,f . p // p,(f * g) . p by FUNCT_2:15; ::_thesis: verum end; now__::_thesis:_(_g_=_id_the_carrier_of_AFP_implies_p,f_._p_//_p,(f_*_g)_._p_) assume g = id the carrier of AFP ; ::_thesis: p,f . p // p,(f * g) . p then f * g = f by FUNCT_2:17; hence p,f . p // p,(f * g) . p by AFF_1:2; ::_thesis: verum end; hence p,f . p // p,(f * g) . p by A5; ::_thesis: verum end; 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 ) proof let AFP be AffinPlane; ::_thesis: 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 ) let f be Permutation of the carrier of AFP; ::_thesis: ( AFP is Fanoian & AFP is translational & f is translation implies ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) ) assume that A1: AFP is Fanoian and A2: AFP is translational and A3: f is translation ; ::_thesis: ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) A4: now__::_thesis:_(_f_<>_id_the_carrier_of_AFP_implies_ex_g_being_Permutation_of_the_carrier_of_AFP_st_ (_g_is_translation_&_g_*_g_=_f_)_) set a = the Element of AFP; set b = f . the Element of AFP; assume f <> id the carrier of AFP ; ::_thesis: ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) then the Element of AFP <> f . the Element of AFP by A3, TRANSGEO:def_11; then consider c being Element of AFP such that A5: not LIN the Element of AFP,f . the Element of AFP,c by AFF_1:13; consider d being Element of AFP such that A6: c,f . the Element of AFP // the Element of AFP,d and A7: c, the Element of AFP // f . the Element of AFP,d by DIRAF:40; not LIN c,f . the Element of AFP, the Element of AFP by A5, AFF_1:6; then consider p being Element of AFP such that A8: LIN f . the Element of AFP, the Element of AFP,p and A9: LIN c,d,p by A1, A6, A7, Th2; consider f1 being Permutation of the carrier of AFP such that A10: f1 is translation and A11: f1 . p = the Element of AFP by A2, Th7; consider f2 being Permutation of the carrier of AFP such that A12: f2 is translation and A13: f2 . p = f . the Element of AFP by A2, Th7; A14: f1 * f2 is translation by A10, A12, TRANSGEO:82; A15: LIN p,c,d by A9, AFF_1:6; then A16: p,c // p,d by AFF_1:def_1; A17: now__::_thesis:_not_p,c_//_p,_the_Element_of_AFP assume p,c // p, the Element of AFP ; ::_thesis: contradiction then LIN p,c, the Element of AFP by AFF_1:def_1; then A18: LIN p, the Element of AFP,c by AFF_1:6; ( LIN p, the Element of AFP, the Element of AFP & LIN p, the Element of AFP,f . the Element of AFP ) by A8, AFF_1:6, AFF_1:7; then p = the Element of AFP by A5, A18, AFF_1:8; then ( the Element of AFP,c // c,f . the Element of AFP or the Element of AFP = d ) by A6, A16, AFF_1:5; then ( c, the Element of AFP // c,f . the Element of AFP or the Element of AFP = d ) by AFF_1:4; then ( LIN c, the Element of AFP,f . the Element of AFP or the Element of AFP = d ) by AFF_1:def_1; then the Element of AFP,c // the Element of AFP,f . the Element of AFP by A5, A7, AFF_1:4, AFF_1:6; then LIN the Element of AFP,c,f . the Element of AFP by AFF_1:def_1; hence contradiction by A5, AFF_1:6; ::_thesis: verum end; consider f3 being Permutation of the carrier of AFP such that A19: f3 is translation and A20: f3 . p = c by A2, Th7; f3 " is translation by A19, TRANSGEO:81; then A21: f1 * (f3 ") is translation by A10, TRANSGEO:82; LIN p, the Element of AFP,f . the Element of AFP by A8, AFF_1:6; then p,f1 . p // p,f2 . p by A11, A13, AFF_1:def_1; then A22: p, the Element of AFP // p,(f1 * f2) . p by A10, A11, A12, Th11; consider f4 being Permutation of the carrier of AFP such that A23: f4 is translation and A24: f4 . p = d by A2, Th7; f4 . ((f2 ") . (f . the Element of AFP)) = f4 . p by A13, TRANSGEO:2; then A25: (f4 * (f2 ")) . (f . the Element of AFP) = d by A24, FUNCT_2:15; consider h being Permutation of the carrier of AFP such that A26: h is translation and A27: h . c = the Element of AFP by A2, Th7; not LIN c, the Element of AFP,f . the Element of AFP by A5, AFF_1:6; then A28: h . (f . the Element of AFP) = d by A6, A7, A26, A27, Th3; f1 . ((f3 ") . c) = f1 . p by A20, TRANSGEO:2; then (f1 * (f3 ")) . c = the Element of AFP by A11, FUNCT_2:15; then A29: f1 * (f3 ") = h by A26, A27, A21, TRANSGEO:80; A30: f2 " is translation by A12, TRANSGEO:81; then f4 * (f2 ") is translation by A23, TRANSGEO:82; then f1 * (f3 ") = f4 * (f2 ") by A26, A28, A29, A25, TRANSGEO:80; then f1 * ((f3 ") * f3) = (f4 * (f2 ")) * f3 by RELAT_1:36; then f1 * (id the carrier of AFP) = (f4 * (f2 ")) * f3 by FUNCT_2:61; then f1 = (f4 * (f2 ")) * f3 by FUNCT_2:17 .= f4 * ((f2 ") * f3) by RELAT_1:36 .= f4 * (f3 * (f2 ")) by A2, A19, A30, Th10 .= (f4 * f3) * (f2 ") by RELAT_1:36 ; then A31: f1 * f2 = (f4 * f3) * ((f2 ") * f2) by RELAT_1:36 .= (f4 * f3) * (id the carrier of AFP) by FUNCT_2:61 .= f4 * f3 by FUNCT_2:17 ; p,f3 . p // p,f4 . p by A20, A24, A15, AFF_1:def_1; then p,c // p,(f3 * f4) . p by A19, A20, A23, Th11; then p,c // p,(f1 * f2) . p by A2, A19, A23, A31, Th10; then p = (f1 * f2) . p by A22, A17, AFF_1:5; then (f1 ") * (f1 * f2) = (f1 ") * (id the carrier of AFP) by A14, TRANSGEO:def_11; then ((f1 ") * f1) * f2 = (f1 ") * (id the carrier of AFP) by RELAT_1:36; then (id the carrier of AFP) * f2 = (f1 ") * (id the carrier of AFP) by FUNCT_2:61; then f2 = (f1 ") * (id the carrier of AFP) by FUNCT_2:17; then A32: (f2 * f2) . the Element of AFP = (f2 * (f1 ")) . the Element of AFP by FUNCT_2:17 .= f2 . ((f1 ") . the Element of AFP) by FUNCT_2:15 .= f . the Element of AFP by A11, A13, TRANSGEO:2 ; f2 * f2 is translation by A12, TRANSGEO:82; hence ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) by A3, A12, A32, TRANSGEO:80; ::_thesis: verum end; now__::_thesis:_(_f_=_id_the_carrier_of_AFP_implies_ex_g_being_Permutation_of_the_carrier_of_AFP_st_ (_g_is_translation_&_g_*_g_=_f_)_) set g = id the carrier of AFP; A33: ( id the carrier of AFP is translation & (id the carrier of AFP) * (id the carrier of AFP) = id the carrier of AFP ) by FUNCT_2:17, TRANSGEO:77; assume f = id the carrier of AFP ; ::_thesis: ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) hence ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) by A33; ::_thesis: verum end; hence ex g being Permutation of the carrier of AFP st ( g is translation & g * g = f ) by A4; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let f be Permutation of the carrier of AFP; ::_thesis: ( AFP is Fanoian & f is translation & f * f = id the carrier of AFP implies f = id the carrier of AFP ) set a = the Element of AFP; assume that A1: AFP is Fanoian and A2: f is translation and A3: f * f = id the carrier of AFP ; ::_thesis: f = id the carrier of AFP assume f <> id the carrier of AFP ; ::_thesis: contradiction then the Element of AFP <> f . the Element of AFP by A2, TRANSGEO:def_11; then consider b being Element of AFP such that A4: not LIN the Element of AFP,f . the Element of AFP,b by AFF_1:13; A5: f is dilatation by A2, TRANSGEO:def_11; then A6: the Element of AFP,b // f . the Element of AFP,f . b by TRANSGEO:64; f . b, the Element of AFP // f . (f . b),f . the Element of AFP by A5, TRANSGEO:64; then f . b, the Element of AFP // (f * f) . b,f . the Element of AFP by FUNCT_2:15; then f . b, the Element of AFP // b,f . the Element of AFP by A3, FUNCT_1:18; then A7: the Element of AFP,f . b // f . the Element of AFP,b by AFF_1:4; the Element of AFP,f . the Element of AFP // b,f . b by A2, A5, TRANSGEO:78; hence contradiction by A1, A4, A6, A7, Def1; ::_thesis: verum end; 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 proof let AFP be AffinPlane; ::_thesis: 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 let f1, f2, g be Permutation of the carrier of AFP; ::_thesis: ( AFP is translational & AFP is Fanoian & f1 is translation & f2 is translation & g = f1 * f1 & g = f2 * f2 implies f1 = f2 ) assume that A1: AFP is translational and A2: AFP is Fanoian and A3: f1 is translation and A4: f2 is translation and A5: ( g = f1 * f1 & g = f2 * f2 ) ; ::_thesis: f1 = f2 set h = (f2 ") * f1; A6: f2 " is translation by A4, TRANSGEO:81; ((f2 ") * f1) * ((f2 ") * f1) = (f2 ") * (f1 * ((f2 ") * f1)) by RELAT_1:36 .= (f2 ") * ((f1 * (f2 ")) * f1) by RELAT_1:36 .= (f2 ") * (((f2 ") * f1) * f1) by A1, A3, A6, Th10 .= (f2 ") * ((f2 ") * (f1 * f1)) by RELAT_1:36 .= ((f2 ") * (f2 ")) * (f1 * f1) by RELAT_1:36 .= (g ") * g by A5, FUNCT_1:44 .= id the carrier of AFP by FUNCT_2:61 ; then (f2 ") * f1 = id the carrier of AFP by A2, A3, A6, Th13, TRANSGEO:82; then (f2 ") * f1 = (f2 ") * f2 by FUNCT_2:61; hence f1 = f2 by TRANSGEO:5; ::_thesis: verum end;