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