:: TRANSGEO semantic presentation begin definition let A be set ; let f, g be Permutation of A; :: original: * redefine funcg * f -> Permutation of A; coherence g * f is Permutation of A proof thus g * f is Permutation of A ; ::_thesis: verum end; end; theorem Th1: :: TRANSGEO:1 for A being non empty set for y being Element of A for f being Permutation of A ex x being Element of A st f . x = y proof let A be non empty set ; ::_thesis: for y being Element of A for f being Permutation of A ex x being Element of A st f . x = y let y be Element of A; ::_thesis: for f being Permutation of A ex x being Element of A st f . x = y let f be Permutation of A; ::_thesis: ex x being Element of A st f . x = y rng f = A by FUNCT_2:def_3; then ex x being set st ( x in dom f & f . x = y ) by FUNCT_1:def_3; hence ex x being Element of A st f . x = y ; ::_thesis: verum end; theorem Th2: :: TRANSGEO:2 for A being non empty set for x, y being Element of A for f being Permutation of A holds ( f . x = y iff (f ") . y = x ) proof let A be non empty set ; ::_thesis: for x, y being Element of A for f being Permutation of A holds ( f . x = y iff (f ") . y = x ) let x, y be Element of A; ::_thesis: for f being Permutation of A holds ( f . x = y iff (f ") . y = x ) let f be Permutation of A; ::_thesis: ( f . x = y iff (f ") . y = x ) A1: now__::_thesis:_(_f_._x_=_y_implies_x_=_(f_")_._y_) x in A ; then A2: x in dom f by FUNCT_2:def_1; assume f . x = y ; ::_thesis: x = (f ") . y hence x = (f ") . y by A2, FUNCT_1:34; ::_thesis: verum end; rng f = A by FUNCT_2:def_3; hence ( f . x = y iff (f ") . y = x ) by A1, FUNCT_1:35; ::_thesis: verum end; definition let A be non empty set ; let f, g be Permutation of A; funcf \ g -> Permutation of A equals :: TRANSGEO:def 1 (g * f) * (g "); coherence (g * f) * (g ") is Permutation of A ; end; :: deftheorem defines \ TRANSGEO:def_1_:_ for A being non empty set for f, g being Permutation of A holds f \ g = (g * f) * (g "); scheme :: TRANSGEO:sch 1 EXPermutation{ F1() -> non empty set , P1[ set , set ] } : ex f being Permutation of F1() st for x, y being Element of F1() holds ( f . x = y iff P1[x,y] ) provided A1: for x being Element of F1() ex y being Element of F1() st P1[x,y] and A2: for y being Element of F1() ex x being Element of F1() st P1[x,y] and A3: for x, y, x9 being Element of F1() st P1[x,y] & P1[x9,y] holds x = x9 and A4: for x, y, y9 being Element of F1() st P1[x,y] & P1[x,y9] holds y = y9 proof A5: for x being Element of F1() ex y being Element of F1() st P1[x,y] by A1; consider f being Function of F1(),F1() such that A6: for x being Element of F1() holds P1[x,f . x] from FUNCT_2:sch_3(A5); now__::_thesis:_for_y_being_set_st_y_in_F1()_holds_ y_in_rng_f let y be set ; ::_thesis: ( y in F1() implies y in rng f ) assume A7: y in F1() ; ::_thesis: y in rng f then consider x being Element of F1() such that A8: P1[x,y] by A2; P1[x,f . x] by A6; then f . x = y by A4, A7, A8; hence y in rng f by FUNCT_2:4; ::_thesis: verum end; then F1() c= rng f by TARSKI:def_3; then A9: rng f = F1() by XBOOLE_0:def_10; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_F1()_&_x2_in_F1()_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in F1() & x2 in F1() & f . x1 = f . x2 implies x1 = x2 ) assume that A10: x1 in F1() and A11: x2 in F1() ; ::_thesis: ( f . x1 = f . x2 implies x1 = x2 ) A12: f . x1 is Element of F1() by A10, FUNCT_2:5; ( P1[x1,f . x1] & P1[x2,f . x2] ) by A6, A10, A11; hence ( f . x1 = f . x2 implies x1 = x2 ) by A3, A10, A11, A12; ::_thesis: verum end; then f is one-to-one by FUNCT_2:19; then reconsider f = f as Permutation of F1() by A9, FUNCT_2:57; take f ; ::_thesis: for x, y being Element of F1() holds ( f . x = y iff P1[x,y] ) let x, y be Element of F1(); ::_thesis: ( f . x = y iff P1[x,y] ) thus ( f . x = y implies P1[x,y] ) by A6; ::_thesis: ( P1[x,y] implies f . x = y ) assume A13: P1[x,y] ; ::_thesis: f . x = y P1[x,f . x] by A6; hence f . x = y by A4, A13; ::_thesis: verum end; theorem :: TRANSGEO:3 for A being non empty set for x being Element of A for f being Permutation of A holds ( f . ((f ") . x) = x & (f ") . (f . x) = x ) by Th2; theorem :: TRANSGEO:4 for A being non empty set for f being Permutation of A holds f * (id A) = (id A) * f proof let A be non empty set ; ::_thesis: for f being Permutation of A holds f * (id A) = (id A) * f let f be Permutation of A; ::_thesis: f * (id A) = (id A) * f f * (id A) = f by FUNCT_2:17; hence f * (id A) = (id A) * f by FUNCT_2:17; ::_thesis: verum end; Lm1: for A being non empty set for f, g, h being Permutation of A st f * g = f * h holds g = h proof let A be non empty set ; ::_thesis: for f, g, h being Permutation of A st f * g = f * h holds g = h let f, g, h be Permutation of A; ::_thesis: ( f * g = f * h implies g = h ) assume f * g = f * h ; ::_thesis: g = h then ((f ") * f) * g = (f ") * (f * h) by RELAT_1:36; then ((f ") * f) * g = ((f ") * f) * h by RELAT_1:36; then (id A) * g = ((f ") * f) * h by FUNCT_2:61; then (id A) * g = (id A) * h by FUNCT_2:61; then g = (id A) * h by FUNCT_2:17; hence g = h by FUNCT_2:17; ::_thesis: verum end; Lm2: for A being non empty set for g, f, h being Permutation of A st g * f = h * f holds g = h proof let A be non empty set ; ::_thesis: for g, f, h being Permutation of A st g * f = h * f holds g = h let g, f, h be Permutation of A; ::_thesis: ( g * f = h * f implies g = h ) assume g * f = h * f ; ::_thesis: g = h then g * (f * (f ")) = (h * f) * (f ") by RELAT_1:36; then g * (f * (f ")) = h * (f * (f ")) by RELAT_1:36; then g * (id A) = h * (f * (f ")) by FUNCT_2:61; then g * (id A) = h * (id A) by FUNCT_2:61; then g = h * (id A) by FUNCT_2:17; hence g = h by FUNCT_2:17; ::_thesis: verum end; theorem :: TRANSGEO:5 for A being non empty set for g, f, h being Permutation of A st ( g * f = h * f or f * g = f * h ) holds g = h by Lm1, Lm2; theorem :: TRANSGEO:6 for A being non empty set for f, g, h being Permutation of A holds (f * g) \ h = (f \ h) * (g \ h) proof let A be non empty set ; ::_thesis: for f, g, h being Permutation of A holds (f * g) \ h = (f \ h) * (g \ h) let f, g, h be Permutation of A; ::_thesis: (f * g) \ h = (f \ h) * (g \ h) thus (f * g) \ h = (h * (f * ((id A) * g))) * (h ") by FUNCT_2:17 .= (h * (f * (((h ") * h) * g))) * (h ") by FUNCT_2:61 .= (h * (f * ((h ") * (h * g)))) * (h ") by RELAT_1:36 .= (h * ((f * (h ")) * (h * g))) * (h ") by RELAT_1:36 .= ((h * (f * (h "))) * (h * g)) * (h ") by RELAT_1:36 .= (h * (f * (h "))) * ((h * g) * (h ")) by RELAT_1:36 .= (f \ h) * (g \ h) by RELAT_1:36 ; ::_thesis: verum end; theorem :: TRANSGEO:7 for A being non empty set for f, g being Permutation of A holds (f ") \ g = (f \ g) " proof let A be non empty set ; ::_thesis: for f, g being Permutation of A holds (f ") \ g = (f \ g) " let f, g be Permutation of A; ::_thesis: (f ") \ g = (f \ g) " thus (f \ g) " = ((g ") ") * ((g * f) ") by FUNCT_1:44 .= ((g ") ") * ((f ") * (g ")) by FUNCT_1:44 .= g * ((f ") * (g ")) by FUNCT_1:43 .= (f ") \ g by RELAT_1:36 ; ::_thesis: verum end; theorem :: TRANSGEO:8 for A being non empty set for f, g, h being Permutation of A holds f \ (g * h) = (f \ h) \ g proof let A be non empty set ; ::_thesis: for f, g, h being Permutation of A holds f \ (g * h) = (f \ h) \ g let f, g, h be Permutation of A; ::_thesis: f \ (g * h) = (f \ h) \ g thus f \ (g * h) = ((g * h) * f) * ((h ") * (g ")) by FUNCT_1:44 .= (((g * h) * f) * (h ")) * (g ") by RELAT_1:36 .= ((g * (h * f)) * (h ")) * (g ") by RELAT_1:36 .= (f \ h) \ g by RELAT_1:36 ; ::_thesis: verum end; theorem :: TRANSGEO:9 for A being non empty set for f being Permutation of A holds (id A) \ f = id A proof let A be non empty set ; ::_thesis: for f being Permutation of A holds (id A) \ f = id A let f be Permutation of A; ::_thesis: (id A) \ f = id A thus (id A) \ f = f * (f ") by FUNCT_2:17 .= id A by FUNCT_2:61 ; ::_thesis: verum end; theorem :: TRANSGEO:10 for A being non empty set for f being Permutation of A holds f \ (id A) = f proof let A be non empty set ; ::_thesis: for f being Permutation of A holds f \ (id A) = f let f be Permutation of A; ::_thesis: f \ (id A) = f thus f \ (id A) = f * ((id A) ") by FUNCT_2:17 .= f * (id A) by FUNCT_1:45 .= f by FUNCT_2:17 ; ::_thesis: verum end; theorem :: TRANSGEO:11 for A being non empty set for a being Element of A for f, g being Permutation of A st f . a = a holds (f \ g) . (g . a) = g . a proof let A be non empty set ; ::_thesis: for a being Element of A for f, g being Permutation of A st f . a = a holds (f \ g) . (g . a) = g . a let a be Element of A; ::_thesis: for f, g being Permutation of A st f . a = a holds (f \ g) . (g . a) = g . a let f, g be Permutation of A; ::_thesis: ( f . a = a implies (f \ g) . (g . a) = g . a ) assume A1: f . a = a ; ::_thesis: (f \ g) . (g . a) = g . a (g ") . (g . a) = ((g ") * g) . a by FUNCT_2:15 .= (id A) . a by FUNCT_2:61 .= a by FUNCT_1:18 ; hence (f \ g) . (g . a) = (g * f) . a by FUNCT_2:15 .= g . a by A1, FUNCT_2:15 ; ::_thesis: verum end; definition let A be non empty set ; let f be Permutation of A; let R be Relation of [:A,A:]; predf is_FormalIz_of R means :Def2: :: TRANSGEO:def 2 for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R; end; :: deftheorem Def2 defines is_FormalIz_of TRANSGEO:def_2_:_ for A being non empty set for f being Permutation of A for R being Relation of [:A,A:] holds ( f is_FormalIz_of R iff for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ); theorem Th12: :: TRANSGEO:12 for A being non empty set for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds id A is_FormalIz_of R proof let A be non empty set ; ::_thesis: for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds id A is_FormalIz_of R let R be Relation of [:A,A:]; ::_thesis: ( R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R ) assume A1: for x being set st x in [:A,A:] holds [x,x] in R ; :: according to RELAT_2:def_1 ::_thesis: id A is_FormalIz_of R let x be Element of A; :: according to TRANSGEO:def_2 ::_thesis: for y being Element of A holds [[x,y],[((id A) . x),((id A) . y)]] in R let y be Element of A; ::_thesis: [[x,y],[((id A) . x),((id A) . y)]] in R A2: [x,y] in [:A,A:] by ZFMISC_1:def_2; ( (id A) . x = x & (id A) . y = y ) by FUNCT_1:18; hence [[x,y],[((id A) . x),((id A) . y)]] in R by A1, A2; ::_thesis: verum end; theorem Th13: :: TRANSGEO:13 for A being non empty set for f being Permutation of A for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds f " is_FormalIz_of R proof let A be non empty set ; ::_thesis: for f being Permutation of A for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds f " is_FormalIz_of R let f be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds f " is_FormalIz_of R let R be Relation of [:A,A:]; ::_thesis: ( R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f " is_FormalIz_of R ) assume A1: for x, y being set st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds [y,x] in R ; :: according to RELAT_2:def_3 ::_thesis: ( not f is_FormalIz_of R or f " is_FormalIz_of R ) assume A2: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to TRANSGEO:def_2 ::_thesis: f " is_FormalIz_of R let x be Element of A; :: according to TRANSGEO:def_2 ::_thesis: for y being Element of A holds [[x,y],[((f ") . x),((f ") . y)]] in R let y be Element of A; ::_thesis: [[x,y],[((f ") . x),((f ") . y)]] in R A3: [[((f ") . x),((f ") . y)],[(f . ((f ") . x)),(f . ((f ") . y))]] in R by A2; A4: ( [((f ") . x),((f ") . y)] in [:A,A:] & [(f . ((f ") . x)),(f . ((f ") . y))] in [:A,A:] ) by ZFMISC_1:def_2; ( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2; hence [[x,y],[((f ") . x),((f ") . y)]] in R by A1, A3, A4; ::_thesis: verum end; theorem :: TRANSGEO:14 for A being non empty set for f, g being Permutation of A for R being Relation of [:A,A:] st R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R holds f * g is_FormalIz_of R proof let A be non empty set ; ::_thesis: for f, g being Permutation of A for R being Relation of [:A,A:] st R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R holds f * g is_FormalIz_of R let f, g be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R holds f * g is_FormalIz_of R let R be Relation of [:A,A:]; ::_thesis: ( R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R implies f * g is_FormalIz_of R ) assume that A1: for x, y, z being set st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds [x,z] in R and A2: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R and A3: for x, y being Element of A holds [[x,y],[(g . x),(g . y)]] in R ; :: according to RELAT_2:def_8,TRANSGEO:def_2 ::_thesis: f * g is_FormalIz_of R let x be Element of A; :: according to TRANSGEO:def_2 ::_thesis: for y being Element of A holds [[x,y],[((f * g) . x),((f * g) . y)]] in R let y be Element of A; ::_thesis: [[x,y],[((f * g) . x),((f * g) . y)]] in R ( f . (g . x) = (f * g) . x & f . (g . y) = (f * g) . y ) by FUNCT_2:15; then A4: [[(g . x),(g . y)],[((f * g) . x),((f * g) . y)]] in R by A2; A5: [((f * g) . x),((f * g) . y)] in [:A,A:] by ZFMISC_1:def_2; A6: ( [x,y] in [:A,A:] & [(g . x),(g . y)] in [:A,A:] ) by ZFMISC_1:def_2; [[x,y],[(g . x),(g . y)]] in R by A3; hence [[x,y],[((f * g) . x),((f * g) . y)]] in R by A1, A4, A6, A5; ::_thesis: verum end; theorem Th15: :: TRANSGEO:15 for A being non empty set for f, g being Permutation of A for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R holds f * g is_FormalIz_of R proof let A be non empty set ; ::_thesis: for f, g being Permutation of A for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R holds f * g is_FormalIz_of R let f, g be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R holds f * g is_FormalIz_of R let R be Relation of [:A,A:]; ::_thesis: ( ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R implies f * g is_FormalIz_of R ) assume that A1: for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R and A2: for x, y, z being Element of A holds [[x,x],[y,z]] in R and A3: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R and A4: for x, y being Element of A holds [[x,y],[(g . x),(g . y)]] in R ; :: according to TRANSGEO:def_2 ::_thesis: f * g is_FormalIz_of R let x be Element of A; :: according to TRANSGEO:def_2 ::_thesis: for y being Element of A holds [[x,y],[((f * g) . x),((f * g) . y)]] in R let y be Element of A; ::_thesis: [[x,y],[((f * g) . x),((f * g) . y)]] in R ( f . (g . x) = (f * g) . x & f . (g . y) = (f * g) . y ) by FUNCT_2:15; then A5: [[(g . x),(g . y)],[((f * g) . x),((f * g) . y)]] in R by A3; A6: now__::_thesis:_(_g_._x_=_g_._y_implies_[[x,y],[((f_*_g)_._x),((f_*_g)_._y)]]_in_R_) assume g . x = g . y ; ::_thesis: [[x,y],[((f * g) . x),((f * g) . y)]] in R then x = y by FUNCT_2:58; hence [[x,y],[((f * g) . x),((f * g) . y)]] in R by A2; ::_thesis: verum end; [[x,y],[(g . x),(g . y)]] in R by A4; hence [[x,y],[((f * g) . x),((f * g) . y)]] in R by A1, A5, A6; ::_thesis: verum end; definition let A be non empty set ; let f be Permutation of A; let R be Relation of [:A,A:]; predf is_automorphism_of R means :Def3: :: TRANSGEO:def 3 for x, y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ); end; :: deftheorem Def3 defines is_automorphism_of TRANSGEO:def_3_:_ for A being non empty set for f being Permutation of A for R being Relation of [:A,A:] holds ( f is_automorphism_of R iff for x, y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) ); theorem Th16: :: TRANSGEO:16 for A being non empty set for R being Relation of [:A,A:] holds id A is_automorphism_of R proof let A be non empty set ; ::_thesis: for R being Relation of [:A,A:] holds id A is_automorphism_of R let R be Relation of [:A,A:]; ::_thesis: id A is_automorphism_of R let x be Element of A; :: according to TRANSGEO:def_3 ::_thesis: for y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R ) let y, z, t be Element of A; ::_thesis: ( [[x,y],[z,t]] in R iff [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R ) A1: (id A) . z = z by FUNCT_1:18; A2: ( (id A) . x = x & (id A) . y = y ) by FUNCT_1:18; hence ( [[x,y],[z,t]] in R implies [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R ) by A1, FUNCT_1:18; ::_thesis: ( [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R implies [[x,y],[z,t]] in R ) assume [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R ; ::_thesis: [[x,y],[z,t]] in R hence [[x,y],[z,t]] in R by A2, A1, FUNCT_1:18; ::_thesis: verum end; theorem Th17: :: TRANSGEO:17 for A being non empty set for f being Permutation of A for R being Relation of [:A,A:] st f is_automorphism_of R holds f " is_automorphism_of R proof let A be non empty set ; ::_thesis: for f being Permutation of A for R being Relation of [:A,A:] st f is_automorphism_of R holds f " is_automorphism_of R let f be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st f is_automorphism_of R holds f " is_automorphism_of R let R be Relation of [:A,A:]; ::_thesis: ( f is_automorphism_of R implies f " is_automorphism_of R ) assume A1: for x, y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) ; :: according to TRANSGEO:def_3 ::_thesis: f " is_automorphism_of R let x be Element of A; :: according to TRANSGEO:def_3 ::_thesis: for y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[((f ") . x),((f ") . y)],[((f ") . z),((f ") . t)]] in R ) let y, z, t be Element of A; ::_thesis: ( [[x,y],[z,t]] in R iff [[((f ") . x),((f ") . y)],[((f ") . z),((f ") . t)]] in R ) A2: ( f . ((f ") . z) = z & f . ((f ") . t) = t ) by Th2; ( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2; hence ( [[x,y],[z,t]] in R iff [[((f ") . x),((f ") . y)],[((f ") . z),((f ") . t)]] in R ) by A1, A2; ::_thesis: verum end; theorem Th18: :: TRANSGEO:18 for A being non empty set for f, g being Permutation of A for R being Relation of [:A,A:] st f is_automorphism_of R & g is_automorphism_of R holds g * f is_automorphism_of R proof let A be non empty set ; ::_thesis: for f, g being Permutation of A for R being Relation of [:A,A:] st f is_automorphism_of R & g is_automorphism_of R holds g * f is_automorphism_of R let f, g be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st f is_automorphism_of R & g is_automorphism_of R holds g * f is_automorphism_of R let R be Relation of [:A,A:]; ::_thesis: ( f is_automorphism_of R & g is_automorphism_of R implies g * f is_automorphism_of R ) assume that A1: for x, y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) and A2: for x, y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(g . x),(g . y)],[(g . z),(g . t)]] in R ) ; :: according to TRANSGEO:def_3 ::_thesis: g * f is_automorphism_of R let x be Element of A; :: according to TRANSGEO:def_3 ::_thesis: for y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[((g * f) . x),((g * f) . y)],[((g * f) . z),((g * f) . t)]] in R ) let y, z, t be Element of A; ::_thesis: ( [[x,y],[z,t]] in R iff [[((g * f) . x),((g * f) . y)],[((g * f) . z),((g * f) . t)]] in R ) A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15; A4: ( g . (f . z) = (g * f) . z & g . (f . t) = (g * f) . t ) by FUNCT_2:15; ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) by A1; hence ( [[x,y],[z,t]] in R iff [[((g * f) . x),((g * f) . y)],[((g * f) . z),((g * f) . t)]] in R ) by A2, A3, A4; ::_thesis: verum end; theorem :: TRANSGEO:19 for A being non empty set for f being Permutation of A for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R holds f is_automorphism_of R proof let A be non empty set ; ::_thesis: for f being Permutation of A for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R holds f is_automorphism_of R let f be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R holds f is_automorphism_of R let R be Relation of [:A,A:]; ::_thesis: ( R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R ) assume that A1: for x, y being set st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds [y,x] in R and A2: for x, y, z being set st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds [x,z] in R and A3: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to RELAT_2:def_3,RELAT_2:def_8,TRANSGEO:def_2 ::_thesis: f is_automorphism_of R let x be Element of A; :: according to TRANSGEO:def_3 ::_thesis: for y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) let y, z, t be Element of A; ::_thesis: ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) A4: [z,t] in [:A,A:] by ZFMISC_1:def_2; A5: [(f . z),(f . t)] in [:A,A:] by ZFMISC_1:def_2; A6: [(f . x),(f . y)] in [:A,A:] by ZFMISC_1:def_2; A7: [x,y] in [:A,A:] by ZFMISC_1:def_2; A8: now__::_thesis:_(_[[(f_._x),(f_._y)],[(f_._z),(f_._t)]]_in_R_implies_[[x,y],[z,t]]_in_R_) [[z,t],[(f . z),(f . t)]] in R by A3; then A9: [[(f . z),(f . t)],[z,t]] in R by A1, A4, A5; assume A10: [[(f . x),(f . y)],[(f . z),(f . t)]] in R ; ::_thesis: [[x,y],[z,t]] in R [[x,y],[(f . x),(f . y)]] in R by A3; then [[x,y],[(f . z),(f . t)]] in R by A2, A7, A6, A5, A10; hence [[x,y],[z,t]] in R by A2, A7, A4, A5, A9; ::_thesis: verum end; now__::_thesis:_(_[[x,y],[z,t]]_in_R_implies_[[(f_._x),(f_._y)],[(f_._z),(f_._t)]]_in_R_) [[x,y],[(f . x),(f . y)]] in R by A3; then A11: [[(f . x),(f . y)],[x,y]] in R by A1, A7, A6; A12: [[z,t],[(f . z),(f . t)]] in R by A3; assume [[x,y],[z,t]] in R ; ::_thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R then [[(f . x),(f . y)],[z,t]] in R by A2, A7, A4, A6, A11; hence [[(f . x),(f . y)],[(f . z),(f . t)]] in R by A2, A4, A6, A5, A12; ::_thesis: verum end; hence ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) by A8; ::_thesis: verum end; theorem :: TRANSGEO:20 for A being non empty set for f being Permutation of A for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds f is_automorphism_of R proof let A be non empty set ; ::_thesis: for f being Permutation of A for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds f is_automorphism_of R let f be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds f is_automorphism_of R let R be Relation of [:A,A:]; ::_thesis: ( ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R ) assume that A1: for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds [[x,y],[z,t]] in R and A2: for x, y, z being Element of A holds [[x,x],[y,z]] in R and A3: for x, y being set st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds [y,x] in R and A4: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to RELAT_2:def_3,TRANSGEO:def_2 ::_thesis: f is_automorphism_of R A5: for x, y, z being Element of A holds [[y,z],[x,x]] in R proof let x, y, z be Element of A; ::_thesis: [[y,z],[x,x]] in R A6: ( [y,z] in [:A,A:] & [x,x] in [:A,A:] ) by ZFMISC_1:def_2; [[x,x],[y,z]] in R by A2; hence [[y,z],[x,x]] in R by A3, A6; ::_thesis: verum end; let x be Element of A; :: according to TRANSGEO:def_3 ::_thesis: for y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) let y, z, t be Element of A; ::_thesis: ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) A7: [[x,y],[(f . x),(f . y)]] in R by A4; A8: [[z,t],[(f . z),(f . t)]] in R by A4; ( [z,t] in [:A,A:] & [(f . z),(f . t)] in [:A,A:] ) by ZFMISC_1:def_2; then A9: [[(f . z),(f . t)],[z,t]] in R by A3, A8; A10: now__::_thesis:_(_[[(f_._x),(f_._y)],[(f_._z),(f_._t)]]_in_R_implies_[[x,y],[z,t]]_in_R_) assume A11: [[(f . x),(f . y)],[(f . z),(f . t)]] in R ; ::_thesis: [[x,y],[z,t]] in R A12: now__::_thesis:_(_f_._x_<>_f_._y_&_f_._z_<>_f_._t_implies_[[x,y],[z,t]]_in_R_) assume that A13: f . x <> f . y and A14: f . z <> f . t ; ::_thesis: [[x,y],[z,t]] in R [[x,y],[(f . z),(f . t)]] in R by A1, A7, A11, A13; hence [[x,y],[z,t]] in R by A1, A9, A14; ::_thesis: verum end; A15: now__::_thesis:_(_f_._z_=_f_._t_implies_[[x,y],[z,t]]_in_R_) assume f . z = f . t ; ::_thesis: [[x,y],[z,t]] in R then z = t by FUNCT_2:58; hence [[x,y],[z,t]] in R by A5; ::_thesis: verum end; now__::_thesis:_(_f_._x_=_f_._y_implies_[[x,y],[z,t]]_in_R_) assume f . x = f . y ; ::_thesis: [[x,y],[z,t]] in R then x = y by FUNCT_2:58; hence [[x,y],[z,t]] in R by A2; ::_thesis: verum end; hence [[x,y],[z,t]] in R by A15, A12; ::_thesis: verum end; ( [x,y] in [:A,A:] & [(f . x),(f . y)] in [:A,A:] ) by ZFMISC_1:def_2; then A16: [[(f . x),(f . y)],[x,y]] in R by A3, A7; now__::_thesis:_(_[[x,y],[z,t]]_in_R_implies_[[(f_._x),(f_._y)],[(f_._z),(f_._t)]]_in_R_) assume A17: [[x,y],[z,t]] in R ; ::_thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R now__::_thesis:_(_x_<>_y_&_z_<>_t_implies_[[(f_._x),(f_._y)],[(f_._z),(f_._t)]]_in_R_) assume that A18: x <> y and A19: z <> t ; ::_thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R [[(f . x),(f . y)],[z,t]] in R by A1, A16, A17, A18; hence [[(f . x),(f . y)],[(f . z),(f . t)]] in R by A1, A8, A19; ::_thesis: verum end; hence [[(f . x),(f . y)],[(f . z),(f . t)]] in R by A2, A5; ::_thesis: verum end; hence ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) by A10; ::_thesis: verum end; theorem :: TRANSGEO:21 for A being non empty set for f, g being Permutation of A for R being Relation of [:A,A:] st f is_FormalIz_of R & g is_automorphism_of R holds f \ g is_FormalIz_of R proof let A be non empty set ; ::_thesis: for f, g being Permutation of A for R being Relation of [:A,A:] st f is_FormalIz_of R & g is_automorphism_of R holds f \ g is_FormalIz_of R let f, g be Permutation of A; ::_thesis: for R being Relation of [:A,A:] st f is_FormalIz_of R & g is_automorphism_of R holds f \ g is_FormalIz_of R let R be Relation of [:A,A:]; ::_thesis: ( f is_FormalIz_of R & g is_automorphism_of R implies f \ g is_FormalIz_of R ) assume that A1: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R and A2: for x, y, z, t being Element of A holds ( [[x,y],[z,t]] in R iff [[(g . x),(g . y)],[(g . z),(g . t)]] in R ) ; :: according to TRANSGEO:def_2,TRANSGEO:def_3 ::_thesis: f \ g is_FormalIz_of R let x be Element of A; :: according to TRANSGEO:def_2 ::_thesis: for y being Element of A holds [[x,y],[((f \ g) . x),((f \ g) . y)]] in R let y be Element of A; ::_thesis: [[x,y],[((f \ g) . x),((f \ g) . y)]] in R A3: [[((g ") . x),((g ") . y)],[(f . ((g ") . x)),(f . ((g ") . y))]] in R by A1; ( g . ((g ") . x) = x & g . ((g ") . y) = y ) by Th2; then [[x,y],[(g . (f . ((g ") . x))),(g . (f . ((g ") . y)))]] in R by A2, A3; then [[x,y],[((g * f) . ((g ") . x)),(g . (f . ((g ") . y)))]] in R by FUNCT_2:15; then [[x,y],[((g * f) . ((g ") . x)),((g * f) . ((g ") . y))]] in R by FUNCT_2:15; then [[x,y],[(((g * f) * (g ")) . x),((g * f) . ((g ") . y))]] in R by FUNCT_2:15; hence [[x,y],[((f \ g) . x),((f \ g) . y)]] in R by FUNCT_2:15; ::_thesis: verum end; definition let AS be non empty AffinStruct ; let f be Permutation of the carrier of AS; predf is_DIL_of AS means :Def4: :: TRANSGEO:def 4 f is_FormalIz_of the CONGR of AS; end; :: deftheorem Def4 defines is_DIL_of TRANSGEO:def_4_:_ for AS being non empty AffinStruct for f being Permutation of the carrier of AS holds ( f is_DIL_of AS iff f is_FormalIz_of the CONGR of AS ); theorem Th22: :: TRANSGEO:22 for AS being non empty AffinStruct for f being Permutation of the carrier of AS holds ( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b ) proof let AS be non empty AffinStruct ; ::_thesis: for f being Permutation of the carrier of AS holds ( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b ) let f be Permutation of the carrier of AS; ::_thesis: ( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b ) A1: now__::_thesis:_(_(_for_a,_b_being_Element_of_AS_holds_a,b_//_f_._a,f_._b_)_implies_f_is_DIL_of_AS_) assume A2: for a, b being Element of AS holds a,b // f . a,f . b ; ::_thesis: f is_DIL_of AS for x, y being Element of AS holds [[x,y],[(f . x),(f . y)]] in the CONGR of AS proof let x, y be Element of AS; ::_thesis: [[x,y],[(f . x),(f . y)]] in the CONGR of AS x,y // f . x,f . y by A2; hence [[x,y],[(f . x),(f . y)]] in the CONGR of AS by ANALOAF:def_2; ::_thesis: verum end; then f is_FormalIz_of the CONGR of AS by Def2; hence f is_DIL_of AS by Def4; ::_thesis: verum end; now__::_thesis:_(_f_is_DIL_of_AS_implies_for_a,_b_being_Element_of_AS_holds_a,b_//_f_._a,f_._b_) assume A3: f is_DIL_of AS ; ::_thesis: for a, b being Element of AS holds a,b // f . a,f . b let a, b be Element of AS; ::_thesis: a,b // f . a,f . b f is_FormalIz_of the CONGR of AS by A3, Def4; then [[a,b],[(f . a),(f . b)]] in the CONGR of AS by Def2; hence a,b // f . a,f . b by ANALOAF:def_2; ::_thesis: verum end; hence ( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b ) by A1; ::_thesis: verum end; definition let IT be non empty AffinStruct ; attrIT is CongrSpace-like means :Def5: :: TRANSGEO:def 5 ( ( for x, y, z, t, a, b being Element of IT st x,y // a,b & a,b // z,t & a <> b holds x,y // z,t ) & ( for x, y, z being Element of IT holds x,x // y,z ) & ( for x, y, z, t being Element of IT st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of IT holds x,y // x,y ) ); end; :: deftheorem Def5 defines CongrSpace-like TRANSGEO:def_5_:_ for IT being non empty AffinStruct holds ( IT is CongrSpace-like iff ( ( for x, y, z, t, a, b being Element of IT st x,y // a,b & a,b // z,t & a <> b holds x,y // z,t ) & ( for x, y, z being Element of IT holds x,x // y,z ) & ( for x, y, z, t being Element of IT st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of IT holds x,y // x,y ) ) ); registration cluster non empty strict CongrSpace-like for AffinStruct ; existence ex b1 being non empty AffinStruct st ( b1 is strict & b1 is CongrSpace-like ) proof set OAS = the strict OAffinSpace; A1: ( ( for x, y, z, t being Element of the strict OAffinSpace st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of the strict OAffinSpace holds x,y // x,y ) ) by DIRAF:1, DIRAF:2; ( ( for x, y, z, t, a, b being Element of the strict OAffinSpace st x,y // a,b & a,b // z,t & a <> b holds x,y // z,t ) & ( for x, y, z being Element of the strict OAffinSpace holds x,x // y,z ) ) by DIRAF:3, DIRAF:4; then the strict OAffinSpace is CongrSpace-like by A1, Def5; hence ex b1 being non empty AffinStruct st ( b1 is strict & b1 is CongrSpace-like ) ; ::_thesis: verum end; end; definition mode CongrSpace is non empty CongrSpace-like AffinStruct ; end; Lm3: for CS being CongrSpace holds the CONGR of CS is_reflexive_in [: the carrier of CS, the carrier of CS:] proof let CS be CongrSpace; ::_thesis: the CONGR of CS is_reflexive_in [: the carrier of CS, the carrier of CS:] let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in [: the carrier of CS, the carrier of CS:] or [x,x] in the CONGR of CS ) assume x in [: the carrier of CS, the carrier of CS:] ; ::_thesis: [x,x] in the CONGR of CS then consider x1, x2 being Element of CS such that A1: x = [x1,x2] by DOMAIN_1:1; x1,x2 // x1,x2 by Def5; hence [x,x] in the CONGR of CS by A1, ANALOAF:def_2; ::_thesis: verum end; Lm4: for CS being CongrSpace holds the CONGR of CS is_symmetric_in [: the carrier of CS, the carrier of CS:] proof let CS be CongrSpace; ::_thesis: the CONGR of CS is_symmetric_in [: the carrier of CS, the carrier of CS:] let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in [: the carrier of CS, the carrier of CS:] or not y in [: the carrier of CS, the carrier of CS:] or not [x,y] in the CONGR of CS or [y,x] in the CONGR of CS ) assume that A1: x in [: the carrier of CS, the carrier of CS:] and A2: y in [: the carrier of CS, the carrier of CS:] and A3: [x,y] in the CONGR of CS ; ::_thesis: [y,x] in the CONGR of CS consider x1, x2 being Element of CS such that A4: x = [x1,x2] by A1, DOMAIN_1:1; consider y1, y2 being Element of CS such that A5: y = [y1,y2] by A2, DOMAIN_1:1; x1,x2 // y1,y2 by A3, A4, A5, ANALOAF:def_2; then y1,y2 // x1,x2 by Def5; hence [y,x] in the CONGR of CS by A4, A5, ANALOAF:def_2; ::_thesis: verum end; theorem Th23: :: TRANSGEO:23 for CS being CongrSpace holds id the carrier of CS is_DIL_of CS proof let CS be CongrSpace; ::_thesis: id the carrier of CS is_DIL_of CS id the carrier of CS is_FormalIz_of the CONGR of CS by Lm3, Th12; hence id the carrier of CS is_DIL_of CS by Def4; ::_thesis: verum end; theorem Th24: :: TRANSGEO:24 for CS being CongrSpace for f being Permutation of the carrier of CS st f is_DIL_of CS holds f " is_DIL_of CS proof let CS be CongrSpace; ::_thesis: for f being Permutation of the carrier of CS st f is_DIL_of CS holds f " is_DIL_of CS let f be Permutation of the carrier of CS; ::_thesis: ( f is_DIL_of CS implies f " is_DIL_of CS ) assume f is_DIL_of CS ; ::_thesis: f " is_DIL_of CS then f is_FormalIz_of the CONGR of CS by Def4; then f " is_FormalIz_of the CONGR of CS by Lm4, Th13; hence f " is_DIL_of CS by Def4; ::_thesis: verum end; theorem Th25: :: TRANSGEO:25 for CS being CongrSpace for f, g being Permutation of the carrier of CS st f is_DIL_of CS & g is_DIL_of CS holds f * g is_DIL_of CS proof let CS be CongrSpace; ::_thesis: for f, g being Permutation of the carrier of CS st f is_DIL_of CS & g is_DIL_of CS holds f * g is_DIL_of CS let f, g be Permutation of the carrier of CS; ::_thesis: ( f is_DIL_of CS & g is_DIL_of CS implies f * g is_DIL_of CS ) A1: now__::_thesis:_for_a,_b,_x,_y,_z,_t_being_Element_of_CS_st_[[x,y],[a,b]]_in_the_CONGR_of_CS_&_[[a,b],[z,t]]_in_the_CONGR_of_CS_&_a_<>_b_holds_ [[x,y],[z,t]]_in_the_CONGR_of_CS let a, b, x, y, z, t be Element of CS; ::_thesis: ( [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS & a <> b implies [[x,y],[z,t]] in the CONGR of CS ) assume that A2: ( [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS ) and A3: a <> b ; ::_thesis: [[x,y],[z,t]] in the CONGR of CS ( x,y // a,b & a,b // z,t ) by A2, ANALOAF:def_2; then x,y // z,t by A3, Def5; hence [[x,y],[z,t]] in the CONGR of CS by ANALOAF:def_2; ::_thesis: verum end; A4: now__::_thesis:_for_x,_y,_z_being_Element_of_CS_holds_[[x,x],[y,z]]_in_the_CONGR_of_CS let x, y, z be Element of CS; ::_thesis: [[x,x],[y,z]] in the CONGR of CS x,x // y,z by Def5; hence [[x,x],[y,z]] in the CONGR of CS by ANALOAF:def_2; ::_thesis: verum end; assume ( f is_DIL_of CS & g is_DIL_of CS ) ; ::_thesis: f * g is_DIL_of CS then ( f is_FormalIz_of the CONGR of CS & g is_FormalIz_of the CONGR of CS ) by Def4; then f * g is_FormalIz_of the CONGR of CS by A1, A4, Th15; hence f * g is_DIL_of CS by Def4; ::_thesis: verum end; theorem Th26: :: TRANSGEO:26 for OAS being OAffinSpace holds OAS is CongrSpace-like proof let OAS be OAffinSpace; ::_thesis: OAS is CongrSpace-like thus for x, y, z, t, a, b being Element of OAS st x,y // a,b & a,b // z,t & a <> b holds x,y // z,t by DIRAF:3; :: according to TRANSGEO:def_5 ::_thesis: ( ( for x, y, z being Element of OAS holds x,x // y,z ) & ( for x, y, z, t being Element of OAS st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of OAS holds x,y // x,y ) ) thus for x, y, z being Element of OAS holds x,x // y,z by DIRAF:4; ::_thesis: ( ( for x, y, z, t being Element of OAS st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of OAS holds x,y // x,y ) ) thus for x, y, z, t being Element of OAS st x,y // z,t holds z,t // x,y by DIRAF:2; ::_thesis: for x, y being Element of OAS holds x,y // x,y thus for x, y being Element of OAS holds x,y // x,y by DIRAF:1; ::_thesis: verum end; definition let OAS be OAffinSpace; let f be Permutation of the carrier of OAS; attrf is positive_dilatation means :Def6: :: TRANSGEO:def 6 f is_DIL_of OAS; end; :: deftheorem Def6 defines positive_dilatation TRANSGEO:def_6_:_ for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( f is positive_dilatation iff f is_DIL_of OAS ); theorem Th27: :: TRANSGEO:27 for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS holds ( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b ) A1: now__::_thesis:_(_(_for_a,_b_being_Element_of_OAS_holds_a,b_//_f_._a,f_._b_)_implies_f_is_positive_dilatation_) assume for a, b being Element of OAS holds a,b // f . a,f . b ; ::_thesis: f is positive_dilatation then f is_DIL_of OAS by Th22; hence f is positive_dilatation by Def6; ::_thesis: verum end; now__::_thesis:_(_f_is_positive_dilatation_implies_for_a,_b_being_Element_of_OAS_holds_a,b_//_f_._a,f_._b_) assume f is positive_dilatation ; ::_thesis: for a, b being Element of OAS holds a,b // f . a,f . b then f is_DIL_of OAS by Def6; hence for a, b being Element of OAS holds a,b // f . a,f . b by Th22; ::_thesis: verum end; hence ( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b ) by A1; ::_thesis: verum end; definition let OAS be OAffinSpace; let f be Permutation of the carrier of OAS; attrf is negative_dilatation means :Def7: :: TRANSGEO:def 7 for a, b being Element of OAS holds a,b // f . b,f . a; end; :: deftheorem Def7 defines negative_dilatation TRANSGEO:def_7_:_ for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( f is negative_dilatation iff for a, b being Element of OAS holds a,b // f . b,f . a ); theorem Th28: :: TRANSGEO:28 for OAS being OAffinSpace holds id the carrier of OAS is positive_dilatation proof let OAS be OAffinSpace; ::_thesis: id the carrier of OAS is positive_dilatation OAS is CongrSpace by Th26; then id the carrier of OAS is_DIL_of OAS by Th23; hence id the carrier of OAS is positive_dilatation by Def6; ::_thesis: verum end; theorem :: TRANSGEO:29 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is positive_dilatation holds f " is positive_dilatation proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is positive_dilatation holds f " is positive_dilatation let f be Permutation of the carrier of OAS; ::_thesis: ( f is positive_dilatation implies f " is positive_dilatation ) assume f is positive_dilatation ; ::_thesis: f " is positive_dilatation then A1: f is_DIL_of OAS by Def6; OAS is CongrSpace by Th26; then f " is_DIL_of OAS by A1, Th24; hence f " is positive_dilatation by Def6; ::_thesis: verum end; theorem :: TRANSGEO:30 for OAS being OAffinSpace for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds f * g is positive_dilatation proof let OAS be OAffinSpace; ::_thesis: for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds f * g is positive_dilatation let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is positive_dilatation & g is positive_dilatation implies f * g is positive_dilatation ) assume ( f is positive_dilatation & g is positive_dilatation ) ; ::_thesis: f * g is positive_dilatation then A1: ( f is_DIL_of OAS & g is_DIL_of OAS ) by Def6; OAS is CongrSpace by Th26; then f * g is_DIL_of OAS by A1, Th25; hence f * g is positive_dilatation by Def6; ::_thesis: verum end; theorem :: TRANSGEO:31 for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( not f is negative_dilatation or not f is positive_dilatation ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS holds ( not f is negative_dilatation or not f is positive_dilatation ) given f being Permutation of the carrier of OAS such that A1: ( f is negative_dilatation & f is positive_dilatation ) ; ::_thesis: contradiction consider a, b being Element of OAS such that A2: a <> b by STRUCT_0:def_10; ( a,b // f . a,f . b & a,b // f . b,f . a ) by A1, Def7, Th27; then f . a,f . b // f . b,f . a by A2, ANALOAF:def_5; then f . a = f . b by ANALOAF:def_5; hence contradiction by A2, FUNCT_2:58; ::_thesis: verum end; theorem :: TRANSGEO:32 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is negative_dilatation holds f " is negative_dilatation proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is negative_dilatation holds f " is negative_dilatation let f be Permutation of the carrier of OAS; ::_thesis: ( f is negative_dilatation implies f " is negative_dilatation ) assume A1: f is negative_dilatation ; ::_thesis: f " is negative_dilatation let x be Element of OAS; :: according to TRANSGEO:def_7 ::_thesis: for b being Element of OAS holds x,b // (f ") . b,(f ") . x let y be Element of OAS; ::_thesis: x,y // (f ") . y,(f ") . x set x9 = (f ") . x; set y9 = (f ") . y; ( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2; then (f ") . y,(f ") . x // x,y by A1, Def7; hence x,y // (f ") . y,(f ") . x by DIRAF:2; ::_thesis: verum end; theorem :: TRANSGEO:33 for OAS being OAffinSpace for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is negative_dilatation holds ( f * g is negative_dilatation & g * f is negative_dilatation ) proof let OAS be OAffinSpace; ::_thesis: for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is negative_dilatation holds ( f * g is negative_dilatation & g * f is negative_dilatation ) let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is positive_dilatation & g is negative_dilatation implies ( f * g is negative_dilatation & g * f is negative_dilatation ) ) assume A1: ( f is positive_dilatation & g is negative_dilatation ) ; ::_thesis: ( f * g is negative_dilatation & g * f is negative_dilatation ) thus for x, y being Element of OAS holds x,y // (f * g) . y,(f * g) . x :: according to TRANSGEO:def_7 ::_thesis: g * f is negative_dilatation proof let x, y be Element of OAS; ::_thesis: x,y // (f * g) . y,(f * g) . x set x9 = g . x; set y9 = g . y; A2: ( (f * g) . x = f . (g . x) & (f * g) . y = f . (g . y) ) by FUNCT_2:15; A3: now__::_thesis:_(_g_._x_=_g_._y_implies_x,y_//_(f_*_g)_._y,(f_*_g)_._x_) assume g . x = g . y ; ::_thesis: x,y // (f * g) . y,(f * g) . x then x = y by FUNCT_2:58; hence x,y // (f * g) . y,(f * g) . x by DIRAF:4; ::_thesis: verum end; ( x,y // g . y,g . x & g . y,g . x // f . (g . y),f . (g . x) ) by A1, Def7, Th27; hence x,y // (f * g) . y,(f * g) . x by A2, A3, DIRAF:3; ::_thesis: verum end; thus for x, y being Element of OAS holds x,y // (g * f) . y,(g * f) . x :: according to TRANSGEO:def_7 ::_thesis: verum proof let x, y be Element of OAS; ::_thesis: x,y // (g * f) . y,(g * f) . x set x9 = f . x; set y9 = f . y; A4: ( (g * f) . x = g . (f . x) & (g * f) . y = g . (f . y) ) by FUNCT_2:15; A5: now__::_thesis:_(_f_._x_=_f_._y_implies_x,y_//_(g_*_f)_._y,(g_*_f)_._x_) assume f . x = f . y ; ::_thesis: x,y // (g * f) . y,(g * f) . x then x = y by FUNCT_2:58; hence x,y // (g * f) . y,(g * f) . x by DIRAF:4; ::_thesis: verum end; ( x,y // f . x,f . y & f . x,f . y // g . (f . y),g . (f . x) ) by A1, Def7, Th27; hence x,y // (g * f) . y,(g * f) . x by A4, A5, DIRAF:3; ::_thesis: verum end; end; definition let OAS be OAffinSpace; let f be Permutation of the carrier of OAS; attrf is dilatation means :Def8: :: TRANSGEO:def 8 f is_FormalIz_of lambda the CONGR of OAS; end; :: deftheorem Def8 defines dilatation TRANSGEO:def_8_:_ for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( f is dilatation iff f is_FormalIz_of lambda the CONGR of OAS ); theorem Th34: :: TRANSGEO:34 for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS holds ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b ) A1: now__::_thesis:_(_(_for_a,_b_being_Element_of_OAS_holds_a,b_'||'_f_._a,f_._b_)_implies_f_is_dilatation_) assume A2: for a, b being Element of OAS holds a,b '||' f . a,f . b ; ::_thesis: f is dilatation now__::_thesis:_for_a,_b_being_Element_of_OAS_holds_[[a,b],[(f_._a),(f_._b)]]_in_lambda_the_CONGR_of_OAS let a, b be Element of OAS; ::_thesis: [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS a,b '||' f . a,f . b by A2; hence [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS by DIRAF:18; ::_thesis: verum end; then f is_FormalIz_of lambda the CONGR of OAS by Def2; hence f is dilatation by Def8; ::_thesis: verum end; now__::_thesis:_(_f_is_dilatation_implies_for_a,_b_being_Element_of_OAS_holds_a,b_'||'_f_._a,f_._b_) assume A3: f is dilatation ; ::_thesis: for a, b being Element of OAS holds a,b '||' f . a,f . b let a, b be Element of OAS; ::_thesis: a,b '||' f . a,f . b f is_FormalIz_of lambda the CONGR of OAS by A3, Def8; then [[a,b],[(f . a),(f . b)]] in lambda the CONGR of OAS by Def2; hence a,b '||' f . a,f . b by DIRAF:18; ::_thesis: verum end; hence ( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b ) by A1; ::_thesis: verum end; theorem :: TRANSGEO:35 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st ( f is positive_dilatation or f is negative_dilatation ) holds f is dilatation proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st ( f is positive_dilatation or f is negative_dilatation ) holds f is dilatation let f be Permutation of the carrier of OAS; ::_thesis: ( ( f is positive_dilatation or f is negative_dilatation ) implies f is dilatation ) assume A1: ( f is positive_dilatation or f is negative_dilatation ) ; ::_thesis: f is dilatation now__::_thesis:_for_x,_y_being_Element_of_OAS_holds_x,y_'||'_f_._x,f_._y let x, y be Element of OAS; ::_thesis: x,y '||' f . x,f . y ( x,y // f . x,f . y or x,y // f . y,f . x ) by A1, Def7, Th27; hence x,y '||' f . x,f . y by DIRAF:def_4; ::_thesis: verum end; hence f is dilatation by Th34; ::_thesis: verum end; theorem :: TRANSGEO:36 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is dilatation holds ex f9 being Permutation of the carrier of (Lambda OAS) st ( f = f9 & f9 is_DIL_of Lambda OAS ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation holds ex f9 being Permutation of the carrier of (Lambda OAS) st ( f = f9 & f9 is_DIL_of Lambda OAS ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation implies ex f9 being Permutation of the carrier of (Lambda OAS) st ( f = f9 & f9 is_DIL_of Lambda OAS ) ) A1: Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def_2; then reconsider f9 = f as Permutation of the carrier of (Lambda OAS) ; assume f is dilatation ; ::_thesis: ex f9 being Permutation of the carrier of (Lambda OAS) st ( f = f9 & f9 is_DIL_of Lambda OAS ) then A2: f is_FormalIz_of lambda the CONGR of OAS by Def8; take f9 ; ::_thesis: ( f = f9 & f9 is_DIL_of Lambda OAS ) thus ( f = f9 & f9 is_DIL_of Lambda OAS ) by A2, A1, Def4; ::_thesis: verum end; theorem :: TRANSGEO:37 for OAS being OAffinSpace for f being Permutation of the carrier of (Lambda OAS) st f is_DIL_of Lambda OAS holds ex f9 being Permutation of the carrier of OAS st ( f = f9 & f9 is dilatation ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of (Lambda OAS) st f is_DIL_of Lambda OAS holds ex f9 being Permutation of the carrier of OAS st ( f = f9 & f9 is dilatation ) let f be Permutation of the carrier of (Lambda OAS); ::_thesis: ( f is_DIL_of Lambda OAS implies ex f9 being Permutation of the carrier of OAS st ( f = f9 & f9 is dilatation ) ) A1: Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def_2; then reconsider f9 = f as Permutation of the carrier of OAS ; assume f is_DIL_of Lambda OAS ; ::_thesis: ex f9 being Permutation of the carrier of OAS st ( f = f9 & f9 is dilatation ) then A2: f is_FormalIz_of the CONGR of (Lambda OAS) by Def4; take f9 ; ::_thesis: ( f = f9 & f9 is dilatation ) thus ( f = f9 & f9 is dilatation ) by A2, A1, Def8; ::_thesis: verum end; theorem :: TRANSGEO:38 for OAS being OAffinSpace holds id the carrier of OAS is dilatation proof let OAS be OAffinSpace; ::_thesis: id the carrier of OAS is dilatation now__::_thesis:_for_x,_y_being_Element_of_OAS_holds_x,y_'||'_(id_the_carrier_of_OAS)_._x,(id_the_carrier_of_OAS)_._y let x, y be Element of OAS; ::_thesis: x,y '||' (id the carrier of OAS) . x,(id the carrier of OAS) . y ( (id the carrier of OAS) . x = x & (id the carrier of OAS) . y = y ) by FUNCT_1:18; hence x,y '||' (id the carrier of OAS) . x,(id the carrier of OAS) . y by DIRAF:19; ::_thesis: verum end; hence id the carrier of OAS is dilatation by Th34; ::_thesis: verum end; theorem Th39: :: TRANSGEO:39 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is dilatation holds f " is dilatation proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation holds f " is dilatation let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation implies f " is dilatation ) assume A1: f is dilatation ; ::_thesis: f " is dilatation now__::_thesis:_for_x,_y_being_Element_of_OAS_holds_x,y_'||'_(f_")_._x,(f_")_._y let x, y be Element of OAS; ::_thesis: x,y '||' (f ") . x,(f ") . y set x9 = (f ") . x; set y9 = (f ") . y; ( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2; then (f ") . x,(f ") . y '||' x,y by A1, Th34; hence x,y '||' (f ") . x,(f ") . y by DIRAF:22; ::_thesis: verum end; hence f " is dilatation by Th34; ::_thesis: verum end; theorem Th40: :: TRANSGEO:40 for OAS being OAffinSpace for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation holds f * g is dilatation proof let OAS be OAffinSpace; ::_thesis: for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation holds f * g is dilatation let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & g is dilatation implies f * g is dilatation ) assume A1: ( f is dilatation & g is dilatation ) ; ::_thesis: f * g is dilatation now__::_thesis:_for_x,_y_being_Element_of_OAS_holds_x,y_'||'_(f_*_g)_._x,(f_*_g)_._y let x, y be Element of OAS; ::_thesis: x,y '||' (f * g) . x,(f * g) . y set x9 = g . x; set y9 = g . y; A2: ( (f * g) . x = f . (g . x) & (f * g) . y = f . (g . y) ) by FUNCT_2:15; A3: now__::_thesis:_(_g_._x_=_g_._y_implies_x,y_'||'_(f_*_g)_._x,(f_*_g)_._y_) assume g . x = g . y ; ::_thesis: x,y '||' (f * g) . x,(f * g) . y then x = y by FUNCT_2:58; hence x,y '||' (f * g) . x,(f * g) . y by DIRAF:20; ::_thesis: verum end; ( x,y '||' g . x,g . y & g . x,g . y '||' f . (g . x),f . (g . y) ) by A1, Th34; hence x,y '||' (f * g) . x,(f * g) . y by A2, A3, DIRAF:23; ::_thesis: verum end; hence f * g is dilatation by Th34; ::_thesis: verum end; theorem Th41: :: TRANSGEO:41 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is dilatation holds for a, b, c, d being Element of OAS holds ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation holds for a, b, c, d being Element of OAS holds ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation implies for a, b, c, d being Element of OAS holds ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) ) assume A1: f is dilatation ; ::_thesis: for a, b, c, d being Element of OAS holds ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) let a, b, c, d be Element of OAS; ::_thesis: ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) A2: c,d '||' f . c,f . d by A1, Th34; A3: a,b '||' f . a,f . b by A1, Th34; A4: now__::_thesis:_(_f_._a,f_._b_'||'_f_._c,f_._d_implies_a,b_'||'_c,d_) A5: now__::_thesis:_(_a,b_'||'_f_._c,f_._d_implies_a,b_'||'_c,d_) A6: now__::_thesis:_(_f_._c_=_f_._d_implies_a,b_'||'_c,d_) assume f . c = f . d ; ::_thesis: a,b '||' c,d then c = d by FUNCT_2:58; hence a,b '||' c,d by DIRAF:20; ::_thesis: verum end; assume a,b '||' f . c,f . d ; ::_thesis: a,b '||' c,d hence a,b '||' c,d by A2, A6, DIRAF:23; ::_thesis: verum end; A7: now__::_thesis:_(_f_._a_=_f_._b_implies_a,b_'||'_c,d_) assume f . a = f . b ; ::_thesis: a,b '||' c,d then a = b by FUNCT_2:58; hence a,b '||' c,d by DIRAF:20; ::_thesis: verum end; assume f . a,f . b '||' f . c,f . d ; ::_thesis: a,b '||' c,d hence a,b '||' c,d by A3, A7, A5, DIRAF:23; ::_thesis: verum end; now__::_thesis:_(_a,b_'||'_c,d_implies_f_._a,f_._b_'||'_f_._c,f_._d_) A8: now__::_thesis:_(_f_._a,f_._b_'||'_c,d_implies_f_._a,f_._b_'||'_f_._c,f_._d_) A9: ( c = d implies f . a,f . b '||' f . c,f . d ) by DIRAF:20; assume f . a,f . b '||' c,d ; ::_thesis: f . a,f . b '||' f . c,f . d hence f . a,f . b '||' f . c,f . d by A2, A9, DIRAF:23; ::_thesis: verum end; assume a,b '||' c,d ; ::_thesis: f . a,f . b '||' f . c,f . d then ( f . a,f . b '||' c,d or a = b ) by A3, DIRAF:23; hence f . a,f . b '||' f . c,f . d by A8, DIRAF:20; ::_thesis: verum end; hence ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) by A4; ::_thesis: verum end; theorem Th42: :: TRANSGEO:42 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is dilatation holds for a, b, c being Element of OAS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation holds for a, b, c being Element of OAS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation implies for a, b, c being Element of OAS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) ) assume A1: f is dilatation ; ::_thesis: for a, b, c being Element of OAS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) let a, b, c be Element of OAS; ::_thesis: ( LIN a,b,c iff LIN f . a,f . b,f . c ) ( a,b '||' a,c iff f . a,f . b '||' f . a,f . c ) by A1, Th41; hence ( LIN a,b,c iff LIN f . a,f . b,f . c ) by DIRAF:def_5; ::_thesis: verum end; theorem Th43: :: TRANSGEO:43 for OAS being OAffinSpace for x, y being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & LIN x,f . x,y holds LIN x,f . x,f . y proof let OAS be OAffinSpace; ::_thesis: for x, y being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & LIN x,f . x,y holds LIN x,f . x,f . y let x, y be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & LIN x,f . x,y holds LIN x,f . x,f . y let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & LIN x,f . x,y implies LIN x,f . x,f . y ) assume A1: f is dilatation ; ::_thesis: ( not LIN x,f . x,y or LIN x,f . x,f . y ) assume A2: LIN x,f . x,y ; ::_thesis: LIN x,f . x,f . y now__::_thesis:_(_x_<>_y_implies_LIN_x,f_._x,f_._y_) assume A3: x <> y ; ::_thesis: LIN x,f . x,f . y ( x,f . x '||' x,y & x,y '||' f . x,f . y ) by A1, A2, Th34, DIRAF:def_5; then x,f . x '||' f . x,f . y by A3, DIRAF:23; then f . x,x '||' f . x,f . y by DIRAF:22; then LIN f . x,x,f . y by DIRAF:def_5; hence LIN x,f . x,f . y by DIRAF:30; ::_thesis: verum end; hence LIN x,f . x,f . y by DIRAF:31; ::_thesis: verum end; theorem Th44: :: TRANSGEO:44 for OAS being OAffinSpace for a, b, c, d being Element of OAS holds ( not a,b '||' c,d or a,c '||' b,d or ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) ) proof let OAS be OAffinSpace; ::_thesis: for a, b, c, d being Element of OAS holds ( not a,b '||' c,d or a,c '||' b,d or ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) ) let a, b, c, d be Element of OAS; ::_thesis: ( not a,b '||' c,d or a,c '||' b,d or ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) ) assume A1: a,b '||' c,d ; ::_thesis: ( a,c '||' b,d or ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) ) assume A2: not a,c '||' b,d ; ::_thesis: ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) A3: now__::_thesis:_(_a_<>_b_implies_ex_x_being_Element_of_OAS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) consider z being Element of OAS such that A4: a,b '||' c,z and A5: a,c '||' b,z by DIRAF:26; assume A6: a <> b ; ::_thesis: ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) A7: now__::_thesis:_(_b_<>_z_implies_ex_x_being_Element_of_OAS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) c,d '||' c,z by A1, A6, A4, DIRAF:23; then LIN c,d,z by DIRAF:def_5; then LIN d,c,z by DIRAF:30; then d,c '||' d,z by DIRAF:def_5; then z,d '||' d,c by DIRAF:22; then consider t being Element of OAS such that A8: b,d '||' d,t and A9: b,z '||' c,t by A2, A5, DIRAF:27; assume b <> z ; ::_thesis: ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) then a,c '||' c,t by A5, A9, DIRAF:23; then c,a '||' c,t by DIRAF:22; then LIN c,a,t by DIRAF:def_5; then A10: LIN a,c,t by DIRAF:30; d,b '||' d,t by A8, DIRAF:22; then LIN d,b,t by DIRAF:def_5; then LIN b,d,t by DIRAF:30; hence ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) by A10; ::_thesis: verum end; now__::_thesis:_(_b_=_z_implies_ex_x_being_Element_of_OAS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) assume b = z ; ::_thesis: ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) then b,a '||' b,c by A4, DIRAF:22; then LIN b,a,c by DIRAF:def_5; then A11: LIN a,c,b by DIRAF:30; LIN b,d,b by DIRAF:31; hence ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) by A11; ::_thesis: verum end; hence ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) by A7; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_ex_x_being_Element_of_OAS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) assume a = b ; ::_thesis: ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) then ( LIN a,c,a & LIN b,d,a ) by DIRAF:31; hence ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) ; ::_thesis: verum end; hence ex x being Element of OAS st ( LIN a,c,x & LIN b,d,x ) by A3; ::_thesis: verum end; theorem Th45: :: TRANSGEO:45 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is dilatation holds ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation holds ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation implies ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) ) assume A1: f is dilatation ; ::_thesis: ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) A2: now__::_thesis:_(_(_for_x,_y_being_Element_of_OAS_holds_x,f_._x_'||'_y,f_._y_)_&_f_<>_id_the_carrier_of_OAS_implies_for_x_being_Element_of_OAS_holds_not_f_._x_=_x_) assume A3: for x, y being Element of OAS holds x,f . x '||' y,f . y ; ::_thesis: ( f <> id the carrier of OAS implies for x being Element of OAS holds not f . x = x ) assume f <> id the carrier of OAS ; ::_thesis: for x being Element of OAS holds not f . x = x then consider y being Element of OAS such that A4: f . y <> (id the carrier of OAS) . y by FUNCT_2:63; given x being Element of OAS such that A5: f . x = x ; ::_thesis: contradiction x <> y by A5, A4, FUNCT_1:18; then consider z being Element of OAS such that A6: not LIN x,y,z by DIRAF:37; x,z '||' f . x,f . z by A1, Th34; then LIN x,z,f . z by A5, DIRAF:def_5; then A7: LIN z,f . z,x by DIRAF:30; LIN z,f . z,z by DIRAF:31; then A8: z,f . z '||' x,z by A7, DIRAF:34; A9: f . y <> y by A4, FUNCT_1:18; x,y '||' f . x,f . y by A1, Th34; then A10: LIN x,y,f . y by A5, DIRAF:def_5; then LIN y,x,f . y by DIRAF:30; then A11: y,x '||' y,f . y by DIRAF:def_5; A12: LIN y,f . y,x by A10, DIRAF:30; A13: now__::_thesis:_not_z_=_f_._z assume z = f . z ; ::_thesis: contradiction then z,y '||' z,f . y by A1, Th34; then LIN z,y,f . y by DIRAF:def_5; then ( LIN y,f . y,y & LIN y,f . y,z ) by DIRAF:30, DIRAF:31; hence contradiction by A9, A12, A6, DIRAF:32; ::_thesis: verum end; y,f . y '||' z,f . z by A3; then y,f . y '||' x,z by A13, A8, DIRAF:23; then y,x '||' x,z by A9, A11, DIRAF:23; then x,y '||' x,z by DIRAF:22; hence contradiction by A6, DIRAF:def_5; ::_thesis: verum end; now__::_thesis:_(_(_f_=_id_the_carrier_of_OAS_or_for_z_being_Element_of_OAS_holds_f_._z_<>_z_)_implies_for_x,_y_being_Element_of_OAS_holds_x,f_._x_'||'_y,f_._y_) assume A14: ( f = id the carrier of OAS or for z being Element of OAS holds f . z <> z ) ; ::_thesis: for x, y being Element of OAS holds x,f . x '||' y,f . y let x, y be Element of OAS; ::_thesis: x,f . x '||' y,f . y A15: x,y '||' f . x,f . y by A1, Th34; A16: now__::_thesis:_(_(_for_z_being_Element_of_OAS_holds_f_._z_<>_z_)_implies_x,f_._x_'||'_y,f_._y_) assume A17: for z being Element of OAS holds f . z <> z ; ::_thesis: x,f . x '||' y,f . y assume A18: not x,f . x '||' y,f . y ; ::_thesis: contradiction then consider z being Element of OAS such that A19: LIN x,f . x,z and A20: LIN y,f . y,z by A15, Th44; set t = f . z; LIN x,f . x,f . z by A1, A19, Th43; then A21: x,f . x '||' z,f . z by A19, DIRAF:34; LIN y,f . y,f . z by A1, A20, Th43; then A22: y,f . y '||' z,f . z by A20, DIRAF:34; z <> f . z by A17; hence contradiction by A18, A21, A22, DIRAF:23; ::_thesis: verum end; now__::_thesis:_(_f_=_id_the_carrier_of_OAS_implies_x,f_._x_'||'_y,f_._y_) assume f = id the carrier of OAS ; ::_thesis: x,f . x '||' y,f . y then f . y = y by FUNCT_1:18; hence x,f . x '||' y,f . y by DIRAF:20; ::_thesis: verum end; hence x,f . x '||' y,f . y by A14, A16; ::_thesis: verum end; hence ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) by A2; ::_thesis: verum end; theorem Th46: :: TRANSGEO:46 for OAS being OAffinSpace for a, b, x being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds f . x = x proof let OAS be OAffinSpace; ::_thesis: for a, b, x being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds f . x = x let a, b, x be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds f . x = x let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . a = a & f . b = b & not LIN a,b,x implies f . x = x ) assume that A1: f is dilatation and A2: f . a = a and A3: f . b = b and A4: not LIN a,b,x ; ::_thesis: f . x = x a,x '||' a,f . x by A1, A2, Th34; then LIN a,x,f . x by DIRAF:def_5; then A5: LIN x,f . x,a by DIRAF:30; b,x '||' b,f . x by A1, A3, Th34; then LIN b,x,f . x by DIRAF:def_5; then A6: ( LIN x,f . x,x & LIN x,f . x,b ) by DIRAF:30, DIRAF:31; assume f . x <> x ; ::_thesis: contradiction hence contradiction by A4, A5, A6, DIRAF:32; ::_thesis: verum end; theorem Th47: :: TRANSGEO:47 for OAS being OAffinSpace for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds f = id the carrier of OAS proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds f = id the carrier of OAS let a, b be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds f = id the carrier of OAS let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . a = a & f . b = b & a <> b implies f = id the carrier of OAS ) assume that A1: f is dilatation and A2: f . a = a and A3: f . b = b and A4: a <> b ; ::_thesis: f = id the carrier of OAS now__::_thesis:_for_x_being_Element_of_OAS_holds_f_._x_=_(id_the_carrier_of_OAS)_._x let x be Element of OAS; ::_thesis: f . x = (id the carrier of OAS) . x A5: now__::_thesis:_(_LIN_a,b,x_implies_f_._x_=_x_) assume A6: LIN a,b,x ; ::_thesis: f . x = x now__::_thesis:_(_x_<>_a_implies_f_._x_=_x_) consider z being Element of OAS such that A7: not LIN a,b,z by A4, DIRAF:37; assume A8: x <> a ; ::_thesis: f . x = x A9: not LIN a,z,x proof assume LIN a,z,x ; ::_thesis: contradiction then A10: LIN a,x,z by DIRAF:30; ( LIN a,x,a & LIN a,x,b ) by A6, DIRAF:30, DIRAF:31; hence contradiction by A8, A7, A10, DIRAF:32; ::_thesis: verum end; f . z = z by A1, A2, A3, A7, Th46; hence f . x = x by A1, A2, A9, Th46; ::_thesis: verum end; hence f . x = x by A2; ::_thesis: verum end; ( not LIN a,b,x implies f . x = x ) by A1, A2, A3, Th46; hence f . x = (id the carrier of OAS) . x by A5, FUNCT_1:18; ::_thesis: verum end; hence f = id the carrier of OAS by FUNCT_2:63; ::_thesis: verum end; theorem :: TRANSGEO:48 for OAS being OAffinSpace for a, b being Element of OAS for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds f = g proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds f = g let a, b be Element of OAS; ::_thesis: for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds f = g let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b implies f = g ) assume that A1: f is dilatation and A2: g is dilatation and A3: f . a = g . a and A4: f . b = g . b ; ::_thesis: ( a = b or f = g ) A5: ((g ") * f) . b = (g ") . (g . b) by A4, FUNCT_2:15 .= b by Th2 ; A6: g " is dilatation by A2, Th39; assume A7: a <> b ; ::_thesis: f = g ((g ") * f) . a = (g ") . (g . a) by A3, FUNCT_2:15 .= a by Th2 ; then A8: (g ") * f = id the carrier of OAS by A1, A7, A5, A6, Th40, Th47; now__::_thesis:_for_x_being_Element_of_OAS_holds_g_._x_=_f_._x let x be Element of OAS; ::_thesis: g . x = f . x (g ") . (f . x) = ((g ") * f) . x by FUNCT_2:15; then (g ") . (f . x) = x by A8, FUNCT_1:18; hence g . x = f . x by Th2; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; definition let OAS be OAffinSpace; let f be Permutation of the carrier of OAS; attrf is translation means :Def9: :: TRANSGEO:def 9 ( f is dilatation & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) ); end; :: deftheorem Def9 defines translation TRANSGEO:def_9_:_ for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( f is translation iff ( f is dilatation & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) ) ); theorem Th49: :: TRANSGEO:49 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is dilatation holds ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation holds ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation implies ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) ) assume A1: f is dilatation ; ::_thesis: ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) then ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) by Th45; hence ( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) by A1, Def9; ::_thesis: verum end; theorem Th50: :: TRANSGEO:50 for OAS being OAffinSpace for a, x being Element of OAS for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds f . x = g . x proof let OAS be OAffinSpace; ::_thesis: for a, x being Element of OAS for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds f . x = g . x let a, x be Element of OAS; ::_thesis: for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds f . x = g . x let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is translation & g is translation & f . a = g . a & not LIN a,f . a,x implies f . x = g . x ) assume that A1: f is translation and A2: g is translation and A3: f . a = g . a and A4: not LIN a,f . a,x ; ::_thesis: f . x = g . x set b = f . a; set y = f . x; set z = g . x; g is dilatation by A2, Def9; then A5: ( a,x '||' f . a,g . x & a,f . a '||' x,g . x ) by A2, A3, Th34, Th49; A6: f is dilatation by A1, Def9; then A7: a,x '||' f . a,f . x by Th34; a,f . a '||' x,f . x by A1, A6, Th49; hence f . x = g . x by A4, A7, A5, PASCH:5; ::_thesis: verum end; theorem Th51: :: TRANSGEO:51 for OAS being OAffinSpace for a being Element of OAS for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds f = g proof let OAS be OAffinSpace; ::_thesis: for a being Element of OAS for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds f = g let a be Element of OAS; ::_thesis: for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds f = g let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is translation & g is translation & f . a = g . a implies f = g ) assume that A1: f is translation and A2: g is translation and A3: f . a = g . a ; ::_thesis: f = g set b = f . a; A4: f is dilatation by A1, Def9; A5: now__::_thesis:_(_a_<>_f_._a_implies_f_=_g_) assume A6: a <> f . a ; ::_thesis: f = g for x being Element of OAS holds f . x = g . x proof let x be Element of OAS; ::_thesis: f . x = g . x now__::_thesis:_(_LIN_a,f_._a,x_implies_f_._x_=_g_._x_) assume A7: LIN a,f . a,x ; ::_thesis: f . x = g . x now__::_thesis:_(_x_<>_a_implies_f_._x_=_g_._x_) A8: f <> id the carrier of OAS by A6, FUNCT_1:18; then A9: f . x <> x by A1, Def9; assume x <> a ; ::_thesis: f . x = g . x consider p being Element of OAS such that A10: not LIN a,f . a,p by A6, DIRAF:37; A11: f . p <> p by A1, A8, Def9; A12: not LIN p,f . p,x proof A13: LIN a,f . a,f . x by A4, A7, Th43; LIN a,f . a,a by DIRAF:31; then A14: LIN x,f . x,a by A6, A7, A13, DIRAF:32; A15: LIN p,f . p,p by DIRAF:31; LIN a,f . a,f . a by DIRAF:31; then A16: LIN x,f . x,f . a by A6, A7, A13, DIRAF:32; assume A17: LIN p,f . p,x ; ::_thesis: contradiction then LIN p,f . p,f . x by A4, Th43; then LIN x,f . x,p by A11, A17, A15, DIRAF:32; hence contradiction by A10, A9, A14, A16, DIRAF:32; ::_thesis: verum end; f . p = g . p by A1, A2, A3, A10, Th50; hence f . x = g . x by A1, A2, A12, Th50; ::_thesis: verum end; hence f . x = g . x by A3; ::_thesis: verum end; hence f . x = g . x by A1, A2, A3, Th50; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; now__::_thesis:_(_f_._a_=_a_implies_f_=_g_) assume A18: f . a = a ; ::_thesis: f = g then f = id the carrier of OAS by A1, Def9; hence f = g by A2, A3, A18, Def9; ::_thesis: verum end; hence f = g by A5; ::_thesis: verum end; theorem Th52: :: TRANSGEO:52 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is translation holds f " is translation proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is translation holds f " is translation let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation implies f " is translation ) A1: now__::_thesis:_(_(_for_x_being_Element_of_OAS_holds_f_._x_<>_x_)_implies_for_y_being_Element_of_OAS_holds_not_(f_")_._y_=_y_) assume A2: for x being Element of OAS holds f . x <> x ; ::_thesis: for y being Element of OAS holds not (f ") . y = y given y being Element of OAS such that A3: (f ") . y = y ; ::_thesis: contradiction f . y = y by A3, Th2; hence contradiction by A2; ::_thesis: verum end; assume A4: f is translation ; ::_thesis: f " is translation then f is dilatation by Def9; then A5: f " is dilatation by Th39; ( f = id the carrier of OAS implies f " = id the carrier of OAS ) by FUNCT_1:45; hence f " is translation by A4, A5, A1, Def9; ::_thesis: verum end; theorem :: TRANSGEO:53 for OAS being OAffinSpace for f, g being Permutation of the carrier of OAS st f is translation & g is translation holds f * g is translation proof let OAS be OAffinSpace; ::_thesis: for f, g being Permutation of the carrier of OAS st f is translation & g is translation holds f * g is translation let f, g be Permutation of the carrier of OAS; ::_thesis: ( f is translation & g is translation implies f * g is translation ) assume that A1: f is translation and A2: g is translation ; ::_thesis: f * g is translation ( f is dilatation & g is dilatation ) by A1, A2, Def9; then A3: f * g is dilatation by Th40; now__::_thesis:_(_f_*_g_<>_id_the_carrier_of_OAS_implies_f_*_g_is_translation_) assume A4: f * g <> id the carrier of OAS ; ::_thesis: f * g is translation for x being Element of OAS holds (f * g) . x <> x proof given x being Element of OAS such that A5: (f * g) . x = x ; ::_thesis: contradiction f . (g . x) = x by A5, FUNCT_2:15; then A6: g . x = (f ") . x by Th2; f " is translation by A1, Th52; then f * g = f * (f ") by A2, A6, Th51; hence contradiction by A4, FUNCT_2:61; ::_thesis: verum end; hence f * g is translation by A3, Def9; ::_thesis: verum end; hence f * g is translation by A3, Def9; ::_thesis: verum end; Lm5: for OAS being OAffinSpace for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & not LIN a,f . a,b holds ( a,b // f . a,f . b & a,f . a // b,f . b ) proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & not LIN a,f . a,b holds ( a,b // f . a,f . b & a,f . a // b,f . b ) let a, b be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is translation & not LIN a,f . a,b holds ( a,b // f . a,f . b & a,f . a // b,f . b ) let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation & not LIN a,f . a,b implies ( a,b // f . a,f . b & a,f . a // b,f . b ) ) assume that A1: f is translation and A2: not LIN a,f . a,b ; ::_thesis: ( a,b // f . a,f . b & a,f . a // b,f . b ) A3: f is dilatation by A1, Def9; then A4: a,b '||' f . a,f . b by Th34; a,f . a '||' b,f . b by A1, A3, Th49; hence ( a,b // f . a,f . b & a,f . a // b,f . b ) by A2, A4, PASCH:14; ::_thesis: verum end; Lm6: for OAS being OAffinSpace for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds a,f . a // b,f . b proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds a,f . a // b,f . b let a, b be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds a,f . a // b,f . b let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation & a <> f . a & LIN a,f . a,b implies a,f . a // b,f . b ) assume that A1: f is translation and A2: a <> f . a and A3: LIN a,f . a,b ; ::_thesis: a,f . a // b,f . b consider p being Element of OAS such that A4: not LIN a,f . a,p by A2, DIRAF:37; A5: f is dilatation by A1, Def9; A6: f <> id the carrier of OAS by A2, FUNCT_1:18; then A7: p <> f . p by A1, Def9; A8: b <> f . b by A1, A6, Def9; not LIN p,f . p,b proof A9: LIN p,f . p,p by DIRAF:31; assume A10: LIN p,f . p,b ; ::_thesis: contradiction then LIN p,f . p,f . b by A5, Th43; then A11: LIN b,f . b,p by A7, A10, A9, DIRAF:32; ( LIN a,f . a,f . b & LIN a,f . a,a ) by A3, A5, Th43, DIRAF:31; then A12: LIN b,f . b,a by A2, A3, DIRAF:32; then LIN b,f . b,f . a by A5, Th43; hence contradiction by A4, A8, A12, A11, DIRAF:32; ::_thesis: verum end; then A13: p,f . p // b,f . b by A1, Lm5; not LIN p,f . p,a proof assume A14: LIN p,f . p,a ; ::_thesis: contradiction then ( LIN p,f . p,p & LIN p,f . p,f . a ) by A5, Th43, DIRAF:31; hence contradiction by A4, A7, A14, DIRAF:32; ::_thesis: verum end; then p,f . p // a,f . a by A1, Lm5; hence a,f . a // b,f . b by A7, A13, ANALOAF:def_5; ::_thesis: verum end; Lm7: for OAS being OAffinSpace for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & Mid a,f . a,b & a <> f . a holds a,b // f . a,f . b proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & Mid a,f . a,b & a <> f . a holds a,b // f . a,f . b let a, b be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is translation & Mid a,f . a,b & a <> f . a holds a,b // f . a,f . b let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation & Mid a,f . a,b & a <> f . a implies a,b // f . a,f . b ) assume that A1: f is translation and A2: Mid a,f . a,b and A3: a <> f . a ; ::_thesis: a,b // f . a,f . b A4: a,f . a // b,f . b by A1, A2, A3, Lm6, DIRAF:28; now__::_thesis:_(_b_<>_f_._a_implies_a,b_//_f_._a,f_._b_) Mid b,f . a,a by A2, DIRAF:9; then b,f . a // f . a,a by DIRAF:def_3; then b,f . a // b,a by ANALOAF:def_5; then A5: a,b // f . a,b by DIRAF:2; a,f . a // f . a,b by A2, DIRAF:def_3; then f . a,b // b,f . b by A3, A4, ANALOAF:def_5; then A6: f . a,b // f . a,f . b by ANALOAF:def_5; assume b <> f . a ; ::_thesis: a,b // f . a,f . b hence a,b // f . a,f . b by A5, A6, DIRAF:3; ::_thesis: verum end; hence a,b // f . a,f . b by A1, A2, A3, Lm6, DIRAF:28; ::_thesis: verum end; Lm8: for OAS being OAffinSpace for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & a <> f . a & b <> f . a & Mid a,b,f . a holds a,b // f . a,f . b proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & a <> f . a & b <> f . a & Mid a,b,f . a holds a,b // f . a,f . b let a, b be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & b <> f . a & Mid a,b,f . a holds a,b // f . a,f . b let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation & a <> f . a & b <> f . a & Mid a,b,f . a implies a,b // f . a,f . b ) assume that A1: f is translation and A2: a <> f . a and A3: b <> f . a and A4: Mid a,b,f . a ; ::_thesis: a,b // f . a,f . b A5: a,b // b,f . a by A4, DIRAF:def_3; A6: f is dilatation by A1, Def9; A7: LIN a,b,f . a by A4, DIRAF:28; then A8: LIN a,f . a,b by DIRAF:30; A9: f <> id the carrier of OAS by A2, FUNCT_1:18; now__::_thesis:_(_a_<>_b_implies_a,b_//_f_._a,f_._b_) assume A10: a <> b ; ::_thesis: a,b // f . a,f . b A11: now__::_thesis:_not_a,b_//_f_._b,f_._a LIN f . a,a,b by A7, DIRAF:30; then f . a,a '||' f . a,b by DIRAF:def_5; then A12: a,f . a '||' b,f . a by DIRAF:22; consider q being Element of OAS such that A13: not LIN a,f . a,q by A2, DIRAF:37; consider x being Element of OAS such that A14: q,b // b,x and A15: q,a // f . a,x by A5, A10, ANALOAF:def_5; A16: a,q // x,f . a by A15, DIRAF:2; A17: Mid q,b,x by A14, DIRAF:def_3; then A18: LIN x,b,q by DIRAF:9, DIRAF:28; A19: x <> f . a proof assume x = f . a ; ::_thesis: contradiction then Mid q,b,f . a by A14, DIRAF:def_3; then LIN q,b,f . a by DIRAF:28; then A20: LIN f . a,b,q by DIRAF:30; A21: LIN a,b,a by DIRAF:31; ( LIN f . a,b,a & LIN f . a,b,b ) by A7, DIRAF:30, DIRAF:31; then LIN a,b,q by A3, A20, DIRAF:32; hence contradiction by A7, A10, A13, A21, DIRAF:32; ::_thesis: verum end; A22: not LIN x,f . a,b proof assume LIN x,f . a,b ; ::_thesis: contradiction then LIN f . a,x,b by DIRAF:30; then A23: f . a,x '||' f . a,b by DIRAF:def_5; LIN f . a,b,a by A7, DIRAF:30; then A24: f . a,b '||' f . a,a by DIRAF:def_5; q,a '||' f . a,x by A15, DIRAF:def_4; then f . a,b '||' q,a by A19, A23, DIRAF:23; then f . a,a '||' q,a by A3, A24, DIRAF:23; then a,f . a '||' a,q by DIRAF:22; hence contradiction by A13, DIRAF:def_5; ::_thesis: verum end; a,f . a // q,f . q by A1, A13, Lm5; then a,f . a '||' q,f . q by DIRAF:def_4; then b,f . a '||' q,f . q by A2, A12, DIRAF:23; then A25: f . a,b '||' q,f . q by DIRAF:22; A26: LIN a,f . a,f . b by A6, A8, Th43; ( a,q // f . a,f . q & a <> q ) by A1, A13, Lm5, DIRAF:31; then f . a,f . q // x,f . a by A16, ANALOAF:def_5; then f . a,f . q '||' f . a,x by DIRAF:def_4; then LIN f . a,f . q,x by DIRAF:def_5; then A27: LIN x,f . a,f . q by DIRAF:30; A28: b <> f . b by A1, A9, Def9; LIN a,f . a,f . a by DIRAF:31; then A29: LIN b,f . b,f . a by A2, A8, A26, DIRAF:32; LIN a,f . a,a by DIRAF:31; then LIN b,f . b,a by A2, A8, A26, DIRAF:32; then A30: not LIN b,f . b,q by A13, A29, A28, DIRAF:32; A31: not LIN b,f . b,f . q proof b,f . b '||' q,f . q by A1, A6, Th49; then A32: b,f . b '||' f . q,q by DIRAF:22; assume LIN b,f . b,f . q ; ::_thesis: contradiction hence contradiction by A28, A30, A32, DIRAF:33; ::_thesis: verum end; then A33: f . b <> f . q by DIRAF:31; ( a,b // a,f . a & a,f . a // b,f . b ) by A1, A2, A8, A5, Lm6, ANALOAF:def_5; then A34: a,b // b,f . b by A2, DIRAF:3; assume a,b // f . b,f . a ; ::_thesis: contradiction then b,f . b // f . b,f . a by A10, A34, ANALOAF:def_5; then Mid b,f . b,f . a by DIRAF:def_3; then A35: Mid f . a,f . b,b by DIRAF:9; A36: LIN x,b,b by DIRAF:31; Mid x,b,q by A17, DIRAF:9; then Mid x,f . a,f . q by A22, A27, A25, PASCH:8; then consider y being Element of OAS such that A37: Mid x,y,b and A38: Mid y,f . b,f . q by A35, A22, PASCH:27; LIN x,y,b by A37, DIRAF:28; then A39: LIN x,b,y by DIRAF:30; A40: x <> b by A22, DIRAF:31; then LIN b,q,y by A18, A39, A36, DIRAF:32; then A41: b,q '||' b,y by DIRAF:def_5; A42: LIN y,f . b,f . q by A38, DIRAF:28; then LIN f . b,f . q,y by DIRAF:30; then A43: f . b,f . q '||' f . b,y by DIRAF:def_5; b,q '||' f . b,f . q by A6, Th34; then b,q '||' f . b,y by A33, A43, DIRAF:23; then f . b,y '||' b,y by A33, A41, DIRAF:23; then y,b '||' y,f . b by DIRAF:22; then A44: LIN y,b,f . b by DIRAF:def_5; A45: LIN y,b,b by DIRAF:31; LIN y,b,q by A40, A18, A39, A36, DIRAF:32; hence contradiction by A42, A30, A31, A44, A45, DIRAF:32; ::_thesis: verum end; a,b '||' f . a,f . b by A6, Th34; hence a,b // f . a,f . b by A11, DIRAF:def_4; ::_thesis: verum end; hence a,b // f . a,f . b by DIRAF:4; ::_thesis: verum end; Lm9: for OAS being OAffinSpace for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds a,b // f . a,f . b proof let OAS be OAffinSpace; ::_thesis: for a, b being Element of OAS for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds a,b // f . a,f . b let a, b be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds a,b // f . a,f . b let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation & a <> f . a & LIN a,f . a,b implies a,b // f . a,f . b ) assume that A1: f is translation and A2: a <> f . a and A3: LIN a,f . a,b ; ::_thesis: a,b // f . a,f . b f <> id the carrier of OAS by A2, FUNCT_1:18; then A4: b <> f . b by A1, Def9; A5: f is dilatation by A1, Def9; now__::_thesis:_(_a_<>_b_implies_a,b_//_f_._a,f_._b_) assume A6: a <> b ; ::_thesis: a,b // f . a,f . b A7: now__::_thesis:_(_Mid_f_._a,a,b_implies_a,b_//_f_._a,f_._b_) assume A8: Mid f . a,a,b ; ::_thesis: a,b // f . a,f . b A9: now__::_thesis:_(_Mid_f_._b,b,a_implies_a,b_//_f_._a,f_._b_) assume Mid f . b,b,a ; ::_thesis: a,b // f . a,f . b then Mid a,b,f . b by DIRAF:9; then a,b // b,f . b by DIRAF:def_3; then A10: a,b // a,f . b by ANALOAF:def_5; Mid b,a,f . a by A8, DIRAF:9; then b,a // a,f . a by DIRAF:def_3; then A11: a,b // f . a,a by ANALOAF:def_5; then f . a,a // a,f . b by A6, A10, ANALOAF:def_5; then f . a,a // f . a,f . b by ANALOAF:def_5; hence a,b // f . a,f . b by A10, A11, DIRAF:3; ::_thesis: verum end; A12: now__::_thesis:_(_Mid_b,a,f_._b_implies_a,b_//_f_._a,f_._b_) A13: now__::_thesis:_(_a_=_f_._b_implies_a,b_//_f_._a,f_._b_) assume A14: a = f . b ; ::_thesis: a,b // f . a,f . b a,f . a // b,f . b by A1, A2, A3, Lm6; hence a,b // f . a,f . b by A14, DIRAF:2; ::_thesis: verum end; assume Mid b,a,f . b ; ::_thesis: a,b // f . a,f . b then ( b,a // f . b,f . a or a = f . b ) by A1, A4, Lm8; hence a,b // f . a,f . b by A13, DIRAF:2; ::_thesis: verum end; A15: now__::_thesis:_(_Mid_b,f_._b,a_implies_a,b_//_f_._a,f_._b_) assume Mid b,f . b,a ; ::_thesis: a,b // f . a,f . b then b,a // f . b,f . a by A1, A4, Lm7; hence a,b // f . a,f . b by DIRAF:2; ::_thesis: verum end; ( LIN a,f . a,f . b & LIN a,f . a,a ) by A3, A5, Th43, DIRAF:31; hence a,b // f . a,f . b by A2, A3, A15, A12, A9, DIRAF:29, DIRAF:32; ::_thesis: verum end; A16: now__::_thesis:_(_Mid_a,b,f_._a_implies_a,b_//_f_._a,f_._b_) assume A17: Mid a,b,f . a ; ::_thesis: a,b // f . a,f . b ( b = f . a implies a,b // f . a,f . b ) by A1, A2, A3, Lm6; hence a,b // f . a,f . b by A1, A2, A17, Lm8; ::_thesis: verum end; ( Mid a,f . a,b implies a,b // f . a,f . b ) by A1, A2, Lm7; hence a,b // f . a,f . b by A3, A7, A16, DIRAF:29; ::_thesis: verum end; hence a,b // f . a,f . b by DIRAF:4; ::_thesis: verum end; theorem Th54: :: TRANSGEO:54 for OAS being OAffinSpace for f being Permutation of the carrier of OAS st f is translation holds f is positive_dilatation proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS st f is translation holds f is positive_dilatation let f be Permutation of the carrier of OAS; ::_thesis: ( f is translation implies f is positive_dilatation ) assume A1: f is translation ; ::_thesis: f is positive_dilatation A2: now__::_thesis:_(_(_for_x_being_Element_of_OAS_holds_f_._x_<>_x_)_implies_f_is_positive_dilatation_) assume A3: for x being Element of OAS holds f . x <> x ; ::_thesis: f is positive_dilatation for a, b being Element of OAS holds a,b // f . a,f . b proof let a, b be Element of OAS; ::_thesis: a,b // f . a,f . b A4: a <> f . a by A3; ( not LIN a,f . a,b implies a,b // f . a,f . b ) by A1, Lm5; hence a,b // f . a,f . b by A1, A4, Lm9; ::_thesis: verum end; hence f is positive_dilatation by Th27; ::_thesis: verum end; ( f = id the carrier of OAS implies f is positive_dilatation ) by Th28; hence f is positive_dilatation by A1, A2, Def9; ::_thesis: verum end; theorem Th55: :: TRANSGEO:55 for OAS being OAffinSpace for p, q, x being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & not LIN p,q,x holds Mid x,p,f . x proof let OAS be OAffinSpace; ::_thesis: for p, q, x being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & not LIN p,q,x holds Mid x,p,f . x let p, q, x be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & not LIN p,q,x holds Mid x,p,f . x let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . p = p & Mid q,p,f . q & not LIN p,q,x implies Mid x,p,f . x ) assume that A1: f is dilatation and A2: f . p = p and A3: ( Mid q,p,f . q & not LIN p,q,x ) ; ::_thesis: Mid x,p,f . x q,x '||' f . q,f . x by A1, Th34; then A4: q,x '||' f . x,f . q by DIRAF:22; p,x '||' p,f . x by A1, A2, Th34; then LIN p,x,f . x by DIRAF:def_5; hence Mid x,p,f . x by A3, A4, PASCH:6; ::_thesis: verum end; theorem Th56: :: TRANSGEO:56 for OAS being OAffinSpace for p, q, x being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds Mid x,p,f . x proof let OAS be OAffinSpace; ::_thesis: for p, q, x being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds Mid x,p,f . x let p, q, x be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds Mid x,p,f . x let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . p = p & Mid q,p,f . q & q <> p implies Mid x,p,f . x ) assume that A1: ( f is dilatation & f . p = p ) and A2: Mid q,p,f . q and A3: q <> p ; ::_thesis: Mid x,p,f . x now__::_thesis:_(_LIN_p,q,x_implies_Mid_x,p,f_._x_) consider r being Element of OAS such that A4: not LIN p,q,r by A3, DIRAF:37; assume A5: LIN p,q,x ; ::_thesis: Mid x,p,f . x A6: ( x = p or not LIN p,r,x ) proof A7: ( LIN p,x,q & LIN p,x,p ) by A5, DIRAF:30, DIRAF:31; assume that A8: x <> p and A9: LIN p,r,x ; ::_thesis: contradiction LIN p,x,r by A9, DIRAF:30; hence contradiction by A4, A8, A7, DIRAF:32; ::_thesis: verum end; Mid r,p,f . r by A1, A2, A4, Th55; hence Mid x,p,f . x by A1, A6, Th55, DIRAF:10; ::_thesis: verum end; hence Mid x,p,f . x by A1, A2, Th55; ::_thesis: verum end; theorem Th57: :: TRANSGEO:57 for OAS being OAffinSpace for p, q, x, y being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y holds x,y // f . y,f . x proof let OAS be OAffinSpace; ::_thesis: for p, q, x, y being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y holds x,y // f . y,f . x let p, q, x, y be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y holds x,y // f . y,f . x let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y implies x,y // f . y,f . x ) assume A1: f is dilatation ; ::_thesis: ( not f . p = p or not q <> p or not Mid q,p,f . q or LIN p,x,y or x,y // f . y,f . x ) assume A2: ( f . p = p & q <> p & Mid q,p,f . q ) ; ::_thesis: ( LIN p,x,y or x,y // f . y,f . x ) then Mid x,p,f . x by A1, Th56; then A3: x,p // p,f . x by DIRAF:def_3; Mid y,p,f . y by A1, A2, Th56; then A4: y,p // p,f . y by DIRAF:def_3; x,y '||' f . x,f . y by A1, Th34; hence ( LIN p,x,y or x,y // f . y,f . x ) by A3, A4, PASCH:12; ::_thesis: verum end; theorem Th58: :: TRANSGEO:58 for OAS being OAffinSpace for p, q, x, y being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & LIN p,x,y holds x,y // f . y,f . x proof let OAS be OAffinSpace; ::_thesis: for p, q, x, y being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & LIN p,x,y holds x,y // f . y,f . x let p, q, x, y be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & LIN p,x,y holds x,y // f . y,f . x let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q & LIN p,x,y implies x,y // f . y,f . x ) assume that A1: f is dilatation and A2: f . p = p and A3: ( q <> p & Mid q,p,f . q ) and A4: LIN p,x,y ; ::_thesis: x,y // f . y,f . x A5: Mid y,p,f . y by A1, A2, A3, Th56; A6: now__::_thesis:_(_x_=_p_implies_x,y_//_f_._y,f_._x_) assume A7: x = p ; ::_thesis: x,y // f . y,f . x then y,x // x,f . y by A5, DIRAF:def_3; hence x,y // f . y,f . x by A2, A7, DIRAF:2; ::_thesis: verum end; A8: now__::_thesis:_(_x_<>_p_&_y_<>_p_&_x_<>_y_implies_x,y_//_f_._y,f_._x_) assume that A9: x <> p and y <> p and A10: x <> y ; ::_thesis: x,y // f . y,f . x consider u being Element of OAS such that A11: not LIN p,x,u by A9, DIRAF:37; consider r being Element of OAS such that A12: x,y '||' u,r and A13: x,u '||' y,r by DIRAF:26; A14: not LIN x,y,u proof assume A15: LIN x,y,u ; ::_thesis: contradiction ( LIN x,y,p & LIN x,y,x ) by A4, DIRAF:30, DIRAF:31; hence contradiction by A10, A11, A15, DIRAF:32; ::_thesis: verum end; then A16: x,y // u,r by A12, A13, PASCH:14; A17: not LIN p,u,r proof A18: now__::_thesis:_not_u_=_r assume u = r ; ::_thesis: contradiction then u,x '||' u,y by A13, DIRAF:22; then LIN u,x,y by DIRAF:def_5; hence contradiction by A14, DIRAF:30; ::_thesis: verum end; LIN x,y,p by A4, DIRAF:30; then x,y '||' x,p by DIRAF:def_5; then x,y '||' p,x by DIRAF:22; then A19: u,r '||' p,x by A10, A12, DIRAF:23; A20: LIN u,r,u by DIRAF:31; assume LIN p,u,r ; ::_thesis: contradiction then A21: LIN u,r,p by DIRAF:30; p,x '||' p,y by A4, DIRAF:def_5; then u,r '||' p,y by A9, A19, DIRAF:23; then A22: LIN u,r,y by A18, A21, DIRAF:33; LIN u,r,x by A18, A21, A19, DIRAF:33; hence contradiction by A14, A18, A22, A20, DIRAF:32; ::_thesis: verum end; then A23: u <> r by DIRAF:31; set u9 = f . u; set r9 = f . r; set x9 = f . x; set y9 = f . y; A24: not LIN f . x,f . y,f . u by A1, A14, Th42; ( f . x,f . y '||' f . u,f . r & f . x,f . u '||' f . y,f . r ) by A1, A12, A13, Th41; then f . x,f . y // f . u,f . r by A24, PASCH:14; then A25: f . r,f . u // f . y,f . x by DIRAF:2; u,r // f . r,f . u by A1, A2, A3, A17, Th57; then x,y // f . r,f . u by A16, A23, DIRAF:3; hence x,y // f . y,f . x by A25, A23, DIRAF:3, FUNCT_2:58; ::_thesis: verum end; Mid x,p,f . x by A1, A2, A3, Th56; hence x,y // f . y,f . x by A2, A6, A8, DIRAF:4, DIRAF:def_3; ::_thesis: verum end; theorem Th59: :: TRANSGEO:59 for OAS being OAffinSpace for p, q being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q holds f is negative_dilatation proof let OAS be OAffinSpace; ::_thesis: for p, q being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q holds f is negative_dilatation let p, q be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q holds f is negative_dilatation let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q implies f is negative_dilatation ) assume A1: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q ) ; ::_thesis: f is negative_dilatation for x, y being Element of OAS holds x,y // f . y,f . x proof let x, y be Element of OAS; ::_thesis: x,y // f . y,f . x ( not LIN p,x,y implies x,y // f . y,f . x ) by A1, Th57; hence x,y // f . y,f . x by A1, Th58; ::_thesis: verum end; hence f is negative_dilatation by Def7; ::_thesis: verum end; theorem Th60: :: TRANSGEO:60 for OAS being OAffinSpace for p being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) holds for y, z being Element of OAS holds y,z // f . y,f . z proof let OAS be OAffinSpace; ::_thesis: for p being Element of OAS for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) holds for y, z being Element of OAS holds y,z // f . y,f . z let p be Element of OAS; ::_thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) holds for y, z being Element of OAS holds y,z // f . y,f . z let f be Permutation of the carrier of OAS; ::_thesis: ( f is dilatation & f . p = p & ( for x being Element of OAS holds p,x // p,f . x ) implies for y, z being Element of OAS holds y,z // f . y,f . z ) assume that A1: f is dilatation and A2: f . p = p and A3: for x being Element of OAS holds p,x // p,f . x ; ::_thesis: for y, z being Element of OAS holds y,z // f . y,f . z A4: for y, z being Element of OAS st not LIN p,y,z holds y,z // f . y,f . z proof let y, z be Element of OAS; ::_thesis: ( not LIN p,y,z implies y,z // f . y,f . z ) assume A5: not LIN p,y,z ; ::_thesis: y,z // f . y,f . z A6: ( p,y // p,f . y & p,z // p,f . z ) by A3; y,z '||' f . y,f . z by A1, Th34; hence y,z // f . y,f . z by A5, A6, PASCH:13; ::_thesis: verum end; let y, z be Element of OAS; ::_thesis: y,z // f . y,f . z ( LIN p,y,z implies y,z // f . y,f . z ) proof assume A7: LIN p,y,z ; ::_thesis: y,z // f . y,f . z A8: now__::_thesis:_(_p_<>_y_&_y_<>_z_&_z_<>_p_implies_y,z_//_f_._y,f_._z_) assume that A9: p <> y and A10: y <> z and z <> p ; ::_thesis: y,z // f . y,f . z consider q being Element of OAS such that A11: not LIN p,y,q by A9, DIRAF:37; A12: not LIN y,z,q proof assume A13: LIN y,z,q ; ::_thesis: contradiction ( LIN y,z,p & LIN y,z,y ) by A7, DIRAF:30, DIRAF:31; hence contradiction by A10, A11, A13, DIRAF:32; ::_thesis: verum end; then A14: not LIN f . y,f . z,f . q by A1, Th42; consider r being Element of OAS such that A15: y,z '||' q,r and A16: y,q '||' z,r by DIRAF:26; ( f . y,f . z '||' f . q,f . r & f . y,f . q '||' f . z,f . r ) by A1, A15, A16, Th41; then f . y,f . z // f . q,f . r by A14, PASCH:14; then A17: f . q,f . r // f . y,f . z by DIRAF:2; A18: q <> r proof assume q = r ; ::_thesis: contradiction then q,y '||' q,z by A16, DIRAF:22; then LIN q,y,z by DIRAF:def_5; hence contradiction by A12, DIRAF:30; ::_thesis: verum end; not LIN p,q,r proof A19: LIN q,r,q by DIRAF:31; assume LIN p,q,r ; ::_thesis: contradiction then A20: LIN q,r,p by DIRAF:30; LIN y,p,z by A7, DIRAF:30; then y,p '||' y,z by DIRAF:def_5; then y,z '||' p,y by DIRAF:22; then q,r '||' p,y by A10, A15, DIRAF:23; then LIN q,r,y by A18, A20, DIRAF:33; hence contradiction by A11, A18, A20, A19, DIRAF:32; ::_thesis: verum end; then A21: q,r // f . q,f . r by A4; y,z // q,r by A15, A16, A12, PASCH:14; then y,z // f . q,f . r by A18, A21, DIRAF:3; hence y,z // f . y,f . z by A18, A17, DIRAF:3, FUNCT_2:58; ::_thesis: verum end; now__::_thesis:_(_p_=_z_implies_y,z_//_f_._y,f_._z_) assume p = z ; ::_thesis: y,z // f . y,f . z then z,y // f . z,f . y by A2, A3; hence y,z // f . y,f . z by DIRAF:2; ::_thesis: verum end; hence y,z // f . y,f . z by A2, A3, A8, DIRAF:4; ::_thesis: verum end; hence y,z // f . y,f . z by A4; ::_thesis: verum end; theorem :: TRANSGEO:61 for OAS being OAffinSpace for f being Permutation of the carrier of OAS holds ( not f is dilatation or f is positive_dilatation or f is negative_dilatation ) proof let OAS be OAffinSpace; ::_thesis: for f being Permutation of the carrier of OAS holds ( not f is dilatation or f is positive_dilatation or f is negative_dilatation ) let f be Permutation of the carrier of OAS; ::_thesis: ( not f is dilatation or f is positive_dilatation or f is negative_dilatation ) assume A1: f is dilatation ; ::_thesis: ( f is positive_dilatation or f is negative_dilatation ) A2: now__::_thesis:_(_for_p_being_Element_of_OAS_holds_not_f_._p_=_p_or_f_is_positive_dilatation_or_f_is_negative_dilatation_) given p being Element of OAS such that A3: f . p = p ; ::_thesis: ( f is positive_dilatation or f is negative_dilatation ) A4: now__::_thesis:_(_not_for_q_being_Element_of_OAS_holds_p,q_//_p,f_._q_implies_f_is_negative_dilatation_) given q being Element of OAS such that A5: not p,q // p,f . q ; ::_thesis: f is negative_dilatation p,q '||' p,f . q by A1, A3, Th34; then A6: p,q // f . q,p by A5, DIRAF:def_4; then q,p // p,f . q by DIRAF:2; then A7: Mid q,p,f . q by DIRAF:def_3; p <> q by A5, A6, DIRAF:2; hence f is negative_dilatation by A1, A3, A7, Th59; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_OAS_holds_p,x_//_p,f_._x_)_implies_f_is_positive_dilatation_) assume for x being Element of OAS holds p,x // p,f . x ; ::_thesis: f is positive_dilatation then for x, y being Element of OAS holds x,y // f . x,f . y by A1, A3, Th60; hence f is positive_dilatation by Th27; ::_thesis: verum end; hence ( f is positive_dilatation or f is negative_dilatation ) by A4; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_OAS_holds_f_._x_<>_x_)_implies_f_is_positive_dilatation_) assume for x being Element of OAS holds f . x <> x ; ::_thesis: f is positive_dilatation then f is translation by A1, Def9; hence f is positive_dilatation by Th54; ::_thesis: verum end; hence ( f is positive_dilatation or f is negative_dilatation ) by A2; ::_thesis: verum end; theorem Th62: :: TRANSGEO:62 for AFS being AffinSpace holds AFS is CongrSpace-like proof let AFS be AffinSpace; ::_thesis: AFS is CongrSpace-like thus for x, y, z, t, a, b being Element of AFS st x,y // a,b & a,b // z,t & a <> b holds x,y // z,t by AFF_1:5; :: according to TRANSGEO:def_5 ::_thesis: ( ( for x, y, z being Element of AFS holds x,x // y,z ) & ( for x, y, z, t being Element of AFS st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of AFS holds x,y // x,y ) ) thus for x, y, z being Element of AFS holds x,x // y,z by AFF_1:3; ::_thesis: ( ( for x, y, z, t being Element of AFS st x,y // z,t holds z,t // x,y ) & ( for x, y being Element of AFS holds x,y // x,y ) ) thus for x, y, z, t being Element of AFS st x,y // z,t holds z,t // x,y by AFF_1:4; ::_thesis: for x, y being Element of AFS holds x,y // x,y thus for x, y being Element of AFS holds x,y // x,y by AFF_1:2; ::_thesis: verum end; theorem :: TRANSGEO:63 for OAS being OAffinSpace holds Lambda OAS is CongrSpace proof let OAS be OAffinSpace; ::_thesis: Lambda OAS is CongrSpace Lambda OAS is AffinSpace by DIRAF:41; hence Lambda OAS is CongrSpace by Th62; ::_thesis: verum end; definition let AFS be AffinSpace; let f be Permutation of the carrier of AFS; attrf is dilatation means :Def10: :: TRANSGEO:def 10 f is_DIL_of AFS; end; :: deftheorem Def10 defines dilatation TRANSGEO:def_10_:_ for AFS being AffinSpace for f being Permutation of the carrier of AFS holds ( f is dilatation iff f is_DIL_of AFS ); theorem Th64: :: TRANSGEO:64 for AFS being AffinSpace for f being Permutation of the carrier of AFS holds ( f is dilatation iff for a, b being Element of AFS holds a,b // f . a,f . b ) proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS holds ( f is dilatation iff for a, b being Element of AFS holds a,b // f . a,f . b ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation iff for a, b being Element of AFS holds a,b // f . a,f . b ) thus ( f is dilatation implies for a, b being Element of AFS holds a,b // f . a,f . b ) ::_thesis: ( ( for a, b being Element of AFS holds a,b // f . a,f . b ) implies f is dilatation ) proof assume A1: f is dilatation ; ::_thesis: for a, b being Element of AFS holds a,b // f . a,f . b let a, b be Element of AFS; ::_thesis: a,b // f . a,f . b f is_DIL_of AFS by A1, Def10; hence a,b // f . a,f . b by Th22; ::_thesis: verum end; assume for a, b being Element of AFS holds a,b // f . a,f . b ; ::_thesis: f is dilatation then f is_DIL_of AFS by Th22; hence f is dilatation by Def10; ::_thesis: verum end; theorem Th65: :: TRANSGEO:65 for AFS being AffinSpace holds id the carrier of AFS is dilatation proof let AFS be AffinSpace; ::_thesis: id the carrier of AFS is dilatation now__::_thesis:_for_x,_y_being_Element_of_AFS_holds_x,y_//_(id_the_carrier_of_AFS)_._x,(id_the_carrier_of_AFS)_._y let x, y be Element of AFS; ::_thesis: x,y // (id the carrier of AFS) . x,(id the carrier of AFS) . y ( (id the carrier of AFS) . x = x & (id the carrier of AFS) . y = y ) by FUNCT_1:18; hence x,y // (id the carrier of AFS) . x,(id the carrier of AFS) . y by AFF_1:2; ::_thesis: verum end; hence id the carrier of AFS is dilatation by Th64; ::_thesis: verum end; theorem Th66: :: TRANSGEO:66 for AFS being AffinSpace for f being Permutation of the carrier of AFS st f is dilatation holds f " is dilatation proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation holds f " is dilatation let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation implies f " is dilatation ) assume A1: f is dilatation ; ::_thesis: f " is dilatation now__::_thesis:_for_x,_y_being_Element_of_AFS_holds_x,y_//_(f_")_._x,(f_")_._y let x, y be Element of AFS; ::_thesis: x,y // (f ") . x,(f ") . y set x9 = (f ") . x; set y9 = (f ") . y; ( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2; then (f ") . x,(f ") . y // x,y by A1, Th64; hence x,y // (f ") . x,(f ") . y by AFF_1:4; ::_thesis: verum end; hence f " is dilatation by Th64; ::_thesis: verum end; theorem Th67: :: TRANSGEO:67 for AFS being AffinSpace for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation holds f * g is dilatation proof let AFS be AffinSpace; ::_thesis: for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation holds f * g is dilatation let f, g be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation & g is dilatation implies f * g is dilatation ) assume A1: ( f is dilatation & g is dilatation ) ; ::_thesis: f * g is dilatation now__::_thesis:_for_x,_y_being_Element_of_AFS_holds_x,y_//_(f_*_g)_._x,(f_*_g)_._y let x, y be Element of AFS; ::_thesis: x,y // (f * g) . x,(f * g) . y set x9 = g . x; set y9 = g . y; A2: ( (f * g) . x = f . (g . x) & (f * g) . y = f . (g . y) ) by FUNCT_2:15; A3: now__::_thesis:_(_g_._x_=_g_._y_implies_x,y_//_(f_*_g)_._x,(f_*_g)_._y_) assume g . x = g . y ; ::_thesis: x,y // (f * g) . x,(f * g) . y then x = y by FUNCT_2:58; hence x,y // (f * g) . x,(f * g) . y by AFF_1:3; ::_thesis: verum end; ( x,y // g . x,g . y & g . x,g . y // f . (g . x),f . (g . y) ) by A1, Th64; hence x,y // (f * g) . x,(f * g) . y by A2, A3, AFF_1:5; ::_thesis: verum end; hence f * g is dilatation by Th64; ::_thesis: verum end; theorem Th68: :: TRANSGEO:68 for AFS being AffinSpace for f being Permutation of the carrier of AFS st f is dilatation holds for a, b, c, d being Element of AFS holds ( a,b // c,d iff f . a,f . b // f . c,f . d ) proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation holds for a, b, c, d being Element of AFS holds ( a,b // c,d iff f . a,f . b // f . c,f . d ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation implies for a, b, c, d being Element of AFS holds ( a,b // c,d iff f . a,f . b // f . c,f . d ) ) assume A1: f is dilatation ; ::_thesis: for a, b, c, d being Element of AFS holds ( a,b // c,d iff f . a,f . b // f . c,f . d ) let a, b, c, d be Element of AFS; ::_thesis: ( a,b // c,d iff f . a,f . b // f . c,f . d ) A2: c,d // f . c,f . d by A1, Th64; A3: a,b // f . a,f . b by A1, Th64; A4: now__::_thesis:_(_f_._a,f_._b_//_f_._c,f_._d_implies_a,b_//_c,d_) A5: now__::_thesis:_(_a,b_//_f_._c,f_._d_implies_a,b_//_c,d_) A6: now__::_thesis:_(_f_._c_=_f_._d_implies_a,b_//_c,d_) assume f . c = f . d ; ::_thesis: a,b // c,d then c = d by FUNCT_2:58; hence a,b // c,d by AFF_1:3; ::_thesis: verum end; assume a,b // f . c,f . d ; ::_thesis: a,b // c,d hence a,b // c,d by A2, A6, AFF_1:5; ::_thesis: verum end; A7: now__::_thesis:_(_f_._a_=_f_._b_implies_a,b_//_c,d_) assume f . a = f . b ; ::_thesis: a,b // c,d then a = b by FUNCT_2:58; hence a,b // c,d by AFF_1:3; ::_thesis: verum end; assume f . a,f . b // f . c,f . d ; ::_thesis: a,b // c,d hence a,b // c,d by A3, A7, A5, AFF_1:5; ::_thesis: verum end; now__::_thesis:_(_a,b_//_c,d_implies_f_._a,f_._b_//_f_._c,f_._d_) A8: now__::_thesis:_(_f_._a,f_._b_//_c,d_implies_f_._a,f_._b_//_f_._c,f_._d_) A9: ( c = d implies f . a,f . b // f . c,f . d ) by AFF_1:3; assume f . a,f . b // c,d ; ::_thesis: f . a,f . b // f . c,f . d hence f . a,f . b // f . c,f . d by A2, A9, AFF_1:5; ::_thesis: verum end; assume a,b // c,d ; ::_thesis: f . a,f . b // f . c,f . d then ( f . a,f . b // c,d or a = b ) by A3, AFF_1:5; hence f . a,f . b // f . c,f . d by A8, AFF_1:3; ::_thesis: verum end; hence ( a,b // c,d iff f . a,f . b // f . c,f . d ) by A4; ::_thesis: verum end; theorem :: TRANSGEO:69 for AFS being AffinSpace for f being Permutation of the carrier of AFS st f is dilatation holds for a, b, c being Element of AFS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation holds for a, b, c being Element of AFS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation implies for a, b, c being Element of AFS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) ) assume A1: f is dilatation ; ::_thesis: for a, b, c being Element of AFS holds ( LIN a,b,c iff LIN f . a,f . b,f . c ) let a, b, c be Element of AFS; ::_thesis: ( LIN a,b,c iff LIN f . a,f . b,f . c ) ( a,b // a,c iff f . a,f . b // f . a,f . c ) by A1, Th68; hence ( LIN a,b,c iff LIN f . a,f . b,f . c ) by AFF_1:def_1; ::_thesis: verum end; theorem Th70: :: TRANSGEO:70 for AFS being AffinSpace for x, y being Element of AFS for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds LIN x,f . x,f . y proof let AFS be AffinSpace; ::_thesis: for x, y being Element of AFS for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds LIN x,f . x,f . y let x, y be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds LIN x,f . x,f . y let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation & LIN x,f . x,y implies LIN x,f . x,f . y ) assume A1: f is dilatation ; ::_thesis: ( not LIN x,f . x,y or LIN x,f . x,f . y ) assume A2: LIN x,f . x,y ; ::_thesis: LIN x,f . x,f . y now__::_thesis:_(_x_<>_y_implies_LIN_x,f_._x,f_._y_) assume A3: x <> y ; ::_thesis: LIN x,f . x,f . y ( x,f . x // x,y & x,y // f . x,f . y ) by A1, A2, Th64, AFF_1:def_1; then x,f . x // f . x,f . y by A3, AFF_1:5; then f . x,x // f . x,f . y by AFF_1:4; then LIN f . x,x,f . y by AFF_1:def_1; hence LIN x,f . x,f . y by AFF_1:6; ::_thesis: verum end; hence LIN x,f . x,f . y by AFF_1:7; ::_thesis: verum end; theorem Th71: :: TRANSGEO:71 for AFS being AffinSpace for a, b, c, d being Element of AFS holds ( not a,b // c,d or a,c // b,d or ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) ) proof let AFS be AffinSpace; ::_thesis: for a, b, c, d being Element of AFS holds ( not a,b // c,d or a,c // b,d or ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) ) let a, b, c, d be Element of AFS; ::_thesis: ( not a,b // c,d or a,c // b,d or ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) ) assume A1: a,b // c,d ; ::_thesis: ( a,c // b,d or ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) ) assume A2: not a,c // b,d ; ::_thesis: ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) A3: now__::_thesis:_(_a_<>_b_implies_ex_x_being_Element_of_AFS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) consider z being Element of AFS such that A4: a,b // c,z and A5: a,c // b,z by DIRAF:40; assume A6: a <> b ; ::_thesis: ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) A7: now__::_thesis:_(_b_<>_z_implies_ex_x_being_Element_of_AFS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) c,d // c,z by A1, A6, A4, AFF_1:5; then LIN c,d,z by AFF_1:def_1; then LIN d,c,z by AFF_1:6; then d,c // d,z by AFF_1:def_1; then z,d // d,c by AFF_1:4; then consider t being Element of AFS such that A8: b,d // d,t and A9: b,z // c,t by A2, A5, DIRAF:40; assume b <> z ; ::_thesis: ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) then a,c // c,t by A5, A9, AFF_1:5; then c,a // c,t by AFF_1:4; then LIN c,a,t by AFF_1:def_1; then A10: LIN a,c,t by AFF_1:6; d,b // d,t by A8, AFF_1:4; then LIN d,b,t by AFF_1:def_1; then LIN b,d,t by AFF_1:6; hence ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) by A10; ::_thesis: verum end; now__::_thesis:_(_b_=_z_implies_ex_x_being_Element_of_AFS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) assume b = z ; ::_thesis: ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) then b,a // b,c by A4, AFF_1:4; then LIN b,a,c by AFF_1:def_1; then A11: LIN a,c,b by AFF_1:6; LIN b,d,b by AFF_1:7; hence ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) by A11; ::_thesis: verum end; hence ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) by A7; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_ex_x_being_Element_of_AFS_st_ (_LIN_a,c,x_&_LIN_b,d,x_)_) assume a = b ; ::_thesis: ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) then ( LIN a,c,a & LIN b,d,a ) by AFF_1:7; hence ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) ; ::_thesis: verum end; hence ex x being Element of AFS st ( LIN a,c,x & LIN b,d,x ) by A3; ::_thesis: verum end; theorem Th72: :: TRANSGEO:72 for AFS being AffinSpace for f being Permutation of the carrier of AFS st f is dilatation holds ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation holds ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation implies ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) ) assume A1: f is dilatation ; ::_thesis: ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) A2: now__::_thesis:_(_(_for_x,_y_being_Element_of_AFS_holds_x,f_._x_//_y,f_._y_)_&_f_<>_id_the_carrier_of_AFS_implies_for_x_being_Element_of_AFS_holds_not_f_._x_=_x_) assume A3: for x, y being Element of AFS holds x,f . x // y,f . y ; ::_thesis: ( f <> id the carrier of AFS implies for x being Element of AFS holds not f . x = x ) assume f <> id the carrier of AFS ; ::_thesis: for x being Element of AFS holds not f . x = x then consider y being Element of AFS such that A4: f . y <> (id the carrier of AFS) . y by FUNCT_2:63; given x being Element of AFS such that A5: f . x = x ; ::_thesis: contradiction x <> y by A5, A4, FUNCT_1:18; then consider z being Element of AFS such that A6: not LIN x,y,z by AFF_1:13; x,z // f . x,f . z by A1, Th64; then LIN x,z,f . z by A5, AFF_1:def_1; then A7: LIN z,f . z,x by AFF_1:6; LIN z,f . z,z by AFF_1:7; then A8: z,f . z // x,z by A7, AFF_1:10; A9: f . y <> y by A4, FUNCT_1:18; x,y // f . x,f . y by A1, Th64; then A10: LIN x,y,f . y by A5, AFF_1:def_1; then LIN y,x,f . y by AFF_1:6; then A11: y,x // y,f . y by AFF_1:def_1; A12: LIN y,f . y,x by A10, AFF_1:6; A13: now__::_thesis:_not_z_=_f_._z assume z = f . z ; ::_thesis: contradiction then z,y // z,f . y by A1, Th64; then LIN z,y,f . y by AFF_1:def_1; then ( LIN y,f . y,y & LIN y,f . y,z ) by AFF_1:6, AFF_1:7; hence contradiction by A9, A12, A6, AFF_1:8; ::_thesis: verum end; y,f . y // z,f . z by A3; then y,f . y // x,z by A13, A8, AFF_1:5; then y,x // x,z by A9, A11, AFF_1:5; then x,y // x,z by AFF_1:4; hence contradiction by A6, AFF_1:def_1; ::_thesis: verum end; now__::_thesis:_(_(_f_=_id_the_carrier_of_AFS_or_for_z_being_Element_of_AFS_holds_f_._z_<>_z_)_implies_for_x,_y_being_Element_of_AFS_holds_x,f_._x_//_y,f_._y_) assume A14: ( f = id the carrier of AFS or for z being Element of AFS holds f . z <> z ) ; ::_thesis: for x, y being Element of AFS holds x,f . x // y,f . y let x, y be Element of AFS; ::_thesis: x,f . x // y,f . y A15: x,y // f . x,f . y by A1, Th64; A16: now__::_thesis:_(_(_for_z_being_Element_of_AFS_holds_f_._z_<>_z_)_implies_x,f_._x_//_y,f_._y_) assume A17: for z being Element of AFS holds f . z <> z ; ::_thesis: x,f . x // y,f . y assume A18: not x,f . x // y,f . y ; ::_thesis: contradiction then consider z being Element of AFS such that A19: LIN x,f . x,z and A20: LIN y,f . y,z by A15, Th71; set t = f . z; LIN x,f . x,f . z by A1, A19, Th70; then A21: x,f . x // z,f . z by A19, AFF_1:10; LIN y,f . y,f . z by A1, A20, Th70; then A22: y,f . y // z,f . z by A20, AFF_1:10; z <> f . z by A17; hence contradiction by A18, A21, A22, AFF_1:5; ::_thesis: verum end; now__::_thesis:_(_f_=_id_the_carrier_of_AFS_implies_x,f_._x_//_y,f_._y_) assume f = id the carrier of AFS ; ::_thesis: x,f . x // y,f . y then f . y = y by FUNCT_1:18; hence x,f . x // y,f . y by AFF_1:3; ::_thesis: verum end; hence x,f . x // y,f . y by A14, A16; ::_thesis: verum end; hence ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) by A2; ::_thesis: verum end; theorem Th73: :: TRANSGEO:73 for AFS being AffinSpace for a, b, x being Element of AFS for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds f . x = x proof let AFS be AffinSpace; ::_thesis: for a, b, x being Element of AFS for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds f . x = x let a, b, x be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds f . x = x let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation & f . a = a & f . b = b & not LIN a,b,x implies f . x = x ) assume that A1: f is dilatation and A2: f . a = a and A3: f . b = b and A4: not LIN a,b,x ; ::_thesis: f . x = x a,x // a,f . x by A1, A2, Th64; then LIN a,x,f . x by AFF_1:def_1; then A5: LIN x,f . x,a by AFF_1:6; b,x // b,f . x by A1, A3, Th64; then LIN b,x,f . x by AFF_1:def_1; then A6: ( LIN x,f . x,x & LIN x,f . x,b ) by AFF_1:6, AFF_1:7; assume f . x <> x ; ::_thesis: contradiction hence contradiction by A4, A5, A6, AFF_1:8; ::_thesis: verum end; theorem Th74: :: TRANSGEO:74 for AFS being AffinSpace for a, b being Element of AFS for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds f = id the carrier of AFS proof let AFS be AffinSpace; ::_thesis: for a, b being Element of AFS for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds f = id the carrier of AFS let a, b be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds f = id the carrier of AFS let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation & f . a = a & f . b = b & a <> b implies f = id the carrier of AFS ) assume that A1: f is dilatation and A2: f . a = a and A3: f . b = b and A4: a <> b ; ::_thesis: f = id the carrier of AFS now__::_thesis:_for_x_being_Element_of_AFS_holds_f_._x_=_(id_the_carrier_of_AFS)_._x let x be Element of AFS; ::_thesis: f . x = (id the carrier of AFS) . x A5: now__::_thesis:_(_LIN_a,b,x_implies_f_._x_=_x_) assume A6: LIN a,b,x ; ::_thesis: f . x = x now__::_thesis:_(_x_<>_a_implies_f_._x_=_x_) consider z being Element of AFS such that A7: not LIN a,b,z by A4, AFF_1:13; assume A8: x <> a ; ::_thesis: f . x = x A9: not LIN a,z,x proof assume LIN a,z,x ; ::_thesis: contradiction then A10: LIN a,x,z by AFF_1:6; ( LIN a,x,a & LIN a,x,b ) by A6, AFF_1:6, AFF_1:7; hence contradiction by A8, A7, A10, AFF_1:8; ::_thesis: verum end; f . z = z by A1, A2, A3, A7, Th73; hence f . x = x by A1, A2, A9, Th73; ::_thesis: verum end; hence f . x = x by A2; ::_thesis: verum end; ( not LIN a,b,x implies f . x = x ) by A1, A2, A3, Th73; hence f . x = (id the carrier of AFS) . x by A5, FUNCT_1:18; ::_thesis: verum end; hence f = id the carrier of AFS by FUNCT_2:63; ::_thesis: verum end; theorem :: TRANSGEO:75 for AFS being AffinSpace for a, b being Element of AFS for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds f = g proof let AFS be AffinSpace; ::_thesis: for a, b being Element of AFS for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds f = g let a, b be Element of AFS; ::_thesis: for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds f = g let f, g be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b implies f = g ) assume that A1: f is dilatation and A2: g is dilatation and A3: f . a = g . a and A4: f . b = g . b ; ::_thesis: ( a = b or f = g ) A5: ((g ") * f) . b = (g ") . (g . b) by A4, FUNCT_2:15 .= b by Th2 ; A6: g " is dilatation by A2, Th66; assume A7: a <> b ; ::_thesis: f = g ((g ") * f) . a = (g ") . (g . a) by A3, FUNCT_2:15 .= a by Th2 ; then A8: (g ") * f = id the carrier of AFS by A1, A7, A5, A6, Th67, Th74; now__::_thesis:_for_x_being_Element_of_AFS_holds_g_._x_=_f_._x let x be Element of AFS; ::_thesis: g . x = f . x (g ") . (f . x) = ((g ") * f) . x by FUNCT_2:15; then (g ") . (f . x) = x by A8, FUNCT_1:18; hence g . x = f . x by Th2; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; theorem Th76: :: TRANSGEO:76 for AFS being AffinSpace for a, b, c, d1, d2 being Element of AFS st not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c // b,d2 holds d1 = d2 proof let AFS be AffinSpace; ::_thesis: for a, b, c, d1, d2 being Element of AFS st not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c // b,d2 holds d1 = d2 let a, b, c, d1, d2 be Element of AFS; ::_thesis: ( not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c // b,d2 implies d1 = d2 ) assume that A1: not LIN a,b,c and A2: a,b // c,d1 and A3: a,b // c,d2 and A4: a,c // b,d1 and A5: a,c // b,d2 ; ::_thesis: d1 = d2 assume A6: d1 <> d2 ; ::_thesis: contradiction a <> c by A1, AFF_1:7; then b,d1 // b,d2 by A4, A5, AFF_1:5; then LIN b,d1,d2 by AFF_1:def_1; then A7: LIN d1,d2,b by AFF_1:6; A8: now__::_thesis:_not_c_=_d1 assume c = d1 ; ::_thesis: contradiction then c,a // c,b by A4, AFF_1:4; then LIN c,a,b by AFF_1:def_1; hence contradiction by A1, AFF_1:6; ::_thesis: verum end; A9: LIN d1,d2,d1 by AFF_1:7; a <> b by A1, AFF_1:7; then c,d1 // c,d2 by A2, A3, AFF_1:5; then A10: LIN c,d1,d2 by AFF_1:def_1; then A11: LIN d1,d2,c by AFF_1:6; LIN d1,d2,c by A10, AFF_1:6; then d1,d2 // c,d1 by A9, AFF_1:10; then ( d1,d2 // a,b or c = d1 ) by A2, AFF_1:5; then d1,d2 // b,a by A8, AFF_1:4; then LIN d1,d2,a by A6, A7, AFF_1:9; hence contradiction by A1, A6, A11, A7, AFF_1:8; ::_thesis: verum end; definition let AFS be AffinSpace; let f be Permutation of the carrier of AFS; attrf is translation means :Def11: :: TRANSGEO:def 11 ( f is dilatation & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ); end; :: deftheorem Def11 defines translation TRANSGEO:def_11_:_ for AFS being AffinSpace for f being Permutation of the carrier of AFS holds ( f is translation iff ( f is dilatation & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ) ); theorem :: TRANSGEO:77 for AFS being AffinSpace holds id the carrier of AFS is translation proof let AFS be AffinSpace; ::_thesis: id the carrier of AFS is translation id the carrier of AFS is dilatation by Th65; hence id the carrier of AFS is translation by Def11; ::_thesis: verum end; theorem Th78: :: TRANSGEO:78 for AFS being AffinSpace for f being Permutation of the carrier of AFS st f is dilatation holds ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS st f is dilatation holds ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is dilatation implies ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) ) assume A1: f is dilatation ; ::_thesis: ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) then ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) by Th72; hence ( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y ) by A1, Def11; ::_thesis: verum end; theorem Th79: :: TRANSGEO:79 for AFS being AffinSpace for a, x being Element of AFS for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds f . x = g . x proof let AFS be AffinSpace; ::_thesis: for a, x being Element of AFS for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds f . x = g . x let a, x be Element of AFS; ::_thesis: for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds f . x = g . x let f, g be Permutation of the carrier of AFS; ::_thesis: ( f is translation & g is translation & f . a = g . a & not LIN a,f . a,x implies f . x = g . x ) assume that A1: f is translation and A2: g is translation and A3: f . a = g . a and A4: not LIN a,f . a,x ; ::_thesis: f . x = g . x set b = f . a; set y = f . x; set z = g . x; g is dilatation by A2, Def11; then A5: ( a,x // f . a,g . x & a,f . a // x,g . x ) by A2, A3, Th64, Th78; A6: f is dilatation by A1, Def11; then A7: a,x // f . a,f . x by Th64; a,f . a // x,f . x by A1, A6, Th78; hence f . x = g . x by A4, A7, A5, Th76; ::_thesis: verum end; theorem Th80: :: TRANSGEO:80 for AFS being AffinSpace for a being Element of AFS for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds f = g proof let AFS be AffinSpace; ::_thesis: for a being Element of AFS for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds f = g let a be Element of AFS; ::_thesis: for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds f = g let f, g be Permutation of the carrier of AFS; ::_thesis: ( f is translation & g is translation & f . a = g . a implies f = g ) assume that A1: f is translation and A2: g is translation and A3: f . a = g . a ; ::_thesis: f = g set b = f . a; A4: f is dilatation by A1, Def11; A5: now__::_thesis:_(_a_<>_f_._a_implies_f_=_g_) assume A6: a <> f . a ; ::_thesis: f = g for x being Element of AFS holds f . x = g . x proof let x be Element of AFS; ::_thesis: f . x = g . x now__::_thesis:_(_LIN_a,f_._a,x_implies_f_._x_=_g_._x_) assume A7: LIN a,f . a,x ; ::_thesis: f . x = g . x now__::_thesis:_(_x_<>_a_implies_f_._x_=_g_._x_) A8: f <> id the carrier of AFS by A6, FUNCT_1:18; then A9: f . x <> x by A1, Def11; assume x <> a ; ::_thesis: f . x = g . x consider p being Element of AFS such that A10: not LIN a,f . a,p by A6, AFF_1:13; A11: f . p <> p by A1, A8, Def11; A12: not LIN p,f . p,x proof A13: LIN a,f . a,f . x by A4, A7, Th70; LIN a,f . a,a by AFF_1:7; then A14: LIN x,f . x,a by A6, A7, A13, AFF_1:8; A15: LIN p,f . p,p by AFF_1:7; LIN a,f . a,f . a by AFF_1:7; then A16: LIN x,f . x,f . a by A6, A7, A13, AFF_1:8; assume A17: LIN p,f . p,x ; ::_thesis: contradiction then LIN p,f . p,f . x by A4, Th70; then LIN x,f . x,p by A11, A17, A15, AFF_1:8; hence contradiction by A10, A9, A14, A16, AFF_1:8; ::_thesis: verum end; f . p = g . p by A1, A2, A3, A10, Th79; hence f . x = g . x by A1, A2, A12, Th79; ::_thesis: verum end; hence f . x = g . x by A3; ::_thesis: verum end; hence f . x = g . x by A1, A2, A3, Th79; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; now__::_thesis:_(_f_._a_=_a_implies_f_=_g_) assume A18: f . a = a ; ::_thesis: f = g then f = id the carrier of AFS by A1, Def11; hence f = g by A2, A3, A18, Def11; ::_thesis: verum end; hence f = g by A5; ::_thesis: verum end; theorem Th81: :: TRANSGEO:81 for AFS being AffinSpace for f being Permutation of the carrier of AFS st f is translation holds f " is translation proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS st f is translation holds f " is translation let f be Permutation of the carrier of AFS; ::_thesis: ( f is translation implies f " is translation ) A1: now__::_thesis:_(_(_for_x_being_Element_of_AFS_holds_f_._x_<>_x_)_implies_for_y_being_Element_of_AFS_holds_not_(f_")_._y_=_y_) assume A2: for x being Element of AFS holds f . x <> x ; ::_thesis: for y being Element of AFS holds not (f ") . y = y given y being Element of AFS such that A3: (f ") . y = y ; ::_thesis: contradiction f . y = y by A3, Th2; hence contradiction by A2; ::_thesis: verum end; assume A4: f is translation ; ::_thesis: f " is translation then f is dilatation by Def11; then A5: f " is dilatation by Th66; ( f = id the carrier of AFS implies f " = id the carrier of AFS ) by FUNCT_1:45; hence f " is translation by A4, A5, A1, Def11; ::_thesis: verum end; theorem :: TRANSGEO:82 for AFS being AffinSpace for f, g being Permutation of the carrier of AFS st f is translation & g is translation holds f * g is translation proof let AFS be AffinSpace; ::_thesis: for f, g being Permutation of the carrier of AFS st f is translation & g is translation holds f * g is translation let f, g be Permutation of the carrier of AFS; ::_thesis: ( f is translation & g is translation implies f * g is translation ) assume that A1: f is translation and A2: g is translation ; ::_thesis: f * g is translation ( f is dilatation & g is dilatation ) by A1, A2, Def11; then A3: f * g is dilatation by Th67; now__::_thesis:_(_f_*_g_<>_id_the_carrier_of_AFS_implies_f_*_g_is_translation_) assume A4: f * g <> id the carrier of AFS ; ::_thesis: f * g is translation for x being Element of AFS holds (f * g) . x <> x proof given x being Element of AFS such that A5: (f * g) . x = x ; ::_thesis: contradiction f . (g . x) = x by A5, FUNCT_2:15; then A6: g . x = (f ") . x by Th2; f " is translation by A1, Th81; then f * g = f * (f ") by A2, A6, Th80; hence contradiction by A4, FUNCT_2:61; ::_thesis: verum end; hence f * g is translation by A3, Def11; ::_thesis: verum end; hence f * g is translation by A3, Def11; ::_thesis: verum end; definition let AFS be AffinSpace; let f be Permutation of the carrier of AFS; attrf is collineation means :: TRANSGEO:def 12 f is_automorphism_of the CONGR of AFS; end; :: deftheorem defines collineation TRANSGEO:def_12_:_ for AFS being AffinSpace for f being Permutation of the carrier of AFS holds ( f is collineation iff f is_automorphism_of the CONGR of AFS ); theorem Th83: :: TRANSGEO:83 for AFS being AffinSpace for f being Permutation of the carrier of AFS holds ( f is collineation iff for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) ) proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS holds ( f is collineation iff for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is collineation iff for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) ) thus ( f is collineation implies for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) ) ::_thesis: ( ( for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) ) implies f is collineation ) proof assume A1: f is_automorphism_of the CONGR of AFS ; :: according to TRANSGEO:def_12 ::_thesis: for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) let x, y, z, t be Element of AFS; ::_thesis: ( x,y // z,t iff f . x,f . y // f . z,f . t ) thus ( x,y // z,t implies f . x,f . y // f . z,f . t ) ::_thesis: ( f . x,f . y // f . z,f . t implies x,y // z,t ) proof assume x,y // z,t ; ::_thesis: f . x,f . y // f . z,f . t then [[x,y],[z,t]] in the CONGR of AFS by ANALOAF:def_2; then [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS by A1, Def3; hence f . x,f . y // f . z,f . t by ANALOAF:def_2; ::_thesis: verum end; assume f . x,f . y // f . z,f . t ; ::_thesis: x,y // z,t then [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS by ANALOAF:def_2; then [[x,y],[z,t]] in the CONGR of AFS by A1, Def3; hence x,y // z,t by ANALOAF:def_2; ::_thesis: verum end; assume A2: for x, y, z, t being Element of AFS holds ( x,y // z,t iff f . x,f . y // f . z,f . t ) ; ::_thesis: f is collineation let x be Element of AFS; :: according to TRANSGEO:def_3,TRANSGEO:def_12 ::_thesis: for y, z, t being Element of the carrier of AFS holds ( [[x,y],[z,t]] in the CONGR of AFS iff [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS ) let y, z, t be Element of AFS; ::_thesis: ( [[x,y],[z,t]] in the CONGR of AFS iff [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS ) ( x,y // z,t iff f . x,f . y // f . z,f . t ) by A2; hence ( [[x,y],[z,t]] in the CONGR of AFS iff [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS ) by ANALOAF:def_2; ::_thesis: verum end; theorem Th84: :: TRANSGEO:84 for AFS being AffinSpace for x, y, z being Element of AFS for f being Permutation of the carrier of AFS st f is collineation holds ( LIN x,y,z iff LIN f . x,f . y,f . z ) proof let AFS be AffinSpace; ::_thesis: for x, y, z being Element of AFS for f being Permutation of the carrier of AFS st f is collineation holds ( LIN x,y,z iff LIN f . x,f . y,f . z ) let x, y, z be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS st f is collineation holds ( LIN x,y,z iff LIN f . x,f . y,f . z ) let f be Permutation of the carrier of AFS; ::_thesis: ( f is collineation implies ( LIN x,y,z iff LIN f . x,f . y,f . z ) ) assume f is collineation ; ::_thesis: ( LIN x,y,z iff LIN f . x,f . y,f . z ) then ( x,y // x,z iff f . x,f . y // f . x,f . z ) by Th83; hence ( LIN x,y,z iff LIN f . x,f . y,f . z ) by AFF_1:def_1; ::_thesis: verum end; theorem :: TRANSGEO:85 for AFS being AffinSpace for f, g being Permutation of the carrier of AFS st f is collineation & g is collineation holds ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation ) proof let AFS be AffinSpace; ::_thesis: for f, g being Permutation of the carrier of AFS st f is collineation & g is collineation holds ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation ) let f, g be Permutation of the carrier of AFS; ::_thesis: ( f is collineation & g is collineation implies ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation ) ) assume ( f is_automorphism_of the CONGR of AFS & g is_automorphism_of the CONGR of AFS ) ; :: according to TRANSGEO:def_12 ::_thesis: ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation ) hence ( f " is_automorphism_of the CONGR of AFS & f * g is_automorphism_of the CONGR of AFS ) by Th17, Th18; :: according to TRANSGEO:def_12 ::_thesis: id the carrier of AFS is collineation thus id the carrier of AFS is_automorphism_of the CONGR of AFS by Th16; :: according to TRANSGEO:def_12 ::_thesis: verum end; theorem Th86: :: TRANSGEO:86 for AFS being AffinSpace for a being Element of AFS for f being Permutation of the carrier of AFS for A being Subset of AFS st a in A holds f . a in f .: A proof let AFS be AffinSpace; ::_thesis: for a being Element of AFS for f being Permutation of the carrier of AFS for A being Subset of AFS st a in A holds f . a in f .: A let a be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS for A being Subset of AFS st a in A holds f . a in f .: A let f be Permutation of the carrier of AFS; ::_thesis: for A being Subset of AFS st a in A holds f . a in f .: A let A be Subset of AFS; ::_thesis: ( a in A implies f . a in f .: A ) A1: dom f = the carrier of AFS by FUNCT_2:52; assume a in A ; ::_thesis: f . a in f .: A hence f . a in f .: A by A1, FUNCT_1:def_6; ::_thesis: verum end; theorem Th87: :: TRANSGEO:87 for AFS being AffinSpace for x being Element of AFS for f being Permutation of the carrier of AFS for A being Subset of AFS holds ( x in f .: A iff ex y being Element of AFS st ( y in A & f . y = x ) ) proof let AFS be AffinSpace; ::_thesis: for x being Element of AFS for f being Permutation of the carrier of AFS for A being Subset of AFS holds ( x in f .: A iff ex y being Element of AFS st ( y in A & f . y = x ) ) let x be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS for A being Subset of AFS holds ( x in f .: A iff ex y being Element of AFS st ( y in A & f . y = x ) ) let f be Permutation of the carrier of AFS; ::_thesis: for A being Subset of AFS holds ( x in f .: A iff ex y being Element of AFS st ( y in A & f . y = x ) ) let A be Subset of AFS; ::_thesis: ( x in f .: A iff ex y being Element of AFS st ( y in A & f . y = x ) ) thus ( x in f .: A implies ex y being Element of AFS st ( y in A & f . y = x ) ) ::_thesis: ( ex y being Element of AFS st ( y in A & f . y = x ) implies x in f .: A ) proof assume x in f .: A ; ::_thesis: ex y being Element of AFS st ( y in A & f . y = x ) then ex y being set st ( y in dom f & y in A & x = f . y ) by FUNCT_1:def_6; hence ex y being Element of AFS st ( y in A & f . y = x ) ; ::_thesis: verum end; given y being Element of AFS such that A1: ( y in A & f . y = x ) ; ::_thesis: x in f .: A dom f = the carrier of AFS by FUNCT_2:52; hence x in f .: A by A1, FUNCT_1:def_6; ::_thesis: verum end; theorem Th88: :: TRANSGEO:88 for AFS being AffinSpace for f being Permutation of the carrier of AFS for A, C being Subset of AFS st f .: A = f .: C holds A = C proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS for A, C being Subset of AFS st f .: A = f .: C holds A = C let f be Permutation of the carrier of AFS; ::_thesis: for A, C being Subset of AFS st f .: A = f .: C holds A = C let A, C be Subset of AFS; ::_thesis: ( f .: A = f .: C implies A = C ) assume A1: f .: A = f .: C ; ::_thesis: A = C now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_A let b be set ; ::_thesis: ( b in C implies b in A ) assume A2: b in C ; ::_thesis: b in A then reconsider b9 = b as Element of AFS ; set y = f . b9; f . b9 in f .: C by A2, Th86; then ex a being Element of AFS st ( a in A & f . a = f . b9 ) by A1, Th87; hence b in A by FUNCT_2:58; ::_thesis: verum end; then A3: C c= A by TARSKI:def_3; now__::_thesis:_for_a_being_set_st_a_in_A_holds_ a_in_C let a be set ; ::_thesis: ( a in A implies a in C ) assume A4: a in A ; ::_thesis: a in C then reconsider a9 = a as Element of AFS ; set x = f . a9; f . a9 in f .: A by A4, Th86; then ex b being Element of AFS st ( b in C & f . b = f . a9 ) by A1, Th87; hence a in C by FUNCT_2:58; ::_thesis: verum end; then A c= C by TARSKI:def_3; hence A = C by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th89: :: TRANSGEO:89 for AFS being AffinSpace for a, b being Element of AFS for f being Permutation of the carrier of AFS st f is collineation holds f .: (Line (a,b)) = Line ((f . a),(f . b)) proof let AFS be AffinSpace; ::_thesis: for a, b being Element of AFS for f being Permutation of the carrier of AFS st f is collineation holds f .: (Line (a,b)) = Line ((f . a),(f . b)) let a, b be Element of AFS; ::_thesis: for f being Permutation of the carrier of AFS st f is collineation holds f .: (Line (a,b)) = Line ((f . a),(f . b)) let f be Permutation of the carrier of AFS; ::_thesis: ( f is collineation implies f .: (Line (a,b)) = Line ((f . a),(f . b)) ) assume A1: f is collineation ; ::_thesis: f .: (Line (a,b)) = Line ((f . a),(f . b)) now__::_thesis:_for_x_being_set_st_x_in_Line_((f_._a),(f_._b))_holds_ x_in_f_.:_(Line_(a,b)) let x be set ; ::_thesis: ( x in Line ((f . a),(f . b)) implies x in f .: (Line (a,b)) ) assume A2: x in Line ((f . a),(f . b)) ; ::_thesis: x in f .: (Line (a,b)) then reconsider x9 = x as Element of AFS ; consider y being Element of AFS such that A3: f . y = x9 by Th1; LIN f . a,f . b,f . y by A2, A3, AFF_1:def_2; then LIN a,b,y by A1, Th84; then y in Line (a,b) by AFF_1:def_2; hence x in f .: (Line (a,b)) by A3, Th87; ::_thesis: verum end; then A4: Line ((f . a),(f . b)) c= f .: (Line (a,b)) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_f_.:_(Line_(a,b))_holds_ x_in_Line_((f_._a),(f_._b)) let x be set ; ::_thesis: ( x in f .: (Line (a,b)) implies x in Line ((f . a),(f . b)) ) assume A5: x in f .: (Line (a,b)) ; ::_thesis: x in Line ((f . a),(f . b)) then reconsider x9 = x as Element of AFS ; consider y being Element of AFS such that A6: y in Line (a,b) and A7: f . y = x9 by A5, Th87; LIN a,b,y by A6, AFF_1:def_2; then LIN f . a,f . b,x9 by A1, A7, Th84; hence x in Line ((f . a),(f . b)) by AFF_1:def_2; ::_thesis: verum end; then f .: (Line (a,b)) c= Line ((f . a),(f . b)) by TARSKI:def_3; hence f .: (Line (a,b)) = Line ((f . a),(f . b)) by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TRANSGEO:90 for AFS being AffinSpace for f being Permutation of the carrier of AFS for K being Subset of AFS st f is collineation & K is being_line holds f .: K is being_line proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS for K being Subset of AFS st f is collineation & K is being_line holds f .: K is being_line let f be Permutation of the carrier of AFS; ::_thesis: for K being Subset of AFS st f is collineation & K is being_line holds f .: K is being_line let K be Subset of AFS; ::_thesis: ( f is collineation & K is being_line implies f .: K is being_line ) assume that A1: f is collineation and A2: K is being_line ; ::_thesis: f .: K is being_line consider a, b being Element of AFS such that A3: a <> b and A4: K = Line (a,b) by A2, AFF_1:def_3; set q = f . b; set p = f . a; A5: f . a <> f . b by A3, FUNCT_2:58; f .: K = Line ((f . a),(f . b)) by A1, A4, Th89; hence f .: K is being_line by A5, AFF_1:def_3; ::_thesis: verum end; theorem Th91: :: TRANSGEO:91 for AFS being AffinSpace for f being Permutation of the carrier of AFS for A, C being Subset of AFS st f is collineation & A // C holds f .: A // f .: C proof let AFS be AffinSpace; ::_thesis: for f being Permutation of the carrier of AFS for A, C being Subset of AFS st f is collineation & A // C holds f .: A // f .: C let f be Permutation of the carrier of AFS; ::_thesis: for A, C being Subset of AFS st f is collineation & A // C holds f .: A // f .: C let A, C be Subset of AFS; ::_thesis: ( f is collineation & A // C implies f .: A // f .: C ) assume that A1: f is collineation and A2: A // C ; ::_thesis: f .: A // f .: C consider a, b, c, d being Element of AFS such that A3: ( a <> b & c <> d ) and A4: a,b // c,d and A5: ( A = Line (a,b) & C = Line (c,d) ) by A2, AFF_1:37; A6: f . a,f . b // f . c,f . d by A1, A4, Th83; A7: ( f . a <> f . b & f . c <> f . d ) by A3, FUNCT_2:58; ( f .: A = Line ((f . a),(f . b)) & f .: C = Line ((f . c),(f . d)) ) by A1, A5, Th89; hence f .: A // f .: C by A7, A6, AFF_1:37; ::_thesis: verum end; theorem :: TRANSGEO:92 for AFP being AffinPlane for f being Permutation of the carrier of AFP st ( for A being Subset of AFP st A is being_line holds f .: A is being_line ) holds f is collineation proof let AFP be AffinPlane; ::_thesis: for f being Permutation of the carrier of AFP st ( for A being Subset of AFP st A is being_line holds f .: A is being_line ) holds f is collineation let f be Permutation of the carrier of AFP; ::_thesis: ( ( for A being Subset of AFP st A is being_line holds f .: A is being_line ) implies f is collineation ) assume A1: for A being Subset of AFP st A is being_line holds f .: A is being_line ; ::_thesis: f is collineation A2: for a, b being Element of AFP st a <> b holds f .: (Line (a,b)) = Line ((f . a),(f . b)) proof let a, b be Element of AFP; ::_thesis: ( a <> b implies f .: (Line (a,b)) = Line ((f . a),(f . b)) ) set A = Line (a,b); set x = f . a; set y = f . b; set K = Line ((f . a),(f . b)); set M = f .: (Line (a,b)); assume A3: a <> b ; ::_thesis: f .: (Line (a,b)) = Line ((f . a),(f . b)) then f . a <> f . b by FUNCT_2:58; then A4: Line ((f . a),(f . b)) is being_line by AFF_1:def_3; Line (a,b) is being_line by A3, AFF_1:def_3; then A5: f .: (Line (a,b)) is being_line by A1; a in Line (a,b) by AFF_1:15; then A6: f . a in f .: (Line (a,b)) by Th86; b in Line (a,b) by AFF_1:15; then A7: f . b in f .: (Line (a,b)) by Th86; ( f . a in Line ((f . a),(f . b)) & f . b in Line ((f . a),(f . b)) ) by AFF_1:15; hence f .: (Line (a,b)) = Line ((f . a),(f . b)) by A3, A4, A5, A6, A7, AFF_1:18, FUNCT_2:58; ::_thesis: verum end; A8: for A being Subset of AFP st f .: A is being_line holds A is being_line proof let A be Subset of AFP; ::_thesis: ( f .: A is being_line implies A is being_line ) set K = f .: A; assume f .: A is being_line ; ::_thesis: A is being_line then consider x, y being Element of AFP such that A9: x <> y and A10: f .: A = Line (x,y) by AFF_1:def_3; y in f .: A by A10, AFF_1:15; then consider b being Element of AFP such that b in A and A11: f . b = y by Th87; x in f .: A by A10, AFF_1:15; then consider a being Element of AFP such that a in A and A12: f . a = x by Th87; set C = Line (a,b); ( Line (a,b) is being_line & f .: (Line (a,b)) = f .: A ) by A2, A9, A10, A12, A11, AFF_1:def_3; hence A is being_line by Th88; ::_thesis: verum end; A13: for A, C being Subset of AFP st f .: A // f .: C holds A // C proof let A, C be Subset of AFP; ::_thesis: ( f .: A // f .: C implies A // C ) set K = f .: A; set M = f .: C; assume A14: f .: A // f .: C ; ::_thesis: A // C then f .: C is being_line by AFF_1:36; then A15: C is being_line by A8; f .: A is being_line by A14, AFF_1:36; then A16: A is being_line by A8; now__::_thesis:_(_A_<>_C_implies_A_//_C_) assume A17: A <> C ; ::_thesis: A // C assume not A // C ; ::_thesis: contradiction then consider p being Element of AFP such that A18: ( p in A & p in C ) by A16, A15, AFF_1:58; set x = f . p; ( f . p in f .: A & f . p in f .: C ) by A18, Th86; hence contradiction by A14, A17, Th88, AFF_1:45; ::_thesis: verum end; hence A // C by A16, AFF_1:41; ::_thesis: verum end; A19: for a, b, c, d being Element of AFP st f . a,f . b // f . c,f . d holds a,b // c,d proof let a, b, c, d be Element of AFP; ::_thesis: ( f . a,f . b // f . c,f . d implies a,b // c,d ) set x = f . a; set y = f . b; set z = f . c; set t = f . d; assume A20: f . a,f . b // f . c,f . d ; ::_thesis: a,b // c,d now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_a,b_//_c,d_) set C = Line (c,d); set A = Line (a,b); set K = f .: (Line (a,b)); set M = f .: (Line (c,d)); A21: ( c in Line (c,d) & d in Line (c,d) ) by AFF_1:15; assume A22: ( a <> b & c <> d ) ; ::_thesis: a,b // c,d then A23: ( f . a <> f . b & f . c <> f . d ) by FUNCT_2:58; ( f .: (Line (a,b)) = Line ((f . a),(f . b)) & f .: (Line (c,d)) = Line ((f . c),(f . d)) ) by A2, A22; then A24: f .: (Line (a,b)) // f .: (Line (c,d)) by A20, A23, AFF_1:37; ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15; hence a,b // c,d by A13, A21, A24, AFF_1:39; ::_thesis: verum end; hence a,b // c,d by AFF_1:3; ::_thesis: verum end; A25: for A, C being Subset of AFP st A // C holds f .: A // f .: C proof let A, C be Subset of AFP; ::_thesis: ( A // C implies f .: A // f .: C ) assume A26: A // C ; ::_thesis: f .: A // f .: C then C is being_line by AFF_1:36; then A27: f .: C is being_line by A1; A is being_line by A26, AFF_1:36; then A28: f .: A is being_line by A1; then A29: f .: A // f .: A by AFF_1:41; ( A <> C implies f .: A // f .: C ) proof assume A30: A <> C ; ::_thesis: f .: A // f .: C assume not f .: A // f .: C ; ::_thesis: contradiction then consider x being Element of AFP such that A31: x in f .: A and A32: x in f .: C by A28, A27, AFF_1:58; consider b being Element of AFP such that A33: b in C and A34: x = f . b by A32, Th87; consider a being Element of AFP such that A35: a in A and A36: x = f . a by A31, Th87; a = b by A36, A34, FUNCT_2:58; hence contradiction by A26, A30, A35, A33, AFF_1:45; ::_thesis: verum end; hence f .: A // f .: C by A29; ::_thesis: verum end; for a, b, c, d being Element of AFP st a,b // c,d holds f . a,f . b // f . c,f . d proof let a, b, c, d be Element of AFP; ::_thesis: ( a,b // c,d implies f . a,f . b // f . c,f . d ) assume A37: a,b // c,d ; ::_thesis: f . a,f . b // f . c,f . d now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_f_._a,f_._b_//_f_._c,f_._d_) set C = Line (c,d); set A = Line (a,b); set K = f .: (Line (a,b)); set M = f .: (Line (c,d)); a in Line (a,b) by AFF_1:15; then A38: f . a in f .: (Line (a,b)) by Th86; b in Line (a,b) by AFF_1:15; then A39: f . b in f .: (Line (a,b)) by Th86; d in Line (c,d) by AFF_1:15; then A40: f . d in f .: (Line (c,d)) by Th86; c in Line (c,d) by AFF_1:15; then A41: f . c in f .: (Line (c,d)) by Th86; assume ( a <> b & c <> d ) ; ::_thesis: f . a,f . b // f . c,f . d then Line (a,b) // Line (c,d) by A37, AFF_1:37; hence f . a,f . b // f . c,f . d by A25, A38, A39, A41, A40, AFF_1:39; ::_thesis: verum end; hence f . a,f . b // f . c,f . d by AFF_1:3; ::_thesis: verum end; hence f is collineation by A19, Th83; ::_thesis: verum end; theorem :: TRANSGEO:93 for AFP being AffinPlane for K being Subset of AFP for p being Element of AFP for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & not p in K & f . p = p holds f = id the carrier of AFP proof let AFP be AffinPlane; ::_thesis: for K being Subset of AFP for p being Element of AFP for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & not p in K & f . p = p holds f = id the carrier of AFP let K be Subset of AFP; ::_thesis: for p being Element of AFP for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & not p in K & f . p = p holds f = id the carrier of AFP let p be Element of AFP; ::_thesis: for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & not p in K & f . p = p holds f = id the carrier of AFP let f be Permutation of the carrier of AFP; ::_thesis: ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & not p in K & f . p = p implies f = id the carrier of AFP ) assume that A1: f is collineation and A2: K is being_line and A3: for x being Element of AFP st x in K holds f . x = x and A4: not p in K and A5: f . p = p ; ::_thesis: f = id the carrier of AFP A6: for x being Element of AFP holds f . x = x proof let x be Element of AFP; ::_thesis: f . x = x now__::_thesis:_(_not_x_in_K_implies_f_._x_=_x_) assume not x in K ; ::_thesis: f . x = x consider a, b being Element of AFP such that A7: a in K and A8: b in K and A9: a <> b by A2, AFF_1:19; set A = Line (p,a); A10: p in Line (p,a) by AFF_1:15; f .: (Line (p,a)) = Line ((f . p),(f . a)) by A1, Th89; then A11: f .: (Line (p,a)) = Line (p,a) by A3, A5, A7; Line (p,a) is being_line by A4, A7, AFF_1:def_3; then consider C being Subset of AFP such that A12: x in C and A13: Line (p,a) // C by AFF_1:49; A14: C is being_line by A13, AFF_1:36; f .: (Line (p,a)) // f .: C by A1, A13, Th91; then A15: f .: C // C by A13, A11, AFF_1:44; A16: a in Line (p,a) by AFF_1:15; not C // K proof assume C // K ; ::_thesis: contradiction then Line (p,a) // K by A13, AFF_1:44; hence contradiction by A4, A7, A10, A16, AFF_1:45; ::_thesis: verum end; then consider c being Element of AFP such that A17: c in C and A18: c in K by A2, A14, AFF_1:58; f . c = c by A3, A18; then c in f .: C by A17, Th86; then A19: f .: C = C by A17, A15, AFF_1:45; set M = Line (p,b); A20: b in Line (p,b) by AFF_1:15; f .: (Line (p,b)) = Line ((f . p),(f . b)) by A1, Th89; then A21: f .: (Line (p,b)) = Line (p,b) by A3, A5, A8; Line (p,b) is being_line by A4, A8, AFF_1:def_3; then consider D being Subset of AFP such that A22: x in D and A23: Line (p,b) // D by AFF_1:49; A24: D is being_line by A23, AFF_1:36; f .: (Line (p,b)) // f .: D by A1, A23, Th91; then A25: f .: D // D by A23, A21, AFF_1:44; A26: p in Line (p,b) by AFF_1:15; not D // K proof assume D // K ; ::_thesis: contradiction then Line (p,b) // K by A23, AFF_1:44; hence contradiction by A4, A8, A26, A20, AFF_1:45; ::_thesis: verum end; then consider d being Element of AFP such that A27: d in D and A28: d in K by A2, A24, AFF_1:58; f . d = d by A3, A28; then d in f .: D by A27, Th86; then A29: f .: D = D by A27, A25, AFF_1:45; A30: Line (p,a) is being_line by A13, AFF_1:36; x = f . x proof assume A31: x <> f . x ; ::_thesis: contradiction ( f . x in C & f . x in D ) by A12, A22, A19, A29, Th86; then C = D by A12, A22, A14, A24, A31, AFF_1:18; then Line (p,a) // Line (p,b) by A13, A23, AFF_1:44; then Line (p,a) = Line (p,b) by A10, A26, AFF_1:45; hence contradiction by A2, A4, A7, A8, A9, A30, A10, A16, A20, AFF_1:18; ::_thesis: verum end; hence f . x = x ; ::_thesis: verum end; hence f . x = x by A3; ::_thesis: verum end; for x being Element of AFP holds f . x = (id the carrier of AFP) . x proof let x be Element of AFP; ::_thesis: f . x = (id the carrier of AFP) . x f . x = x by A6; hence f . x = (id the carrier of AFP) . x by FUNCT_1:18; ::_thesis: verum end; hence f = id the carrier of AFP by FUNCT_2:63; ::_thesis: verum end;