let sn be Real; :: thesis: ( - 1 < sn & sn < 1 implies sn -FanMorphE is one-to-one )
assume A1:
( - 1 < sn & sn < 1 )
; :: thesis: sn -FanMorphE is one-to-one
for x1, x2 being set st x1 in dom (sn -FanMorphE ) & x2 in dom (sn -FanMorphE ) & (sn -FanMorphE ) . x1 = (sn -FanMorphE ) . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom (sn -FanMorphE ) & x2 in dom (sn -FanMorphE ) & (sn -FanMorphE ) . x1 = (sn -FanMorphE ) . x2 implies x1 = x2 )
assume A2:
(
x1 in dom (sn -FanMorphE ) &
x2 in dom (sn -FanMorphE ) &
(sn -FanMorphE ) . x1 = (sn -FanMorphE ) . 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 -FanMorphE ) . p1 = p1
by Th89;
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 -FanMorphE ) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)))]|
by A1, Th91;
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, TOPRNS_1:25;
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
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 A6, TOPRNS_1:25, XCMPLX_1:88;
then
p2 `1 = 0
by A14, XCMPLX_1:6;
hence
x1 = x2
by A2, A5, Th89;
:: thesis: verum end; case A20:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `2 ) / |.p2.| < sn &
p2 `1 >= 0 )
;
:: thesis: x1 = x2then A21:
(sn -FanMorphE ) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)))]|
by A1, Th91;
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, TOPRNS_1:25;
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
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 A20, TOPRNS_1:25, 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, Th89;
:: 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 -FanMorphE ) . p1 = |[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)))]|
by A1, Th91;
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, TOPRNS_1:25;
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 -FanMorphE ) . p2 = p2
by Th89;
A40:
|.p1.| <> 0
by A34, TOPRNS_1:25;
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
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 A34, TOPRNS_1:25, XCMPLX_1:88;
then
p1 `1 = 0
by A46, XCMPLX_1:6;
hence
x1 = x2
by A2, A39, Th89;
:: thesis: verum end; case A52:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `2 ) / |.p2.| >= sn &
p2 `1 >= 0 )
;
:: thesis: x1 = x2then A53:
(sn -FanMorphE ) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)))]|
by A1, Th91;
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 A63:
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 A64:
|.|[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 - sn)))]|.| = |.p1.|
by SQUARE_1:89;
|.p2.| <> 0
by A52, TOPRNS_1:25;
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 A73:
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 A74:
|.|[(|.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, A52, A53, A54, TOPRNS_1:25, XCMPLX_1:90;
then
(((p2 `2 ) / |.p2.|) - sn) / (1 - sn) = (((p1 `2 ) / |.p1.|) - sn) / (1 - sn)
by A2, A35, A52, A53, A63, A73, TOPRNS_1:25, 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, A52, A53, A64, A74, TOPRNS_1:25, XCMPLX_1:88;
then A75:
p2 `2 = p1 `2
by A52, TOPRNS_1:25, XCMPLX_1:88;
A76:
|.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
p2 `1 = sqrt ((p1 `1 ) ^2 )
by A2, A35, A52, A53, A64, A74, A75, A76, SQUARE_1:89;
then A77:
p2 `1 = p1 `1
by A34, SQUARE_1:89;
p2 = |[(p2 `1 ),(p2 `2 )]|
by EUCLID:57;
hence
x1 = x2
by A75, A77, EUCLID:57;
:: thesis: verum end; case A78:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `2 ) / |.p2.| < sn &
p2 `1 >= 0 )
;
:: thesis: x1 = x2then A79:
(sn -FanMorphE ) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)))]|
by A1, Th91;
set p4 =
|[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)))]|;
A80:
(
|[(|.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;
A81:
((p2 `2 ) / |.p2.|) - sn < 0
by A78, XREAL_1:51;
1
+ sn > 0
by A1, XREAL_1:150;
then A82:
(((p2 `2 ) / |.p2.|) - sn) / (1 + sn) < 0
by A81, XREAL_1:143;
|.p2.| <> 0
by A78, TOPRNS_1:25;
then A84:
|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) < 0
by A82, XREAL_1:134;
A85:
((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 A85;
hence
x1 = x2
by A2, A35, A36, A79, A80, A84;
:: thesis: verum end; hence
x1 = x2
;
:: thesis: verum end; case A86:
(
(p1 `2 ) / |.p1.| < sn &
p1 `1 >= 0 &
p1 <> 0. (TOP-REAL 2) )
;
:: thesis: x1 = x2then A87:
(sn -FanMorphE ) . p1 = |[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)))]|
by A1, Th91;
set q4 =
|[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)))]|;
A88:
(
|[(|.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;
A89:
|.p1.| <> 0
by A86, TOPRNS_1:25;
then A90:
|.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 A91:
p2 `1 <= 0
;
:: thesis: x1 = x2then A92:
(sn -FanMorphE ) . p2 = p2
by Th89;
A93:
1
+ sn > 0
by A1, XREAL_1:150;
A94:
((p1 `2 ) / |.p1.|) - sn <= 0
by A86, XREAL_1:49;
then A95:
- (((p1 `2 ) / |.p1.|) - sn) >= - 0
;
- (- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) <= 0
by A93, A94;
then A96:
- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) >= 0
;
A97:
|.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 A97, XREAL_1:74;
then
((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A90, XCMPLX_1:60;
then
((p1 `2 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then A98:
(- ((p1 `2 ) / |.p1.|)) ^2 <= 1
;
(- (1 + sn)) / (1 + sn) <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)
by A93, A95, XREAL_1:74;
then A99:
- 1
<= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)
by A93, XCMPLX_1:198;
1
>= - ((p1 `2 ) / |.p1.|)
by A98, SQUARE_1:121;
then
1
+ sn >= (- ((p1 `2 ) / |.p1.|)) + sn
by XREAL_1:9;
then
(- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) <= 1
by A93, XREAL_1:187;
then
((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1
^2
by A99, SQUARE_1:119;
then A100:
1
- (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 ) >= 0
by XREAL_1:50;
then A101:
1
- ((- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) ^2 ) >= 0
by XCMPLX_1:188;
sqrt (1 - (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 )) >= 0
by A100, 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
p2 `1 = 0
by A2, A87, A88, A91, A92;
then
sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 )) = 0
by A2, A87, A88, A89, A92, XCMPLX_1:6;
then
1
- (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 ) = 0
by A101, 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 A96, SQUARE_1:89;
then
1
= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)
by XCMPLX_1:188;
then
1
* (1 + sn) = - (((p1 `2 ) / |.p1.|) - sn)
by A93, 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 A86, TOPRNS_1:25, XCMPLX_1:88;
then
((p1 `2 ) ^2 ) - ((p1 `2 ) ^2 ) = (p1 `1 ) ^2
by A97, XCMPLX_1:26;
then
p1 `1 = 0
by XCMPLX_1:6;
hence
x1 = x2
by A2, A92, Th89;
:: thesis: verum end; case A102:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `2 ) / |.p2.| >= sn &
p2 `1 >= 0 )
;
:: thesis: x1 = x2then A103:
(sn -FanMorphE ) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)))]|
by A1, Th91;
set p4 =
|[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 - sn)))]|;
A104:
(
|[(|.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;
A105:
((p1 `2 ) / |.p1.|) - sn < 0
by A86, XREAL_1:51;
1
+ sn > 0
by A1, XREAL_1:150;
then A106:
(((p1 `2 ) / |.p1.|) - sn) / (1 + sn) < 0
by A105, XREAL_1:143;
|.p1.| <> 0
by A86, TOPRNS_1:25;
then A108:
|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) < 0
by A106, XREAL_1:134;
A109:
((p2 `2 ) / |.p2.|) - sn >= 0
by A102, XREAL_1:50;
1
- sn > 0
by A1, XREAL_1:151;
then
(((p2 `2 ) / |.p2.|) - sn) / (1 - sn) >= 0
by A109;
hence
x1 = x2
by A2, A87, A88, A103, A104, A108;
:: thesis: verum end; case A110:
(
p2 <> 0. (TOP-REAL 2) &
(p2 `2 ) / |.p2.| < sn &
p2 `1 >= 0 )
;
:: thesis: x1 = x2then A111:
(sn -FanMorphE ) . p2 = |[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)))]|
by A1, Th91;
set p4 =
|[(|.p2.| * (sqrt (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 )))),(|.p2.| * ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)))]|;
A112:
(
|[(|.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;
A113:
(
|[(|.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 A86, XREAL_1:49;
then A114:
- (((p1 `2 ) / |.p1.|) - sn) >= - 0
;
A115:
|.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 A115, XREAL_1:74;
then
((p1 `2 ) ^2 ) / (|.p1.| ^2 ) <= 1
by A90, XCMPLX_1:60;
then
((p1 `2 ) / |.p1.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (p1 `2 ) / |.p1.|
by SQUARE_1:121;
then A116:
(- 1) - sn <= ((p1 `2 ) / |.p1.|) - sn
by XREAL_1:11;
A117:
1
+ sn > 0
by A1, XREAL_1:150;
(- (1 + sn)) / (1 + sn) <= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)
by A114, A117, XREAL_1:74;
then A118:
- 1
<= (- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)
by A117, XCMPLX_1:198;
- ((- 1) - sn) >= - (((p1 `2 ) / |.p1.|) - sn)
by A116, XREAL_1:26;
then
(- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn) <= 1
by A117, XREAL_1:187;
then
((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 <= 1
^2
by A118, SQUARE_1:119;
then
1
- (((- (((p1 `2 ) / |.p1.|) - sn)) / (1 + sn)) ^2 ) >= 0
by XREAL_1:50;
then A119:
1
- ((- ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn))) ^2 ) >= 0
by XCMPLX_1:188;
A120:
(|[(|.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 A113
.=
(|.p1.| ^2 ) * (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 ))
by A119, 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 A113, A120
;
then A121:
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 A122:
|.|[(|.p1.| * (sqrt (1 - (((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)) ^2 )))),(|.p1.| * ((((p1 `2 ) / |.p1.|) - sn) / (1 + sn)))]|.| = |.p1.|
by SQUARE_1:89;
|.p2.| <> 0
by A110, TOPRNS_1:25;
then A123:
|.p2.| ^2 > 0
by SQUARE_1:74;
((p2 `2 ) / |.p2.|) - sn <= 0
by A110, XREAL_1:49;
then A124:
- (((p2 `2 ) / |.p2.|) - sn) >= - 0
;
A125:
|.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 A125, XREAL_1:74;
then
((p2 `2 ) ^2 ) / (|.p2.| ^2 ) <= 1
by A123, XCMPLX_1:60;
then
((p2 `2 ) / |.p2.|) ^2 <= 1
by XCMPLX_1:77;
then
- 1
<= (p2 `2 ) / |.p2.|
by SQUARE_1:121;
then A126:
(- 1) - sn <= ((p2 `2 ) / |.p2.|) - sn
by XREAL_1:11;
(- (1 + sn)) / (1 + sn) <= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)
by A117, A124, XREAL_1:74;
then A127:
- 1
<= (- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)
by A117, XCMPLX_1:198;
- ((- 1) - sn) >= - (((p2 `2 ) / |.p2.|) - sn)
by A126, XREAL_1:26;
then
(- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn) <= 1
by A117, XREAL_1:187;
then
((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 <= 1
^2
by A127, SQUARE_1:119;
then
1
- (((- (((p2 `2 ) / |.p2.|) - sn)) / (1 + sn)) ^2 ) >= 0
by XREAL_1:50;
then A128:
1
- ((- ((((p2 `2 ) / |.p2.|) - sn) / (1 + sn))) ^2 ) >= 0
by XCMPLX_1:188;
A129:
(|[(|.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 A112
.=
(|.p2.| ^2 ) * (1 - (((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) ^2 ))
by A128, 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 A112, A129
;
then A130:
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 A131:
|.|[(|.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, A87, A88, A110, A111, A112, TOPRNS_1:25, XCMPLX_1:90;
then
(((p2 `2 ) / |.p2.|) - sn) / (1 + sn) = (((p1 `2 ) / |.p1.|) - sn) / (1 + sn)
by A2, A87, A110, A111, A121, A130, TOPRNS_1:25, XCMPLX_1:90;
then
((((p2 `2 ) / |.p2.|) - sn) / (1 + sn)) * (1 + sn) = ((p1 `2 ) / |.p1.|) - sn
by A117, XCMPLX_1:88;
then
((p2 `2 ) / |.p2.|) - sn = ((p1 `2 ) / |.p1.|) - sn
by A117, XCMPLX_1:88;
then
((p2 `2 ) / |.p2.|) * |.p2.| = p1 `2
by A2, A87, A110, A111, A122, A131, TOPRNS_1:25, XCMPLX_1:88;
then A132:
p2 `2 = p1 `2
by A110, TOPRNS_1:25, XCMPLX_1:88;
A133:
|.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
p2 `1 = sqrt ((p1 `1 ) ^2 )
by A2, A87, A110, A111, A122, A131, A132, A133, SQUARE_1:89;
then A134:
p2 `1 = p1 `1
by A86, SQUARE_1:89;
p2 = |[(p2 `1 ),(p2 `2 )]|
by EUCLID:57;
hence
x1 = x2
by A132, A134, EUCLID:57;
:: thesis: verum end; hence
x1 = x2
;
:: thesis: verum end;
hence
x1 = x2
;
:: thesis: verum
end;
hence
sn -FanMorphE is one-to-one
by FUNCT_1:def 8; :: thesis: verum