let cn be Real; :: thesis: ( - 1 < cn & cn < 1 implies cn -FanMorphS is one-to-one )
assume A1:
( - 1 < cn & cn < 1 )
; :: thesis: cn -FanMorphS is one-to-one
for x1, x2 being set st x1 in dom (cn -FanMorphS ) & x2 in dom (cn -FanMorphS ) & (cn -FanMorphS ) . x1 = (cn -FanMorphS ) . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom (cn -FanMorphS ) & x2 in dom (cn -FanMorphS ) & (cn -FanMorphS ) . x1 = (cn -FanMorphS ) . x2 implies x1 = x2 )
assume A2:
(
x1 in dom (cn -FanMorphS ) &
x2 in dom (cn -FanMorphS ) &
(cn -FanMorphS ) . x1 = (cn -FanMorphS ) . x2 )
;
:: thesis: x1 = x2
then reconsider p1 =
x1 as
Point of
(TOP-REAL 2) ;
reconsider p2 =
x2 as
Point of
(TOP-REAL 2) by A2;
set q =
p1;
set p =
p2;
A3:
1
- cn > 0
by A1, XREAL_1:151;
per cases
( p1 `2 >= 0 or ( (p1 `1 ) / |.p1.| >= cn & p1 `2 <= 0 & p1 <> 0. (TOP-REAL 2) ) or ( (p1 `1 ) / |.p1.| < cn & p1 `2 <= 0 & p1 <> 0. (TOP-REAL 2) ) )
by JGRAPH_2:11;
suppose A4:
p1 `2 >= 0
;
:: thesis: x1 = x2then A5:
(cn -FanMorphS ) . p1 = p1
by Th120;
per cases
( p2 `2 >= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| < cn & p2 `2 <= 0 ) )
by JGRAPH_2:11;
suppose A6:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| >= cn &
p2 `2 <= 0 )
;
:: thesis: x1 = x2then A7:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, Th122;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|;
A8:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))) &
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) )
by EUCLID:56;
A9:
(
p1 `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))) &
p1 `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) )
by A2, A5, A7, EUCLID:56;
A10:
|.p2.| <> 0
by A6, TOPRNS_1:25;
then A11:
|.p2.| ^2 > 0
by SQUARE_1:74;
A12:
((p2 `1 ) / |.p2.|) - cn >= 0
by A6, XREAL_1:50;
A13:
((p2 `1 ) / |.p2.|) - cn >= 0
by A6, XREAL_1:50;
A14:
(((p2 `1 ) / |.p2.|) - cn) / (1 - cn) >= 0
by A3, A12;
A15:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by XREAL_1:9;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by A15, XREAL_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A11, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p2 `1 ) / |.p2.|
by SQUARE_1:121;
then A16:
1
- cn >= ((p2 `1 ) / |.p2.|) - cn
by XREAL_1:11;
A17:
- (1 - cn) <= - 0
by A3;
- (1 - cn) <= - (((p2 `1 ) / |.p2.|) - cn)
by A16, XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A3, XREAL_1:74;
then A18:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A3, XCMPLX_1:198;
- (- (1 - cn)) >= - (((p2 `1 ) / |.p2.|) - cn)
by A13, A17, XREAL_1:26;
then
(- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn) <= 1
by A3, XREAL_1:187;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A18, SQUARE_1:119;
then A19:
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then A20:
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))) ^2 ) >= 0
by XCMPLX_1:188;
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 )) >= 0
by A19, SQUARE_1:def 4;
then
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) ^2 ) / ((1 - cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) ^2 ) / ((1 - cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))) <= 0
;
then
p1 `2 = 0
by A2, A4, A5, A7, A8;
then
- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))) = - 0
by A9, A10, XCMPLX_1:6;
then
1
- (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ) = 0
by A20, SQUARE_1:92;
then
1
= (((p2 `1 ) / |.p2.|) - cn) / (1 - cn)
by A14, SQUARE_1:83, SQUARE_1:89;
then
1
* (1 - cn) = ((p2 `1 ) / |.p2.|) - cn
by A3, XCMPLX_1:88;
then
1
* |.p2.| = p2 `1
by A6, TOPRNS_1:25, XCMPLX_1:88;
then
p2 `2 = 0
by A15, XCMPLX_1:6;
hence
x1 = x2
by A2, A5, Th120;
:: thesis: verum end; suppose A21:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| < cn &
p2 `2 <= 0 )
;
:: thesis: x1 = x2then A22:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, Th122;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|;
A23:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))) &
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) )
by EUCLID:56;
A24:
(
p1 `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))) &
p1 `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) )
by A2, A5, A22, EUCLID:56;
A25:
|.p2.| <> 0
by A21, TOPRNS_1:25;
then A26:
|.p2.| ^2 > 0
by SQUARE_1:74;
A27:
1
+ cn > 0
by A1, XREAL_1:150;
A28:
((p2 `1 ) / |.p2.|) - cn <= 0
by A21, XREAL_1:49;
then A29:
- (((p2 `1 ) / |.p2.|) - cn) >= - 0
;
- (- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) <= 0
by A27, A28;
then A30:
- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) >= 0
;
A31:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by XREAL_1:9;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by A31, XREAL_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A26, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then A32:
(- ((p2 `1 ) / |.p2.|)) ^2 <= 1
;
(- (1 + cn)) / (1 + cn) <= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by A27, A29, XREAL_1:74;
then A33:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by A27, XCMPLX_1:198;
1
>= - ((p2 `1 ) / |.p2.|)
by A32, SQUARE_1:121;
then
1
+ cn >= (- ((p2 `1 ) / |.p2.|)) + cn
by XREAL_1:9;
then
(- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn) <= 1
by A27, XREAL_1:187;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A33, SQUARE_1:119;
then A34:
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A35:
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 )) >= 0
by A34, SQUARE_1:def 4;
then
sqrt (1 - (((- (((p2 `1 ) / |.p2.|) - cn)) ^2 ) / ((1 + cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) ^2 ) / ((1 + cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))) <= 0
;
then
p1 `2 = 0
by A2, A4, A5, A22, A23;
then
- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))) = - 0
by A24, A25, XCMPLX_1:6;
then
1
- (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ) = 0
by A35, SQUARE_1:92;
then
1
= (- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) ^2
;
then
1
= - ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))
by A30, SQUARE_1:83, SQUARE_1:89;
then
1
= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by XCMPLX_1:188;
then
1
* (1 + cn) = - (((p2 `1 ) / |.p2.|) - cn)
by A27, XCMPLX_1:88;
then
(1 + cn) - cn = - ((p2 `1 ) / |.p2.|)
;
then
1
= (- (p2 `1 )) / |.p2.|
by XCMPLX_1:188;
then
1
* |.p2.| = - (p2 `1 )
by A21, TOPRNS_1:25, XCMPLX_1:88;
then
((p2 `1 ) ^2 ) - ((p2 `1 ) ^2 ) = (p2 `2 ) ^2
by A31, XCMPLX_1:26;
then
p2 `2 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A2, A5, Th120;
:: thesis: verum end; end; suppose A36:
(
(p1 `1 ) / |.p1.| >= cn &
p1 `2 <= 0 &
p1 <> 0. (TOP-REAL 2) )
;
:: thesis: x1 = x2then A37:
(cn -FanMorphS ) . p1 = |[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, Th122;
set q4 =
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|;
A38:
(
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))) &
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) )
by EUCLID:56;
|.p1.| <> 0
by A36, TOPRNS_1:25;
then A39:
|.p1.| ^2 > 0
by SQUARE_1:74;
per cases
( p2 `2 >= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| < cn & p2 `2 <= 0 ) )
by JGRAPH_2:11;
suppose A40:
p2 `2 >= 0
;
:: thesis: x1 = x2then A41:
(cn -FanMorphS ) . p2 = p2
by Th120;
then A42:
(
p2 `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))) &
p2 `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) )
by A2, A37, EUCLID:56;
A43:
|.p1.| <> 0
by A36, TOPRNS_1:25;
then A44:
|.p1.| ^2 > 0
by SQUARE_1:74;
A45:
1
- cn > 0
by A1, XREAL_1:151;
A46:
((p1 `1 ) / |.p1.|) - cn >= 0
by A36, XREAL_1:50;
A47:
((p1 `1 ) / |.p1.|) - cn >= 0
by A36, XREAL_1:50;
A48:
(((p1 `1 ) / |.p1.|) - cn) / (1 - cn) >= 0
by A45, A46;
A49:
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by A49, XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A44, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p1 `1 ) / |.p1.|
by SQUARE_1:121;
then A50:
1
- cn >= ((p1 `1 ) / |.p1.|) - cn
by XREAL_1:11;
A51:
- (1 - cn) <= - 0
by A45;
- (1 - cn) <= - (((p1 `1 ) / |.p1.|) - cn)
by A50, XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A45, XREAL_1:74;
then A52:
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A45, XCMPLX_1:198;
- (- (1 - cn)) >= - (((p1 `1 ) / |.p1.|) - cn)
by A47, A51, XREAL_1:26;
then
(- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn) <= 1
by A45, XREAL_1:187;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A52, SQUARE_1:119;
then A53:
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then A54:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))) ^2 ) >= 0
by XCMPLX_1:188;
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 )) >= 0
by A53, SQUARE_1:def 4;
then
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) ^2 ) / ((1 - cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) ^2 ) / ((1 - cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))) <= 0
;
then
p2 `2 = 0
by A2, A37, A38, A40, A41;
then
- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))) = - 0
by A42, A43, XCMPLX_1:6;
then
1
- (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ) = 0
by A54, SQUARE_1:92;
then
1
= (((p1 `1 ) / |.p1.|) - cn) / (1 - cn)
by A48, SQUARE_1:83, SQUARE_1:89;
then
1
* (1 - cn) = ((p1 `1 ) / |.p1.|) - cn
by A45, XCMPLX_1:88;
then
1
* |.p1.| = p1 `1
by A36, TOPRNS_1:25, XCMPLX_1:88;
then
p1 `2 = 0
by A49, XCMPLX_1:6;
hence
x1 = x2
by A2, A41, Th120;
:: thesis: verum end; suppose A55:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| >= cn &
p2 `2 <= 0 )
;
:: thesis: x1 = x2then A56:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, Th122;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|;
A57:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))) &
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) )
by EUCLID:56;
A58:
(
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))) &
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) )
by EUCLID:56;
A59:
((p1 `1 ) / |.p1.|) - cn >= 0
by A36, XREAL_1:50;
A60:
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by A60, XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A39, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p1 `1 ) / |.p1.|
by SQUARE_1:121;
then A61:
1
- cn >= ((p1 `1 ) / |.p1.|) - cn
by XREAL_1:11;
A62:
- (1 - cn) <= - 0
by A3;
- (1 - cn) <= - (((p1 `1 ) / |.p1.|) - cn)
by A61, XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A3, XREAL_1:74;
then A63:
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)
by A3, XCMPLX_1:198;
- (- (1 - cn)) >= - (((p1 `1 ) / |.p1.|) - cn)
by A59, A62, XREAL_1:26;
then
(- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn) <= 1
by A3, XREAL_1:187;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A63, SQUARE_1:119;
then
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then A64:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))) ^2 ) >= 0
by XCMPLX_1:188;
A65:
(|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 =
(|.p1.| ^2 ) * ((sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))) ^2 )
by A58
.=
(|.p1.| ^2 ) * (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 ))
by A64, SQUARE_1:def 4
;
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 =
((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p1.| ^2
by A58, A65
;
then A66:
sqrt (|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 ) = |.p1.|
by SQUARE_1:89;
then A67:
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 - cn)) ^2 )))))]|.| = |.p1.|
by SQUARE_1:89;
|.p2.| <> 0
by A55, TOPRNS_1:25;
then A68:
|.p2.| ^2 > 0
by SQUARE_1:74;
A69:
((p2 `1 ) / |.p2.|) - cn >= 0
by A55, XREAL_1:50;
A70:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by XREAL_1:9;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by A70, XREAL_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A68, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
1
>= (p2 `1 ) / |.p2.|
by SQUARE_1:121;
then A71:
1
- cn >= ((p2 `1 ) / |.p2.|) - cn
by XREAL_1:11;
A72:
- (1 - cn) <= - 0
by A3;
- (1 - cn) <= - (((p2 `1 ) / |.p2.|) - cn)
by A71, XREAL_1:26;
then
(- (1 - cn)) / (1 - cn) <= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A3, XREAL_1:74;
then A73:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)
by A3, XCMPLX_1:198;
- (- (1 - cn)) >= - (((p2 `1 ) / |.p2.|) - cn)
by A69, A72, XREAL_1:26;
then
(- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn) <= 1
by A3, XREAL_1:187;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 <= 1
^2
by A73, SQUARE_1:119;
then
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 - cn)) ^2 ) >= 0
by XREAL_1:50;
then A74:
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))) ^2 ) >= 0
by XCMPLX_1:188;
A75:
(|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 =
(|.p2.| ^2 ) * ((sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))) ^2 )
by A57
.=
(|.p2.| ^2 ) * (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 ))
by A74, SQUARE_1:def 4
;
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 =
((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p2.| ^2
by A57, A75
;
then A76:
sqrt (|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|.| ^2 ) = |.p2.|
by SQUARE_1:89;
then A77:
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|.| = |.p2.|
by SQUARE_1:89;
(((p2 `1 ) / |.p2.|) - cn) / (1 - cn) = (|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 - cn))) / |.p2.|
by A2, A37, A38, A55, A56, A57, TOPRNS_1:25, XCMPLX_1:90;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 - cn) = (((p1 `1 ) / |.p1.|) - cn) / (1 - cn)
by A2, A37, A55, A56, A66, A76, TOPRNS_1:25, XCMPLX_1:90;
then
((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) * (1 - cn) = ((p1 `1 ) / |.p1.|) - cn
by A3, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) - cn = ((p1 `1 ) / |.p1.|) - cn
by A3, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) * |.p2.| = p1 `1
by A2, A37, A55, A56, A67, A77, TOPRNS_1:25, XCMPLX_1:88;
then A78:
p2 `1 = p1 `1
by A55, TOPRNS_1:25, XCMPLX_1:88;
A79:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
then A80:
(- (p2 `2 )) ^2 = (p1 `2 ) ^2
by A2, A37, A56, A67, A77, A78, A79;
- (- (p1 `2 )) <= 0
by A36;
then A81:
- (p1 `2 ) >= 0
;
- (- (p2 `2 )) <= 0
by A55;
then
- (p2 `2 ) >= 0
;
then
- (p2 `2 ) = sqrt ((- (p1 `2 )) ^2 )
by A80, SQUARE_1:89;
then A82:
- (- (p2 `2 )) = - (- (p1 `2 ))
by A81, SQUARE_1:89;
p2 = |[(p2 `1 ),(p2 `2 )]|
by EUCLID:57;
hence
x1 = x2
by A78, A82, EUCLID:57;
:: thesis: verum end; suppose A83:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| < cn &
p2 `2 <= 0 )
;
:: thesis: x1 = x2then A84:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, Th122;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|;
A85:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))) &
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) )
by EUCLID:56;
A86:
((p2 `1 ) / |.p2.|) - cn < 0
by A83, XREAL_1:51;
1
+ cn > 0
by A1, XREAL_1:150;
then A87:
(((p2 `1 ) / |.p2.|) - cn) / (1 + cn) < 0
by A86, XREAL_1:143;
|.p2.| <> 0
by A83, TOPRNS_1:25;
then A89:
|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) < 0
by A87, XREAL_1:134;
A90:
((p1 `1 ) / |.p1.|) - cn >= 0
by A36, XREAL_1:50;
1
- cn > 0
by A1, XREAL_1:151;
then
(((p1 `1 ) / |.p1.|) - cn) / (1 - cn) >= 0
by A90;
hence
x1 = x2
by A2, A37, A38, A84, A85, A89;
:: thesis: verum end; end; suppose A91:
(
(p1 `1 ) / |.p1.| < cn &
p1 `2 <= 0 &
p1 <> 0. (TOP-REAL 2) )
;
:: thesis: x1 = x2then A92:
(cn -FanMorphS ) . p1 = |[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, Th122;
set q4 =
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|;
A93:
(
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))) &
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) )
by EUCLID:56;
A94:
|.p1.| <> 0
by A91, TOPRNS_1:25;
then A95:
|.p1.| ^2 > 0
by SQUARE_1:74;
per cases
( p2 `2 >= 0 or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 ) or ( p2 <> 0. (TOP-REAL 2) & (p2 `1 ) / |.p2.| < cn & p2 `2 <= 0 ) )
by JGRAPH_2:11;
suppose A96:
p2 `2 >= 0
;
:: thesis: x1 = x2then A97:
(cn -FanMorphS ) . p2 = p2
by Th120;
then A98:
(
p2 `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))) &
p2 `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) )
by A2, A92, EUCLID:56;
A99:
1
+ cn > 0
by A1, XREAL_1:150;
A100:
((p1 `1 ) / |.p1.|) - cn <= 0
by A91, XREAL_1:49;
then A101:
- (((p1 `1 ) / |.p1.|) - cn) >= - 0
;
- (- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) <= 0
by A99, A100;
then A102:
- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) >= 0
;
A103:
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by A103, XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A95, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then A104:
(- ((p1 `1 ) / |.p1.|)) ^2 <= 1
;
(- (1 + cn)) / (1 + cn) <= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by A99, A101, XREAL_1:74;
then A105:
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by A99, XCMPLX_1:198;
1
>= - ((p1 `1 ) / |.p1.|)
by A104, SQUARE_1:121;
then
1
+ cn >= (- ((p1 `1 ) / |.p1.|)) + cn
by XREAL_1:9;
then
(- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn) <= 1
by A99, XREAL_1:187;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A105, SQUARE_1:119;
then A106:
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A107:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 )) >= 0
by A106, SQUARE_1:def 4;
then
sqrt (1 - (((- (((p1 `1 ) / |.p1.|) - cn)) ^2 ) / ((1 + cn) ^2 ))) >= 0
by XCMPLX_1:77;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) ^2 ) / ((1 + cn) ^2 ))) >= 0
;
then
sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )) >= 0
by XCMPLX_1:77;
then
- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))) <= 0
;
then
p2 `2 = 0
by A2, A92, A93, A96, A97;
then
- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))) = - 0
by A94, A98, XCMPLX_1:6;
then
1
- (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ) = 0
by A107, SQUARE_1:92;
then
1
= (- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) ^2
;
then
1
= - ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))
by A102, SQUARE_1:83, SQUARE_1:89;
then
1
= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by XCMPLX_1:188;
then
1
* (1 + cn) = - (((p1 `1 ) / |.p1.|) - cn)
by A99, XCMPLX_1:88;
then
(1 + cn) - cn = - ((p1 `1 ) / |.p1.|)
;
then
1
= (- (p1 `1 )) / |.p1.|
by XCMPLX_1:188;
then
1
* |.p1.| = - (p1 `1 )
by A91, TOPRNS_1:25, XCMPLX_1:88;
then
((p1 `1 ) ^2 ) - ((p1 `1 ) ^2 ) = (p1 `2 ) ^2
by A103, XCMPLX_1:26;
then
p1 `2 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A2, A97, Th120;
:: thesis: verum end; suppose A108:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| >= cn &
p2 `2 <= 0 )
;
:: thesis: x1 = x2then A109:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|
by A1, Th122;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]|;
A110:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))) &
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 - cn)) )
by EUCLID:56;
A111:
((p1 `1 ) / |.p1.|) - cn < 0
by A91, XREAL_1:51;
1
+ cn > 0
by A1, XREAL_1:150;
then A112:
(((p1 `1 ) / |.p1.|) - cn) / (1 + cn) < 0
by A111, XREAL_1:143;
|.p1.| <> 0
by A91, TOPRNS_1:25;
then A114:
|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) < 0
by A112, XREAL_1:134;
A115:
((p2 `1 ) / |.p2.|) - cn >= 0
by A108, XREAL_1:50;
1
- cn > 0
by A1, XREAL_1:151;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 - cn) >= 0
by A115;
hence
x1 = x2
by A2, A92, A93, A109, A110, A114;
:: thesis: verum end; suppose A116:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `1 ) / |.p2.| < cn &
p2 `2 <= 0 )
;
:: thesis: x1 = x2then A117:
(cn -FanMorphS ) . p2 = |[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|
by A1, Th122;
set p4 =
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|;
A118:
(
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))) &
|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) )
by EUCLID:56;
A119:
(
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 = |.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))) &
|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `1 = |.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) )
by EUCLID:56;
((p1 `1 ) / |.p1.|) - cn <= 0
by A91, XREAL_1:49;
then A120:
- (((p1 `1 ) / |.p1.|) - cn) >= - 0
;
A121:
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p1 `2 ) ^2
by XREAL_1:65;
then
0 + ((p1 `1 ) ^2 ) <= ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by XREAL_1:9;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= (|.p1.| ^2 ) / (|.p1.| ^2 )
by A121, XREAL_1:74;
then
((p1 `1 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A95, XCMPLX_1:60;
then
((p1 `1 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (p1 `1 ) / |.p1.|
by SQUARE_1:121;
then A122:
(- 1) - cn <= ((p1 `1 ) / |.p1.|) - cn
by XREAL_1:11;
A123:
1
+ cn > 0
by A1, XREAL_1:150;
(- (1 + cn)) / (1 + cn) <= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by A120, A123, XREAL_1:74;
then A124:
- 1
<= (- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)
by A123, XCMPLX_1:198;
- ((- 1) - cn) >= - (((p1 `1 ) / |.p1.|) - cn)
by A122, XREAL_1:26;
then
(- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn) <= 1
by A123, XREAL_1:187;
then
((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A124, SQUARE_1:119;
then
1
- (((- (((p1 `1 ) / |.p1.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A125:
1
- ((- ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
A126:
(|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 =
(|.p1.| ^2 ) * ((sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))) ^2 )
by A119
.=
(|.p1.| ^2 ) * (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 ))
by A125, SQUARE_1:def 4
;
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 =
((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p1.| ^2
by A119, A126
;
then A127:
sqrt (|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 ) = |.p1.|
by SQUARE_1:89;
then A128:
|.|[(|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))),(|.p1.| * (- (sqrt (1 - (((((p1 `1 ) / |.p1.|) - cn) / (1 + cn)) ^2 )))))]|.| = |.p1.|
by SQUARE_1:89;
|.p2.| <> 0
by A116, TOPRNS_1:25;
then A129:
|.p2.| ^2 > 0
by SQUARE_1:74;
((p2 `1 ) / |.p2.|) - cn <= 0
by A116, XREAL_1:49;
then A130:
- (((p2 `1 ) / |.p2.|) - cn) >= - 0
;
A131:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
0 <= (p2 `2 ) ^2
by XREAL_1:65;
then
0 + ((p2 `1 ) ^2 ) <= ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by XREAL_1:9;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= (|.p2.| ^2 ) / (|.p2.| ^2 )
by A131, XREAL_1:74;
then
((p2 `1 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A129, XCMPLX_1:60;
then
((p2 `1 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (p2 `1 ) / |.p2.|
by SQUARE_1:121;
then A132:
(- 1) - cn <= ((p2 `1 ) / |.p2.|) - cn
by XREAL_1:11;
(- (1 + cn)) / (1 + cn) <= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by A123, A130, XREAL_1:74;
then A133:
- 1
<= (- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)
by A123, XCMPLX_1:198;
- ((- 1) - cn) >= - (((p2 `1 ) / |.p2.|) - cn)
by A132, XREAL_1:26;
then
(- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn) <= 1
by A123, XREAL_1:187;
then
((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 <= 1
^2
by A133, SQUARE_1:119;
then
1
- (((- (((p2 `1 ) / |.p2.|) - cn)) / (1 + cn)) ^2 ) >= 0
by XREAL_1:50;
then A134:
1
- ((- ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))) ^2 ) >= 0
by XCMPLX_1:188;
A135:
(|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 =
(|.p2.| ^2 ) * ((sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))) ^2 )
by A118
.=
(|.p2.| ^2 ) * (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 ))
by A134, SQUARE_1:def 4
;
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 =
((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `1 ) ^2 ) + ((|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]| `2 ) ^2 )
by JGRAPH_3:10
.=
|.p2.| ^2
by A118, A135
;
then A136:
sqrt (|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|.| ^2 ) = |.p2.|
by SQUARE_1:89;
then A137:
|.|[(|.p2.| * ((((p2 `1 ) / |.p2.|) - cn) / (1 + cn))),(|.p2.| * (- (sqrt (1 - (((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) ^2 )))))]|.| = |.p2.|
by SQUARE_1:89;
(((p2 `1 ) / |.p2.|) - cn) / (1 + cn) = (|.p1.| * ((((p1 `1 ) / |.p1.|) - cn) / (1 + cn))) / |.p2.|
by A2, A92, A93, A116, A117, A118, TOPRNS_1:25, XCMPLX_1:90;
then
(((p2 `1 ) / |.p2.|) - cn) / (1 + cn) = (((p1 `1 ) / |.p1.|) - cn) / (1 + cn)
by A2, A92, A116, A117, A127, A136, TOPRNS_1:25, XCMPLX_1:90;
then
((((p2 `1 ) / |.p2.|) - cn) / (1 + cn)) * (1 + cn) = ((p1 `1 ) / |.p1.|) - cn
by A123, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) - cn = ((p1 `1 ) / |.p1.|) - cn
by A123, XCMPLX_1:88;
then
((p2 `1 ) / |.p2.|) * |.p2.| = p1 `1
by A2, A92, A116, A117, A128, A137, TOPRNS_1:25, XCMPLX_1:88;
then A138:
p2 `1 = p1 `1
by A116, TOPRNS_1:25, XCMPLX_1:88;
A139:
|.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 )
by JGRAPH_3:10;
|.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 )
by JGRAPH_3:10;
then A140:
(- (p2 `2 )) ^2 = (p1 `2 ) ^2
by A2, A92, A117, A128, A137, A138, A139;
- (- (p1 `2 )) <= 0
by A91;
then A141:
- (p1 `2 ) >= 0
;
- (- (p2 `2 )) <= 0
by A116;
then
- (p2 `2 ) >= 0
;
then
- (p2 `2 ) = sqrt ((- (p1 `2 )) ^2 )
by A140, SQUARE_1:89;
then A142:
- (- (p2 `2 )) = - (- (p1 `2 ))
by A141, SQUARE_1:89;
p2 = |[(p2 `1 ),(p2 `2 )]|
by EUCLID:57;
hence
x1 = x2
by A138, A142, EUCLID:57;
:: thesis: verum end; end;
end;
hence
cn -FanMorphS is one-to-one
by FUNCT_1:def 8; :: thesis: verum