let cn be Real; :: thesis: for p being Point of (TOP-REAL 2) holds |.((cn -FanMorphS) . p).| = |.p.|
let p be Point of (TOP-REAL 2); :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
set f = cn -FanMorphS ;
set z = (cn -FanMorphS) . p;
set q = p;
reconsider qz = (cn -FanMorphS) . p as Point of (TOP-REAL 2) ;
per cases ( ( (p `1) / |.p.| >= cn & p `2 < 0 ) or ( (p `1) / |.p.| < cn & p `2 < 0 ) or p `2 >= 0 ) ;
suppose A1: ( (p `1) / |.p.| >= cn & p `2 < 0 ) ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
then A2: (cn -FanMorphS) . p = |[(|.p.| * ((((p `1) / |.p.|) - cn) / (1 - cn))),(|.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 - cn)) ^2)))))]| by Th113;
then A3: qz `2 = |.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 - cn)) ^2)))) by EUCLID:52;
A4: qz `1 = |.p.| * ((((p `1) / |.p.|) - cn) / (1 - cn)) by A2, EUCLID:52;
A5: ((p `1) / |.p.|) - cn >= 0 by A1, XREAL_1:48;
A6: |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2) by JGRAPH_3:1;
|.p.| <> 0 by A1, JGRAPH_2:3, TOPRNS_1:24;
then A7: |.p.| ^2 > 0 by SQUARE_1:12;
0 <= (p `2) ^2 by XREAL_1:63;
then 0 + ((p `1) ^2) <= ((p `1) ^2) + ((p `2) ^2) by XREAL_1:7;
then ((p `1) ^2) / (|.p.| ^2) <= (|.p.| ^2) / (|.p.| ^2) by A6, XREAL_1:72;
then ((p `1) ^2) / (|.p.| ^2) <= 1 by A7, XCMPLX_1:60;
then ((p `1) / |.p.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (p `1) / |.p.| by SQUARE_1:51;
then A8: 1 - cn >= ((p `1) / |.p.|) - cn by XREAL_1:9;
per cases ( 1 - cn = 0 or 1 - cn <> 0 ) ;
suppose A9: 1 - cn = 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
A10: (((p `1) / |.p.|) - cn) / (1 - cn) = (((p `1) / |.p.|) - cn) * ((1 - cn) ") by XCMPLX_0:def 9
.= (((p `1) / |.p.|) - cn) * 0 by A9
.= 0 ;
then 1 - (((((p `1) / |.p.|) - cn) / (1 - cn)) ^2) = 1 ;
then (cn -FanMorphS) . p = |[(|.p.| * 0),(|.p.| * (- 1))]| by A1, A10, Th113, SQUARE_1:18
.= |[0,(- |.p.|)]| ;
then ( ((cn -FanMorphS) . p) `2 = - |.p.| & ((cn -FanMorphS) . p) `1 = 0 ) by EUCLID:52;
then |.((cn -FanMorphS) . p).| = sqrt (((- |.p.|) ^2) + (0 ^2)) by JGRAPH_3:1
.= sqrt (|.p.| ^2)
.= |.p.| by SQUARE_1:22 ;
hence |.((cn -FanMorphS) . p).| = |.p.| ; :: thesis: verum
end;
suppose A11: 1 - cn <> 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
per cases ( 1 - cn > 0 or 1 - cn < 0 ) by A11;
suppose A12: 1 - cn > 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
- (1 - cn) <= - (((p `1) / |.p.|) - cn) by A8, XREAL_1:24;
then (- (1 - cn)) / (1 - cn) <= (- (((p `1) / |.p.|) - cn)) / (1 - cn) by A12, XREAL_1:72;
then - 1 <= (- (((p `1) / |.p.|) - cn)) / (1 - cn) by A12, XCMPLX_1:197;
then ((- (((p `1) / |.p.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A5, A12, SQUARE_1:49;
then 1 - (((- (((p `1) / |.p.|) - cn)) / (1 - cn)) ^2) >= 0 by XREAL_1:48;
then A13: 1 - ((- ((((p `1) / |.p.|) - cn) / (1 - cn))) ^2) >= 0 by XCMPLX_1:187;
A14: (qz `2) ^2 = (|.p.| ^2) * ((sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 - cn)) ^2))) ^2) by A3
.= (|.p.| ^2) * (1 - (((((p `1) / |.p.|) - cn) / (1 - cn)) ^2)) by A13, SQUARE_1:def 2 ;
|.qz.| ^2 = ((qz `1) ^2) + ((qz `2) ^2) by JGRAPH_3:1
.= |.p.| ^2 by A4, A14 ;
then sqrt (|.qz.| ^2) = |.p.| by SQUARE_1:22;
hence |.((cn -FanMorphS) . p).| = |.p.| by SQUARE_1:22; :: thesis: verum
end;
end;
end;
end;
end;
suppose A17: ( (p `1) / |.p.| < cn & p `2 < 0 ) ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
then |.p.| <> 0 by JGRAPH_2:3, TOPRNS_1:24;
then A18: |.p.| ^2 > 0 by SQUARE_1:12;
A19: ((p `1) / |.p.|) - cn < 0 by A17, XREAL_1:49;
A20: |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2) by JGRAPH_3:1;
0 <= (p `2) ^2 by XREAL_1:63;
then 0 + ((p `1) ^2) <= ((p `1) ^2) + ((p `2) ^2) by XREAL_1:7;
then ((p `1) ^2) / (|.p.| ^2) <= (|.p.| ^2) / (|.p.| ^2) by A20, XREAL_1:72;
then ((p `1) ^2) / (|.p.| ^2) <= 1 by A18, XCMPLX_1:60;
then ((p `1) / |.p.|) ^2 <= 1 by XCMPLX_1:76;
then - 1 <= (p `1) / |.p.| by SQUARE_1:51;
then A21: (- 1) - cn <= ((p `1) / |.p.|) - cn by XREAL_1:9;
A22: (cn -FanMorphS) . p = |[(|.p.| * ((((p `1) / |.p.|) - cn) / (1 + cn))),(|.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))))]| by A17, Th114;
then A23: qz `2 = |.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))) by EUCLID:52;
A24: qz `1 = |.p.| * ((((p `1) / |.p.|) - cn) / (1 + cn)) by A22, EUCLID:52;
per cases ( 1 + cn = 0 or 1 + cn <> 0 ) ;
suppose A25: 1 + cn = 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
(((p `1) / |.p.|) - cn) / (1 + cn) = (((p `1) / |.p.|) - cn) * ((1 + cn) ") by XCMPLX_0:def 9
.= (((p `1) / |.p.|) - cn) * 0 by A25
.= 0 ;
then ( ((cn -FanMorphS) . p) `2 = - |.p.| & ((cn -FanMorphS) . p) `1 = 0 ) by A22, EUCLID:52;
then |.((cn -FanMorphS) . p).| = sqrt (((- |.p.|) ^2) + (0 ^2)) by JGRAPH_3:1
.= sqrt (|.p.| ^2)
.= |.p.| by SQUARE_1:22 ;
hence |.((cn -FanMorphS) . p).| = |.p.| ; :: thesis: verum
end;
suppose A26: 1 + cn <> 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
per cases ( 1 + cn > 0 or 1 + cn < 0 ) by A26;
suppose A27: 1 + cn > 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
then (- (1 + cn)) / (1 + cn) <= (((p `1) / |.p.|) - cn) / (1 + cn) by A21, XREAL_1:72;
then - 1 <= (((p `1) / |.p.|) - cn) / (1 + cn) by A27, XCMPLX_1:197;
then ((((p `1) / |.p.|) - cn) / (1 + cn)) ^2 <= 1 ^2 by A19, A27, SQUARE_1:49;
then A28: 1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2) >= 0 by XREAL_1:48;
A29: (qz `2) ^2 = (|.p.| ^2) * ((sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2))) ^2) by A23
.= (|.p.| ^2) * (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)) by A28, SQUARE_1:def 2 ;
|.qz.| ^2 = ((qz `1) ^2) + ((qz `2) ^2) by JGRAPH_3:1
.= |.p.| ^2 by A24, A29 ;
then sqrt (|.qz.| ^2) = |.p.| by SQUARE_1:22;
hence |.((cn -FanMorphS) . p).| = |.p.| by SQUARE_1:22; :: thesis: verum
end;
end;
end;
end;
end;
suppose p `2 >= 0 ; :: thesis: |.((cn -FanMorphS) . p).| = |.p.|
hence |.((cn -FanMorphS) . p).| = |.p.| by Th113; :: thesis: verum
end;
end;