:: 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;