let a be Real; for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds
( f is onto & f is isometric )
consider A being Real such that
A1:
A = ((2 * PI) * (- [\(a / (2 * PI))/])) + a
and
A2:
0 <= A
and
A3:
A < 2 * PI
by COMPLEX2:1;
reconsider A = A as Real ;
let f be Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)); ( f = Rotate a implies ( f is onto & f is isometric ) )
assume A4:
f = Rotate a
; ( f is onto & f is isometric )
reconsider g = f as Function of (Euclid 2),(Euclid 2) ;
A5:
Rotate A = Rotate a
by A1, Lm3;
( g is onto & g is isometric )
proof
thus
rng g = the
carrier of
(Euclid 2)
FUNCT_2:def 3 g is isometric 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
object ;
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:67;
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:48;
set qz =
Rotate (
pz,
(- A));
A8:
|.(Rotate (pz,(- A))).| = |.pz.|
by COMPLEX2:53;
(
(Arg pz) - A <= Arg pz &
Arg pz < 2
* PI )
by A2, COMPTRIG:34, XREAL_1:43;
then A9:
(- A) + (Arg pz) < 2
* PI
by XXREAL_0:2;
Rotate (
pz,
(- A))
<> 0
by A6, COMPLEX2:52;
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, COMPTRIG:62;
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:52
.=
|[(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:52
.=
|[(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:52
.=
|[(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:52
.=
|[(Re (Rotate ((Rotate (pz,(- A))),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * <i>)),A)))]|
by COMPLEX1:13
.=
|[(Re pz),(Im pz)]|
by A10, COMPLEX1:13
.=
|[(p `1),(Im pz)]|
by COMPLEX1:12
.=
|[(p `1),(p `2)]|
by COMPLEX1:12
.=
p
by EUCLID:53
;
hence
o in rng g
by A11, Lm1, FUNCT_1:def 3;
verum end; suppose
A > Arg pz
;
o in rng gthen
(Arg pz) - A < 0
by XREAL_1:49;
then A12:
(2 * PI) + ((Arg pz) - A) < 2
* PI
by XREAL_1:30;
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:53;
then
Rotate (
pz,
(- A))
= (|.(Rotate (pz,(- A))).| * (cos (((2 * PI) * 1) + ((- A) + (Arg pz))))) + ((|.(Rotate (pz,(- A))).| * (sin ((- A) + (Arg pz)))) * <i>)
by COMPLEX2:9;
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:8;
(
0 <= (2 * PI) - A &
Arg pz >= 0 )
by A3, COMPTRIG:34, XREAL_1:48;
then A16:
0 <= ((2 * PI) - A) + (Arg pz)
;
Rotate (
pz,
(- A))
<> 0
by A6, COMPLEX2:52;
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:9;
then
Rotate (
(Rotate (pz,(- A))),
A)
= (|.(Rotate (pz,(- A))).| * (cos (Arg pz))) + ((|.(Rotate (pz,(- A))).| * (sin (Arg pz))) * <i>)
by COMPLEX2:8;
then A17:
Rotate (
(Rotate (pz,(- A))),
A)
= pz
by A14, COMPTRIG:62;
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:52
.=
|[(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:52
.=
|[(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:52
.=
|[(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:52
.=
|[(Re (Rotate ((Rotate (pz,(- A))),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * <i>)),A)))]|
by COMPLEX1:13
.=
|[(Re pz),(Im pz)]|
by A17, COMPLEX1:13
.=
|[(p `1),(Im pz)]|
by COMPLEX1:12
.=
|[(p `1),(p `2)]|
by COMPLEX1:12
.=
p
by EUCLID:53
;
hence
o in rng g
by A13, Lm1, FUNCT_1:def 3;
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:4, COMPLEX1:12;
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:52
.=
|[(Re (Rotate ((z + (z * <i>)),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),a)))]|
by EUCLID:52
.=
|[(Re (Rotate ((z + (z * <i>)),a))),(Im (Rotate ((z + ((|[0,0]| `2) * <i>)),a)))]|
by EUCLID:52
.=
|[(Re (Rotate (z,a))),(Im (Rotate (z,a)))]|
by EUCLID:52
.=
|[(Re z),(Im (Rotate (z,a)))]|
by COMPLEX2:52
.=
|[(Re z),(Im z)]|
by COMPLEX2:52
.=
p
by A18, A20, COMPLEX1:4, EUCLID:53
;
hence
o in rng g
by A19, Lm1, FUNCT_1:def 3;
verum end;
end;
let X,
Y be
Point of
(Euclid 2);
VECTMETR:def 3 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:67;
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:52;
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:52;
A23:
(
Re ((y `1) + ((y `2) * <i>)) = y `1 &
Im ((y `1) + ((y `2) * <i>)) = y `2 )
by COMPLEX1:12;
A24:
((sin a) ^2) + ((cos a) ^2) = 1
by SIN_COS:29;
A25:
(
Re ((x `1) + ((x `2) * <i>)) = x `1 &
Im ((x `1) + ((x `2) * <i>)) = x `2 )
by COMPLEX1:12;
(
x = |[(x `1),(x `2)]| &
y = |[(y `1),(y `2)]| )
by EUCLID:53;
hence dist (
X,
Y) =
sqrt ((((x `1) - (y `1)) ^2) + (((x `2) - (y `2)) ^2))
by GOBOARD6:6
.=
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:56
.=
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:56
.=
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:56
.=
sqrt ((((Re (Rotate (xx,a))) - (Re (Rotate (yy,a)))) ^2) + (((Im (Rotate (xx,a))) - (Im (Rotate (yy,a)))) ^2))
by A23, COMPLEX2:56
.=
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:92
.=
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 onto & f is isometric )
; verum