let sn be Real; :: thesis: for p being Point of (TOP-REAL 2) holds |.((sn -FanMorphW) . p).| = |.p.|
let p be Point of (TOP-REAL 2); :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
set z = (sn -FanMorphW) . p;
reconsider q = p, qz = (sn -FanMorphW) . p as Point of (TOP-REAL 2) ;
per cases ( ( (q `2) / |.q.| >= sn & q `1 < 0 ) or ( (q `2) / |.q.| < sn & q `1 < 0 ) or q `1 >= 0 ) ;
suppose A1: ( (q `2) / |.q.| >= sn & q `1 < 0 ) ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
then A2: (sn -FanMorphW) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| by Th23;
then A3: qz `1 = |.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))) by EUCLID:56;
A4: qz `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)) by A2, EUCLID:56;
A5: ((q `2) / |.q.|) - sn >= 0 by A1, XREAL_1:50;
A6: |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) by JGRAPH_3:10;
|.q.| <> 0 by A1, JGRAPH_2:11, TOPRNS_1:25;
then A7: |.q.| ^2 > 0 by SQUARE_1:74;
0 <= (q `1) ^2 by XREAL_1:65;
then 0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) by XREAL_1:9;
then ((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2) by A6, XREAL_1:74;
then ((q `2) ^2) / (|.q.| ^2) <= 1 by A7, XCMPLX_1:60;
then ((q `2) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (q `2) / |.q.| by SQUARE_1:121;
then A8: 1 - sn >= ((q `2) / |.q.|) - sn by XREAL_1:11;
per cases ( 1 - sn = 0 or 1 - sn <> 0 ) ;
suppose A9: 1 - sn = 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
A10: (((q `2) / |.q.|) - sn) / (1 - sn) = (((q `2) / |.q.|) - sn) * ((1 - sn) ") by XCMPLX_0:def 9
.= (((q `2) / |.q.|) - sn) * 0 by A9
.= 0 ;
then - (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))) = - 1 by SQUARE_1:83;
then (sn -FanMorphW) . q = |[(|.q.| * (- 1)),(|.q.| * 0)]| by A1, A10, Th23
.= |[(- |.q.|),0]| ;
then ( ((sn -FanMorphW) . q) `1 = - |.q.| & ((sn -FanMorphW) . q) `2 = 0 ) by EUCLID:56;
then |.((sn -FanMorphW) . p).| = sqrt (((- |.q.|) ^2) + (0 ^2)) by JGRAPH_3:10
.= sqrt (|.q.| ^2)
.= |.q.| by SQUARE_1:89 ;
hence |.((sn -FanMorphW) . p).| = |.p.| ; :: thesis: verum
end;
suppose A11: 1 - sn <> 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
per cases ( 1 - sn > 0 or 1 - sn < 0 ) by A11;
suppose A12: 1 - sn > 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
- (1 - sn) <= - (((q `2) / |.q.|) - sn) by A8, XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((q `2) / |.q.|) - sn)) / (1 - sn) by A12, XREAL_1:74;
then - 1 <= (- (((q `2) / |.q.|) - sn)) / (1 - sn) by A12, XCMPLX_1:198;
then ((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A5, A12, SQUARE_1:119;
then 1 - (((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2) >= 0 by XREAL_1:50;
then A13: 1 - ((- ((((q `2) / |.q.|) - sn) / (1 - sn))) ^2) >= 0 by XCMPLX_1:188;
A14: (qz `1) ^2 = (|.q.| ^2) * ((sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))) ^2) by A3
.= (|.q.| ^2) * (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)) by A13, SQUARE_1:def 4 ;
|.qz.| ^2 = ((qz `1) ^2) + ((qz `2) ^2) by JGRAPH_3:10
.= |.q.| ^2 by A4, A14 ;
then sqrt (|.qz.| ^2) = |.q.| by SQUARE_1:89;
hence |.((sn -FanMorphW) . p).| = |.p.| by SQUARE_1:89; :: thesis: verum
end;
end;
end;
end;
end;
suppose A17: ( (q `2) / |.q.| < sn & q `1 < 0 ) ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
then |.q.| <> 0 by JGRAPH_2:11, TOPRNS_1:25;
then A18: |.q.| ^2 > 0 by SQUARE_1:74;
A19: ((q `2) / |.q.|) - sn < 0 by A17, XREAL_1:51;
A20: |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) by JGRAPH_3:10;
0 <= (q `1) ^2 by XREAL_1:65;
then 0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) by XREAL_1:9;
then ((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2) by A20, XREAL_1:74;
then ((q `2) ^2) / (|.q.| ^2) <= 1 by A18, XCMPLX_1:60;
then ((q `2) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (q `2) / |.q.| by SQUARE_1:121;
then A21: (- 1) - sn <= ((q `2) / |.q.|) - sn by XREAL_1:11;
A22: (sn -FanMorphW) . q = |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]| by A17, Th24;
then A23: qz `1 = |.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))) by EUCLID:56;
A24: qz `2 = |.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)) by A22, EUCLID:56;
per cases ( 1 + sn = 0 or 1 + sn <> 0 ) ;
suppose A25: 1 + sn = 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
(((q `2) / |.q.|) - sn) / (1 + sn) = (((q `2) / |.q.|) - sn) * ((1 + sn) ") by XCMPLX_0:def 9
.= (((q `2) / |.q.|) - sn) * 0 by A25
.= 0 ;
then ( ((sn -FanMorphW) . q) `1 = - |.q.| & ((sn -FanMorphW) . q) `2 = 0 ) by A22, EUCLID:56, SQUARE_1:83;
then |.((sn -FanMorphW) . p).| = sqrt (((- |.q.|) ^2) + (0 ^2)) by JGRAPH_3:10
.= sqrt (|.q.| ^2)
.= |.q.| by SQUARE_1:89 ;
hence |.((sn -FanMorphW) . p).| = |.p.| ; :: thesis: verum
end;
suppose A26: 1 + sn <> 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
per cases ( 1 + sn > 0 or 1 + sn < 0 ) by A26;
suppose A27: 1 + sn > 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
then (- (1 + sn)) / (1 + sn) <= (((q `2) / |.q.|) - sn) / (1 + sn) by A21, XREAL_1:74;
then - 1 <= (((q `2) / |.q.|) - sn) / (1 + sn) by A27, XCMPLX_1:198;
then ((((q `2) / |.q.|) - sn) / (1 + sn)) ^2 <= 1 ^2 by A19, A27, SQUARE_1:119;
then A28: 1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2) >= 0 by XREAL_1:50;
A29: (qz `1) ^2 = (|.q.| ^2) * ((sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))) ^2) by A23
.= (|.q.| ^2) * (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)) by A28, SQUARE_1:def 4 ;
|.qz.| ^2 = ((qz `1) ^2) + ((qz `2) ^2) by JGRAPH_3:10
.= |.q.| ^2 by A24, A29 ;
then sqrt (|.qz.| ^2) = |.q.| by SQUARE_1:89;
hence |.((sn -FanMorphW) . p).| = |.p.| by SQUARE_1:89; :: thesis: verum
end;
end;
end;
end;
end;
suppose q `1 >= 0 ; :: thesis: |.((sn -FanMorphW) . p).| = |.p.|
hence |.((sn -FanMorphW) . p).| = |.p.| by Th23; :: thesis: verum
end;
end;