let a be Real; 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
A1:
A = ((2 * PI ) * (- [\(a / (2 * PI ))/])) + a
and
A2:
0 <= A
and
A3:
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)); ( f = Rotate a implies f is isometric )
assume A4:
f = Rotate a
; f is isometric
reconsider g = f as Function of (Euclid 2),(Euclid 2) ;
A5:
Rotate A = Rotate a
by A1, Lm3;
g is isometric
proof
thus
rng g = the
carrier of
(Euclid 2)
VECTMETR:def 3 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)
;
XBOOLE_0:def 10 the carrier of (Euclid 2) c= rng g
let o be
set ;
TARSKI:def 3 ( not o in the carrier of (Euclid 2) or o in rng g )
assume
o in the
carrier of
(Euclid 2)
;
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 A6:
pz <> 0
;
o in rng gper cases
( A <= Arg pz or A > Arg pz )
;
suppose
A <= Arg pz
;
o in rng gthen A7:
0 <= (Arg pz) - A
by XREAL_1:50;
set qz =
Rotate pz,
(- A);
A8:
|.(Rotate pz,(- A)).| = |.pz.|
by COMPLEX2:67;
(
(Arg pz) - A <= Arg pz &
Arg pz < 2
* PI )
by A2, COMPTRIG:52, XREAL_1:45;
then A9:
(- A) + (Arg pz) < 2
* PI
by XXREAL_0:2;
Rotate pz,
(- A) <> 0
by A6, COMPLEX2:66;
then
Arg (Rotate pz,(- A)) = (- A) + (Arg pz)
by A7, A9, A8, COMPTRIG:def 1;
then A10:
Rotate (Rotate pz,(- A)),
A = pz
by A8, COMPLEX2:19;
set q =
|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]|;
A11:
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 A4, A5, 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 A10, 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 A11, Lm1, FUNCT_1:def 5;
verum end; suppose
A > Arg pz
;
o in rng gthen
(Arg pz) - A < 0
by XREAL_1:51;
then A12:
(2 * PI ) + ((Arg pz) - A) < 2
* PI
by XREAL_1:32;
set qz =
Rotate pz,
(- A);
set q =
|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]|;
A13:
dom g = the
carrier of
(Euclid 2)
by FUNCT_2:def 1;
A14:
|.(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 A15:
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;
(
0 <= (2 * PI ) - A &
Arg pz >= 0 )
by A3, COMPTRIG:52, XREAL_1:50;
then A16:
0 <= ((2 * PI ) - A) + (Arg pz)
;
Rotate pz,
(- A) <> 0
by A6, COMPLEX2:66;
then
Arg (Rotate pz,(- A)) = (2 * PI ) + ((Arg pz) - A)
by A16, A12, A15, 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 A17:
Rotate (Rotate pz,(- A)),
A = pz
by A14, COMPLEX2:19;
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 A4, A5, 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 A17, 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 A13, Lm1, FUNCT_1:def 5;
verum end; suppose A18:
pz = 0
;
o in rng greconsider z =
0 as
Element of
COMPLEX by XCMPLX_0:def 2;
set q =
|[0 ,0 ]|;
A19:
dom g = the
carrier of
(Euclid 2)
by FUNCT_2:def 1;
A20:
p `1 = 0
by A18, COMPLEX1:12, COMPLEX1:28;
g . |[0 ,0 ]| =
|[(Re (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]|
by A4, 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, A20, COMPLEX1:12, EUCLID:57
;
hence
o in rng g
by A19, Lm1, FUNCT_1:def 5;
verum end;
end;
let X,
Y be
Point of
(Euclid 2);
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;
A21:
(
|[(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;
reconsider xx =
(x `1 ) + ((x `2 ) * <i> ),
yy =
(y `1 ) + ((y `2 ) * <i> ) as
Element of
COMPLEX by XCMPLX_0:def 2;
A22:
(
|[(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;
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;
A25:
(
Re ((x `1 ) + ((x `2 ) * <i> )) = x `1 &
Im ((x `1 ) + ((x `2 ) * <i> )) = x `2 )
by COMPLEX1:28;
(
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 A25, 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 A25, 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 A21, A22, TOPREAL6:101
.=
dist |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]|,
gy
by A4, Def3
.=
dist gx,
gy
by A4, Def3
.=
dist (g . X),
(g . Y)
by TOPREAL6:def 1
;
verum
end;
hence
f is isometric
by Def2; verum