thus rng g = the carrier of (Euclid 2) :: according to FUNCT_2:def 3 :: thesis: g is isometric let X, Y be Point of (Euclid 2); :: according to VECTMETR:def 3 :: 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: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 ;
:: thesis: verum