let a be Real; :: thesis: for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds
f is isometric
consider A being real number such that
B1:
A = ((2 * PI ) * (- [\(a / (2 * PI ))/])) + a
and
A1:
( 0 <= A & A < 2 * PI )
by COMPLEX2:2;
reconsider A = A as Real by XREAL_0:def 1;
let f be Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)); :: thesis: ( f = Rotate a implies f is isometric )
assume A2:
f = Rotate a
; :: thesis: f is isometric
B3:
Rotate A = Rotate a
by B1, Lm2;
reconsider g = f as Function of (Euclid 2),(Euclid 2) ;
g is isometric
proof
thus
rng g = the
carrier of
(Euclid 2)
:: according to VECTMETR:def 3 :: thesis: for b1, b2 being Element of the carrier of (Euclid 2) holds dist b1,b2 = dist (g . b1),(g . b2)proof
thus
rng g c= the
carrier of
(Euclid 2)
;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (Euclid 2) c= rng g
let o be
set ;
:: according to TARSKI:def 3 :: thesis: ( not o in the carrier of (Euclid 2) or o in rng g )
assume
o in the
carrier of
(Euclid 2)
;
:: thesis: o in rng g
then reconsider p =
o as
Point of
(TOP-REAL 2) by EUCLID:71;
set pz =
(p `1 ) + ((p `2 ) * <i> );
reconsider pz =
(p `1 ) + ((p `2 ) * <i> ) as
Element of
COMPLEX by XCMPLX_0:def 2;
set arg =
Arg pz;
per cases
( pz <> 0 or pz = 0 )
;
suppose A3:
pz <> 0
;
:: thesis: o in rng gper cases
( A <= Arg pz or A > Arg pz )
;
suppose A4:
A <= Arg pz
;
:: thesis: o in rng gset qz =
Rotate pz,
(- A);
A5:
Rotate pz,
(- A) <> 0
by A3, COMPLEX2:66;
A6:
0 <= (Arg pz) - A
by A4, XREAL_1:50;
(
(Arg pz) - A <= Arg pz &
Arg pz < 2
* PI )
by A1, COMPTRIG:52, XREAL_1:45;
then A7:
(- A) + (Arg pz) < 2
* PI
by XXREAL_0:2;
A8:
|.(Rotate pz,(- A)).| = |.pz.|
by COMPLEX2:67;
then
Arg (Rotate pz,(- A)) = (- A) + (Arg pz)
by A5, A6, A7, COMPTRIG:def 1;
then A9:
Rotate (Rotate pz,(- A)),
A = pz
by A8, COMPLEX2:19;
set q =
|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]|;
A10:
dom g = the
carrier of
(Euclid 2)
by FUNCT_2:def 1;
g . |[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| =
|[(Re (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by A2, B3, Def3
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate (Rotate pz,(- A)),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]|
by COMPLEX1:29
.=
|[(Re pz),(Im pz)]|
by A9, COMPLEX1:29
.=
|[(p `1 ),(Im pz)]|
by COMPLEX1:28
.=
|[(p `1 ),(p `2 )]|
by COMPLEX1:28
.=
p
by EUCLID:57
;
hence
o in rng g
by A10, FUNCT_1:def 5, XX;
:: thesis: verum end; suppose A11:
A > Arg pz
;
:: thesis: o in rng gset qz =
Rotate pz,
(- A);
A12:
Rotate pz,
(- A) <> 0
by A3, COMPLEX2:66;
(
0 <= (2 * PI ) - A &
Arg pz >= 0 )
by A1, COMPTRIG:52, XREAL_1:50;
then A13:
0 <= ((2 * PI ) - A) + (Arg pz)
;
(Arg pz) - A < 0
by A11, XREAL_1:51;
then A14:
(2 * PI ) + ((Arg pz) - A) < 2
* PI
by XREAL_1:32;
A15:
|.(Rotate pz,(- A)).| = |.pz.|
by COMPLEX2:67;
then
Rotate pz,
(- A) = (|.(Rotate pz,(- A)).| * (cos (((2 * PI ) * 1) + ((- A) + (Arg pz))))) + ((|.(Rotate pz,(- A)).| * (sin ((- A) + (Arg pz)))) * <i> )
by COMPLEX2:10;
then
Rotate pz,
(- A) = (|.(Rotate pz,(- A)).| * (cos ((2 * PI ) + ((Arg pz) - A)))) + ((|.(Rotate pz,(- A)).| * (sin (((2 * PI ) * 1) + ((- A) + (Arg pz))))) * <i> )
by COMPLEX2:9;
then
Arg (Rotate pz,(- A)) = (2 * PI ) + ((Arg pz) - A)
by A12, A13, A14, COMPTRIG:def 1;
then
Rotate (Rotate pz,(- A)),
A = (|.(Rotate pz,(- A)).| * (cos (Arg pz))) + ((|.(Rotate pz,(- A)).| * (sin (((2 * PI ) * 1) + (Arg pz)))) * <i> )
by COMPLEX2:10;
then
Rotate (Rotate pz,(- A)),
A = (|.(Rotate pz,(- A)).| * (cos (Arg pz))) + ((|.(Rotate pz,(- A)).| * (sin (Arg pz))) * <i> )
by COMPLEX2:9;
then A16:
Rotate (Rotate pz,(- A)),
A = pz
by A15, COMPLEX2:19;
set q =
|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]|;
A17:
dom g = the
carrier of
(Euclid 2)
by FUNCT_2:def 1;
g . |[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| =
|[(Re (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by A2, B3, Def3
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]|
by EUCLID:56
.=
|[(Re (Rotate (Rotate pz,(- A)),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]|
by COMPLEX1:29
.=
|[(Re pz),(Im pz)]|
by A16, COMPLEX1:29
.=
|[(p `1 ),(Im pz)]|
by COMPLEX1:28
.=
|[(p `1 ),(p `2 )]|
by COMPLEX1:28
.=
p
by EUCLID:57
;
hence
o in rng g
by A17, FUNCT_1:def 5, XX;
:: thesis: verum end; suppose
pz = 0
;
:: thesis: o in rng gthen A18:
(
p `1 = 0 &
p `2 = 0 )
by COMPLEX1:12, COMPLEX1:28;
set q =
|[0 ,0 ]|;
A19:
dom g = the
carrier of
(Euclid 2)
by FUNCT_2:def 1;
reconsider z =
0 as
Element of
COMPLEX by XCMPLX_0:def 2;
g . |[0 ,0 ]| =
|[(Re (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]|
by A2, Def3
.=
|[(Re (Rotate (z + ((|[0 ,0 ]| `2 ) * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]|
by EUCLID:56
.=
|[(Re (Rotate (z + (z * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]|
by EUCLID:56
.=
|[(Re (Rotate (z + (z * <i> )),a)),(Im (Rotate (z + ((|[0 ,0 ]| `2 ) * <i> )),a))]|
by EUCLID:56
.=
|[(Re (Rotate z,a)),(Im (Rotate z,a))]|
by EUCLID:56
.=
|[(Re z),(Im (Rotate z,a))]|
by COMPLEX2:66
.=
|[(Re z),(Im z)]|
by COMPLEX2:66
.=
p
by A18, COMPLEX1:12, EUCLID:57
;
hence
o in rng g
by A19, FUNCT_1:def 5, XX;
:: thesis: verum end;
end;
let X,
Y be
Point of
(Euclid 2);
:: thesis: dist X,Y = dist (g . X),(g . Y)
reconsider x =
X,
y =
Y,
gx =
g . X,
gy =
g . Y as
Point of
(TOP-REAL 2) by EUCLID:71;
A20:
(
|[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]| `1 = Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a) &
|[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]| `2 = Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a) )
by EUCLID:56;
A21:
(
|[(Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a)),(Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a))]| `1 = Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a) &
|[(Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a)),(Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a))]| `2 = Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a) )
by EUCLID:56;
reconsider xx =
(x `1 ) + ((x `2 ) * <i> ),
yy =
(y `1 ) + ((y `2 ) * <i> ) as
Element of
COMPLEX by XCMPLX_0:def 2;
A22:
(
Re ((x `1 ) + ((x `2 ) * <i> )) = x `1 &
Im ((x `1 ) + ((x `2 ) * <i> )) = x `2 )
by COMPLEX1:28;
A23:
(
Re ((y `1 ) + ((y `2 ) * <i> )) = y `1 &
Im ((y `1 ) + ((y `2 ) * <i> )) = y `2 )
by COMPLEX1:28;
A24:
((sin a) ^2 ) + ((cos a) ^2 ) = 1
by SIN_COS:32;
(
x = |[(x `1 ),(x `2 )]| &
y = |[(y `1 ),(y `2 )]| )
by EUCLID:57;
hence dist X,
Y =
sqrt ((((x `1 ) - (y `1 )) ^2 ) + (((x `2 ) - (y `2 )) ^2 ))
by GOBOARD6:9
.=
sqrt ((((((x `1 ) * (x `1 )) - ((2 * (x `1 )) * (y `1 ))) + ((y `1 ) * (y `1 ))) * (((sin a) * (sin a)) + ((cos a) * (cos a)))) + (((((x `2 ) * (x `2 )) - ((2 * (x `2 )) * (y `2 ))) + ((y `2 ) * (y `2 ))) * (((sin a) ^2 ) + ((cos a) ^2 ))))
by A24
.=
sqrt ((((((x `1 ) * (cos a)) - ((x `2 ) * (sin a))) - (((y `1 ) * (cos a)) - ((y `2 ) * (sin a)))) ^2 ) + ((((((x `1 ) * (sin a)) + ((x `2 ) * (cos a))) ^2 ) - ((2 * (((x `1 ) * (sin a)) + ((x `2 ) * (cos a)))) * (((y `1 ) * (sin a)) + ((y `2 ) * (cos a))))) + ((((y `1 ) * (sin a)) + ((y `2 ) * (cos a))) ^2 )))
.=
sqrt ((((Re (Rotate xx,a)) - (((y `1 ) * (cos a)) - ((y `2 ) * (sin a)))) ^2 ) + (((((x `1 ) * (sin a)) + ((x `2 ) * (cos a))) - (((y `1 ) * (sin a)) + ((y `2 ) * (cos a)))) ^2 ))
by A22, COMPLEX2:70
.=
sqrt ((((Re (Rotate xx,a)) - (((y `1 ) * (cos a)) - ((y `2 ) * (sin a)))) ^2 ) + (((Im (Rotate xx,a)) - (((y `1 ) * (sin a)) + ((y `2 ) * (cos a)))) ^2 ))
by A22, COMPLEX2:70
.=
sqrt ((((Re (Rotate xx,a)) - (Re (Rotate yy,a))) ^2 ) + (((Im (Rotate xx,a)) - (((y `1 ) * (sin a)) + ((y `2 ) * (cos a)))) ^2 ))
by A23, COMPLEX2:70
.=
sqrt ((((Re (Rotate xx,a)) - (Re (Rotate yy,a))) ^2 ) + (((Im (Rotate xx,a)) - (Im (Rotate yy,a))) ^2 ))
by A23, COMPLEX2:70
.=
dist |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]|,
|[(Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a)),(Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a))]|
by A20, A21, TOPREAL6:101
.=
dist |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]|,
gy
by A2, Def3
.=
dist gx,
gy
by A2, Def3
.=
dist (g . X),
(g . Y)
by TOPREAL6:def 1
;
:: thesis: verum
end;
hence
f is isometric
by Def2; :: thesis: verum