let cn be Real; for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 < 0 & (q `1) / |.q.| > cn holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 > 0 )
let q be Point of (TOP-REAL 2); ( - 1 < cn & cn < 1 & q `2 < 0 & (q `1) / |.q.| > cn implies for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 > 0 ) )
assume that
A1:
- 1 < cn
and
A2:
cn < 1
and
A3:
q `2 < 0
and
A4:
(q `1) / |.q.| > cn
; for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 > 0 )
let p be Point of (TOP-REAL 2); ( p = (cn -FanMorphS) . q implies ( p `2 < 0 & p `1 > 0 ) )
assume A5:
p = (cn -FanMorphS) . q
; ( p `2 < 0 & p `1 > 0 )
now not p `1 = 0 set q1 =
|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|;
set p1 =
(1 / |.p.|) * p;
set p2 =
(cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|);
(
|[0,(- 1)]| `1 = 0 &
|[0,(- 1)]| `2 = - 1 )
by EUCLID:52;
then A6:
|.p.| * |[0,(- 1)]| =
|[(|.p.| * 0),(|.p.| * (- 1))]|
by EUCLID:57
.=
|[0,(- |.p.|)]|
;
A7:
(
|[cn,(- (sqrt (1 - (cn ^2))))]| `1 = cn &
|[cn,(- (sqrt (1 - (cn ^2))))]| `2 = - (sqrt (1 - (cn ^2))) )
by EUCLID:52;
then A8:
|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]| = |[(|.p.| * cn),(|.p.| * (- (sqrt (1 - (cn ^2)))))]|
by EUCLID:57;
then A9:
(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `1 = |.p.| * cn
by EUCLID:52;
assume A10:
p `1 = 0
;
contradictionthen |.p.| ^2 =
((p `2) ^2) + (0 ^2)
by JGRAPH_3:1
.=
(p `2) ^2
;
then A11:
(
p `2 = |.p.| or
p `2 = - |.p.| )
by SQUARE_1:40;
then A12:
|.p.| <> 0
by A2, A3, A4, A5, JGRAPH_4:137;
A13:
(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `2 = - ((sqrt (1 - (cn ^2))) * |.p.|)
by A8, EUCLID:52;
1
^2 > cn ^2
by A1, A2, SQUARE_1:50;
then A14:
1
- (cn ^2) > 0
by XREAL_1:50;
then
sqrt (1 - (cn ^2)) > 0
by SQUARE_1:25;
then
- (- ((sqrt (1 - (cn ^2))) * |.p.|)) > 0
by A12, XREAL_1:129;
then A15:
(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `2 < 0
by A13;
A16:
|.p.| * ((1 / |.p.|) * p) =
(|.p.| * (1 / |.p.|)) * p
by RLVECT_1:def 7
.=
1
* p
by A12, XCMPLX_1:106
.=
p
by RLVECT_1:def 8
;
A17:
(1 / |.p.|) * p = |[((1 / |.p.|) * (p `1)),((1 / |.p.|) * (p `2))]|
by EUCLID:57;
then ((1 / |.p.|) * p) `2 =
- (|.p.| * (1 / |.p.|))
by A2, A3, A4, A5, A11, EUCLID:52, JGRAPH_4:137
.=
- 1
by A12, XCMPLX_1:106
;
then A18:
p = |.p.| * |[0,(- 1)]|
by A10, A16, A17, EUCLID:52;
A19:
|.(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|).| =
|.|.p.|.| * |.|[cn,(- (sqrt (1 - (cn ^2))))]|.|
by TOPRNS_1:7
.=
|.|.p.|.| * (sqrt ((cn ^2) + ((- (sqrt (1 - (cn ^2)))) ^2)))
by A7, JGRAPH_3:1
.=
|.|.p.|.| * (sqrt ((cn ^2) + ((sqrt (1 - (cn ^2))) ^2)))
.=
|.|.p.|.| * (sqrt ((cn ^2) + (1 - (cn ^2))))
by A14, SQUARE_1:def 2
.=
|.p.|
by ABSVALUE:def 1, SQUARE_1:18
;
then A20:
|.((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)).| = |.p.|
by JGRAPH_4:128;
A21:
((|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) `1) / |.(|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|).| = cn
by A12, A9, A19, XCMPLX_1:89;
then A22:
((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)) `1 = 0
by A15, JGRAPH_4:142;
then |.((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)).| ^2 =
((((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)) `2) ^2) + (0 ^2)
by JGRAPH_3:1
.=
(((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)) `2) ^2
;
then
(
((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)) `2 = |.((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)).| or
((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)) `2 = - |.((cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|)).| )
by SQUARE_1:40;
then A23:
(cn -FanMorphS) . (|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]|) = |[0,(- |.p.|)]|
by A15, A21, A22, A20, EUCLID:53, JGRAPH_4:142;
(
cn -FanMorphS is
one-to-one &
dom (cn -FanMorphS) = the
carrier of
(TOP-REAL 2) )
by A1, A2, FUNCT_2:def 1, JGRAPH_4:133;
then
|.p.| * |[cn,(- (sqrt (1 - (cn ^2))))]| = q
by A5, A18, A23, A6, FUNCT_1:def 4;
hence
contradiction
by A4, A12, A9, A19, XCMPLX_1:89;
verum end;
hence
( p `2 < 0 & p `1 > 0 )
by A2, A3, A4, A5, JGRAPH_4:137; verum