let n be Nat; :: thesis: for p being Point of ()
for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. ()),1)) \ {p} & p in Sphere ((0. ()),1) holds
stereographic_projection (S,p) is being_homeomorphism

let p be Point of (); :: thesis: for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. ()),1)) \ {p} & p in Sphere ((0. ()),1) holds
stereographic_projection (S,p) is being_homeomorphism

let S be SubSpace of TOP-REAL n; :: thesis: ( [#] S = (Sphere ((0. ()),1)) \ {p} & p in Sphere ((0. ()),1) implies stereographic_projection (S,p) is being_homeomorphism )
assume A1: [#] S = (Sphere ((0. ()),1)) \ {p} ; :: thesis: ( not p in Sphere ((0. ()),1) or stereographic_projection (S,p) is being_homeomorphism )
assume A2: p in Sphere ((0. ()),1) ; :: thesis:
set f = stereographic_projection (S,p);
set T = TPlane (p,(0. ()));
A3: dom () = [#] S by FUNCT_2:def 1;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Point of (TOP-REAL n1) ;
|.(p1 - (0. (TOP-REAL n1))).| = 1 by ;
then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;
then |.(p1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;
then A4: |.p.| = 1 by RLVECT_1:4;
then |(p,p)| = 1 ^2 by EUCLID_2:4;
then A5: |(p,p)| = 1 * 1 by SQUARE_1:def 1;
defpred S1[ object , object ] means for q being Point of () st q = \$1 & q in TPlane (p,(0. ())) holds
\$2 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));
A6: for x being object st x in [#] (TPlane (p,(0. ()))) holds
ex y being object st
( y in [#] S & S1[x,y] )
proof
let x be object ; :: thesis: ( x in [#] (TPlane (p,(0. ()))) implies ex y being object st
( y in [#] S & S1[x,y] ) )

assume A7: x in [#] (TPlane (p,(0. ()))) ; :: thesis: ex y being object st
( y in [#] S & S1[x,y] )

[#] (TPlane (p,(0. ()))) c= [#] () by PRE_TOPC:def 4;
then reconsider q = x as Point of () by A7;
set y = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));
take (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) ; :: thesis: ( (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S & S1[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Point of (TOP-REAL n1) ;
q in Plane (p,(0. ())) by ;
then consider x1 being Point of () such that
A8: ( x1 = q & |(p,(x1 - (0. ())))| = 0 ) ;
|(p,(q + ((- 1) * (0. ()))))| = 0 by ;
then |(p,(q + (0. ())))| = 0 by RLVECT_1:10;
then A9: |(p,q)| = 0 by RLVECT_1:4;
A10: |(q,q)| >= 0 by EUCLID_2:35;
A11: not (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p}
proof
assume A12: (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p} ; :: thesis: contradiction
A13: |(((2 * q) + ((|(q,q)| - 1) * p)),p)| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25
.= (|(q,q)| - 1) * |(p,p)| by A9 ;
|(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),p)| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),p)| by EUCLID_2:19
.= ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) * |(p,p)| by A13 ;
then (|(q,q)| + 1) * 1 = (|(q,q)| + 1) * ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) by
.= ((|(q,q)| + 1) * (1 / (|(q,q)| + 1))) * (|(q,q)| - 1)
.= ((|(q,q)| + 1) / (|(q,q)| + 1)) * (|(q,q)| - 1) by XCMPLX_1:99
.= 1 * (|(q,q)| - 1) by ;
hence contradiction ; :: thesis: verum
end;
reconsider y1 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) as Point of (TOP-REAL n1) ;
A14: |(q,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,q)|) + ((|(q,q)| - 1) * |(p,q)|) by EUCLID_2:25
.= 2 * |(q,q)| by A9 ;
A15: |(p,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25
.= |(q,q)| - 1 by A5, A9 ;
A16: |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * (2 * |(q,q)|)) + ((|(q,q)| - 1) * |(p,((2 * q) + ((|(q,q)| - 1) * p)))|) by
.= (|(q,q)| + 1) * (|(q,q)| + 1) by A15 ;
A17: |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| by EUCLID_2:20;
|(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| by EUCLID_2:19
.= ((1 / (|(q,q)| + 1)) * ((1 / (|(q,q)| + 1)) * (|(q,q)| + 1))) * (|(q,q)| + 1) by
.= ((1 / (|(q,q)| + 1)) * ((|(q,q)| + 1) / (|(q,q)| + 1))) * (|(q,q)| + 1) by XCMPLX_1:99
.= ((1 / (|(q,q)| + 1)) * 1) * (|(q,q)| + 1) by
.= (|(q,q)| + 1) / (|(q,q)| + 1) by XCMPLX_1:99
.= 1 by ;
then |.((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))).| = 1 by ;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (0. ())).| = 1 by RLVECT_1:4;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + ((- 1) * (0. ()))).| = 1 by RLVECT_1:10;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) - (0. ())).| = 1 by RLVECT_1:16;
then y1 in Sphere ((0. ()),1) by TOPREAL9:9;
hence (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S by ; :: thesis: S1[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))]
thus S1[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] ; :: thesis: verum
end;
consider g1 being Function of ([#] (TPlane (p,(0. ())))),([#] S) such that
A18: for x being object st x in [#] (TPlane (p,(0. ()))) holds
S1[x,g1 . x] from reconsider g = g1 as Function of (TPlane (p,(0. ()))),S ;
reconsider f1 = stereographic_projection (S,p) as Function of ([#] S),([#] (TPlane (p,(0. ())))) ;
|.(0. ()).| <> |.p.| by ;
then 0. () <> (1 + 1) * p by RLVECT_1:11;
then 0. () <> (1 * p) + (1 * p) by RLVECT_1:def 6;
then 0. () <> (1 * p) + p by RLVECT_1:def 8;
then 0. () <> p + p by RLVECT_1:def 8;
then p + (- p) <> p + p by RLVECT_1:5;
then A19: not - p in {p} by TARSKI:def 1;
|.(- p).| = 1 by ;
then |.((- p) + (0. ())).| = 1 by RLVECT_1:4;
then |.((- p) + ((- 1) * (0. ()))).| = 1 by RLVECT_1:10;
then |.((- p) - (0. ())).| = 1 by RLVECT_1:16;
then A20: - p in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;
then A21: [#] S <> {} by ;
A22: for y, x being object holds
( y in [#] (TPlane (p,(0. ()))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )
proof
let y, x be object ; :: thesis: ( y in [#] (TPlane (p,(0. ()))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )
hereby :: thesis: ( x in [#] S & f1 . x = y implies ( y in [#] (TPlane (p,(0. ()))) & g1 . y = x ) )
assume A23: y in [#] (TPlane (p,(0. ()))) ; :: thesis: ( g1 . y = x implies ( x in [#] S & f1 . x = y ) )
assume A24: g1 . y = x ; :: thesis: ( x in [#] S & f1 . x = y )
hence A25: x in [#] S by ; :: thesis: f1 . x = y
[#] S c= [#] () by PRE_TOPC:def 4;
then reconsider qx = x as Point of () by A25;
[#] (TPlane (p,(0. ()))) c= [#] () by PRE_TOPC:def 4;
then reconsider qy = y as Point of () by A23;
qy in TPlane (p,(0. ())) by A23;
then A26: qx = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by ;
qx in S by ;
then A27: (stereographic_projection (S,p)) . qx = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by ;
qy in Plane (p,(0. ())) by ;
then consider y1 being Point of () such that
A28: ( y1 = qy & |(p,(y1 - (0. ())))| = 0 ) ;
|(p,(qy + ((- 1) * (0. ()))))| = 0 by ;
then |(p,(qy + (0. ())))| = 0 by RLVECT_1:10;
then A29: |(p,qy)| = 0 by RLVECT_1:4;
A30: |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| = (2 * |(qy,p)|) + ((|(qy,qy)| - 1) * |(p,p)|) by EUCLID_2:25
.= |(qy,qy)| - 1 by ;
A31: |(qx,p)| = (1 / (|(qy,qy)| + 1)) * |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| by
.= ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) * 1 by ;
A32: |(qy,qy)| >= 0 by EUCLID_2:35;
A33: 1 - |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) - ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) by
.= ((|(qy,qy)| + 1) - (|(qy,qy)| - 1)) / (|(qy,qy)| + 1) by XCMPLX_1:120
.= 2 / (|(qy,qy)| + 1) ;
A34: 1 / (1 - |(qx,p)|) = (|(qy,qy)| + 1) / 2 by ;
A35: ((|(qy,qy)| + 1) / 2) * qx = (((|(qy,qy)| + 1) / 2) * (1 / (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by
.= (((|(qy,qy)| + 1) * 1) / (2 * (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76
.= (((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76
.= (1 * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by
.= ((1 / 2) * (2 * qy)) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 5
.= (((1 / 2) * 2) * qy) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 7
.= (1 * qy) + (((1 / 2) * (|(qy,qy)| - 1)) * p) by RLVECT_1:def 7
.= qy + (((|(qy,qy)| - 1) / 2) * p) by RLVECT_1:def 8 ;
A36: ((|(qy,qy)| + 1) / 2) * |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) / 2) by
.= 1 * ((|(qy,qy)| - 1) / 2) by
.= (|(qy,qy)| - 1) / 2 ;
thus f1 . x = (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| + 1) / 2) * (|(qx,p)| * p)) by
.= (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| - 1) / 2) * p) by
.= y by ; :: thesis: verum
end;
assume A37: x in [#] S ; :: thesis: ( not f1 . x = y or ( y in [#] (TPlane (p,(0. ()))) & g1 . y = x ) )
assume A38: f1 . x = y ; :: thesis: ( y in [#] (TPlane (p,(0. ()))) & g1 . y = x )
hence y in [#] (TPlane (p,(0. ()))) by ; :: thesis: g1 . y = x
[#] S c= [#] () by PRE_TOPC:def 4;
then reconsider qx = x as Point of () by A37;
qx in S by A37;
then A40: y = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by ;
then reconsider qy = y as Point of () ;
A41: qy in TPlane (p,(0. ())) by ;
A42: g1 . qy = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by ;
reconsider qx1 = qx as Point of (TOP-REAL n1) ;
qx1 in Sphere ((0. ()),1) by ;
then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;
then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;
then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;
then |.qx.| = 1 by RLVECT_1:4;
then |(qx,qx)| = 1 ^2 by EUCLID_2:4;
then A43: |(qx,qx)| = 1 * 1 by SQUARE_1:def 1;
A44: |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| = |((|(qx,p)| * p),qx)| - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:27
.= (|(qx,p)| * |(qx,p)|) - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:19
.= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * |(p,(|(qx,p)| * p))|) by EUCLID_2:19
.= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * (|(qx,p)| * |(p,p)|)) by EUCLID_2:20
.= 0 by A5 ;
A45: |(qx,(qx - (|(qx,p)| * p)))| = |(qx,qx)| - |(qx,(|(qx,p)| * p))| by EUCLID_2:24
.= 1 - (|(qx,p)| * |(qx,p)|) by ;
A46: |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))| = |(qx,(qx - (|(qx,p)| * p)))| - |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| by EUCLID_2:24
.= (1 - (|(qx,p)| * |(qx,p)|)) + 0 by ;
|(qx,p)| <> 1
proof
assume A47: |(qx,p)| = 1 ; :: thesis: contradiction
A48: not qx in {p} by ;
|(qx,p)| - |(qx,qx)| = 0 by ;
then A49: |(qx,(p - qx))| = 0 by EUCLID_2:27;
|(p,p)| - |(qx,p)| = 0 by ;
then A50: |((p - qx),p)| = 0 by EUCLID_2:24;
|((p - qx),(p - qx))| = 0 - 0 by ;
then p - qx = 0. () by EUCLID_2:41;
then p = qx by RLVECT_1:21;
hence contradiction by A48, TARSKI:def 1; :: thesis: verum
end;
then A51: 1 - |(qx,p)| <> 0 ;
then A52: (1 - |(qx,p)|) * (1 - |(qx,p)|) <> 0 ;
A53: |(qy,qy)| = (1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),qy)| by
.= (1 / (1 - |(qx,p)|)) * ((1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))|) by
.= ((1 / (1 - |(qx,p)|)) * (1 / (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by A46
.= (1 / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:102
.= (1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:99 ;
A54: |(qy,qy)| + 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) + (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by
.= ((1 - (|(qx,p)| * |(qx,p)|)) + ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:62
.= (2 * (1 - |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))
.= 2 * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74
.= 2 * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78
.= 2 * (1 / (1 - |(qx,p)|)) by
.= (2 * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;
A55: |(qy,qy)| - 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) - (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by
.= ((1 - (|(qx,p)| * |(qx,p)|)) - ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:120
.= ((2 * |(qx,p)|) * (1 - |(qx,p)|)) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))
.= (2 * |(qx,p)|) * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74
.= (2 * |(qx,p)|) * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78
.= (2 * |(qx,p)|) * (1 / (1 - |(qx,p)|)) by
.= ((2 * |(qx,p)|) * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;
A56: 1 / (|(qy,qy)| + 1) = (1 - |(qx,p)|) / 2 by ;
A57: (|(qy,qy)| - 1) / (|(qy,qy)| + 1) = (2 * |(qx,p)|) / ((1 - |(qx,p)|) * (2 / (1 - |(qx,p)|))) by
.= (2 * |(qx,p)|) / ((2 * (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:74
.= (2 * |(qx,p)|) / (2 * ((1 - |(qx,p)|) / (1 - |(qx,p)|))) by XCMPLX_1:74
.= (2 * |(qx,p)|) / (2 * 1) by
.= |(qx,p)| ;
A58: (1 - |(qx,p)|) * qy = ((1 - |(qx,p)|) * (1 / (1 - |(qx,p)|))) * (qx - (|(qx,p)| * p)) by
.= (((1 - |(qx,p)|) * 1) / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by XCMPLX_1:74
.= 1 * (qx - (|(qx,p)| * p)) by
.= qx - (|(qx,p)| * p) by RLVECT_1:def 8 ;
thus g1 . y = ((1 / (|(qy,qy)| + 1)) * (2 * qy)) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by
.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 7
.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + (((1 / (|(qy,qy)| + 1)) * (|(qy,qy)| - 1)) * p) by RLVECT_1:def 7
.= ((1 - |(qx,p)|) * qy) + (((1 * (|(qy,qy)| - 1)) / (|(qy,qy)| + 1)) * p) by
.= qx - ((|(qx,p)| * p) - (|(qx,p)| * p)) by
.= qx - (0. ()) by RLVECT_1:5
.= qx + ((- 1) * (0. ())) by RLVECT_1:16
.= qx + (0. ()) by RLVECT_1:10
.= x by RLVECT_1:4 ; :: thesis: verum
end;
for y being object holds
( y in [#] (TPlane (p,(0. ()))) iff ex x being object st
( x in dom () & y = () . x ) )
proof
let y be object ; :: thesis: ( y in [#] (TPlane (p,(0. ()))) iff ex x being object st
( x in dom () & y = () . x ) )

hereby :: thesis: ( ex x being object st
( x in dom () & y = () . x ) implies y in [#] (TPlane (p,(0. ()))) )
assume A59: y in [#] (TPlane (p,(0. ()))) ; :: thesis: ex x being object st
( x in dom () & y = () . x )

reconsider x = g . y as object ;
take x = x; :: thesis: ( x in dom () & y = () . x )
thus x in dom () by A22, A3, A59; :: thesis: y = () . x
thus y = () . x by ; :: thesis: verum
end;
given x being object such that A60: ( x in dom () & y = () . x ) ; :: thesis: y in [#] (TPlane (p,(0. ())))
thus y in [#] (TPlane (p,(0. ()))) by ; :: thesis: verum
end;
then A61: rng () = [#] (TPlane (p,(0. ()))) by FUNCT_1:def 3;
A62: stereographic_projection (S,p) is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom () or not x2 in dom () or not () . x1 = () . x2 or x1 = x2 )
assume A63: ( x1 in dom () & x2 in dom () ) ; :: thesis: ( not () . x1 = () . x2 or x1 = x2 )
assume A64: (stereographic_projection (S,p)) . x1 = () . x2 ; :: thesis: x1 = x2
( g1 . (() . x1) = x1 & g1 . (() . x2) = x2 ) by ;
hence x1 = x2 by A64; :: thesis: verum
end;
A65: stereographic_projection (S,p) is continuous
proof
A66: [#] S c= [#] () by PRE_TOPC:def 4;
set f0 = InnerProduct p;
consider f1 being Function of (TOP-REAL n1),R^1 such that
A67: ( ( for q being Point of () holds f1 . q = 1 ) & f1 is continuous ) by JGRAPH_2:20;
consider f2 being Function of (),R^1 such that
A68: ( ( for q being Point of ()
for r1, r2 being Real st f1 . q = r1 & () . q = r2 holds
f2 . q = r1 - r2 ) & f2 is continuous ) by ;
reconsider f2 = f2 as continuous Function of (),R^1 by A68;
reconsider S1 = S as non empty TopSpace by ;
set f3 = f2 | S1;
A69: for q being Point of () st q in S1 holds
(f2 | S1) . q = 1 - |(q,p)|
proof
let q be Point of (); :: thesis: ( q in S1 implies (f2 | S1) . q = 1 - |(q,p)| )
assume B70: q in S1 ; :: thesis: (f2 | S1) . q = 1 - |(q,p)|
A71: [#] S1 c= [#] () by PRE_TOPC:def 4;
( (InnerProduct p) . q = |(q,p)| & f1 . q = 1 ) by ;
then A72: f2 . q = 1 - |(q,p)| by A68;
thus (f2 | S1) . q = (f2 | the carrier of S1) . q by
.= 1 - |(q,p)| by ; :: thesis: verum
end;
A73: for q being Point of S1 holds (f2 | S1) . q <> 0
proof
let q be Point of S1; :: thesis: (f2 | S1) . q <> 0
reconsider qx = q as Point of () by A66;
reconsider qx1 = qx as Point of (TOP-REAL n1) ;
qx1 in Sphere ((0. ()),1) by ;
then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;
then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;
then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;
then |.qx.| = 1 by RLVECT_1:4;
then |(qx,qx)| = 1 ^2 by EUCLID_2:4;
then A74: |(qx,qx)| = 1 * 1 by SQUARE_1:def 1;
|(qx,p)| <> 1
proof
assume A75: |(qx,p)| = 1 ; :: thesis: contradiction
A76: not qx in {p} by ;
|(qx,p)| - |(qx,qx)| = 0 by ;
then A77: |(qx,(p - qx))| = 0 by EUCLID_2:27;
|(p,p)| - |(qx,p)| = 0 by ;
then A78: |((p - qx),p)| = 0 by EUCLID_2:24;
|((p - qx),(p - qx))| = 0 - 0 by ;
then p - qx = 0. () by EUCLID_2:41;
then p = qx by RLVECT_1:21;
hence contradiction by A76, TARSKI:def 1; :: thesis: verum
end;
then A79: 1 - |(qx,p)| <> 0 ;
qx in S1 ;
hence (f2 | S1) . q <> 0 by ; :: thesis: verum
end;
then consider f4 being Function of S1,R^1 such that
A80: ( ( for q being Point of S1
for r1 being Real st (f2 | S1) . q = r1 holds
f4 . q = 1 / r1 ) & f4 is continuous ) by JGRAPH_2:26;
consider f5 being Function of S1,(TOP-REAL n1) such that
A81: ( ( for a being Point of S1
for b being Point of ()
for r being Real st a = b & f4 . a = r holds
f5 . b = r * b ) & f5 is continuous ) by ;
set f6 = () | S1;
A82: for q being Point of () st q in S1 holds
(() | S1) . q = |(q,p)|
proof
let q be Point of (); :: thesis: ( q in S1 implies (() | S1) . q = |(q,p)| )
assume B83: q in S1 ; :: thesis: (() | S1) . q = |(q,p)|
A84: [#] S1 c= [#] () by PRE_TOPC:def 4;
A85: (InnerProduct p) . q = |(q,p)| by Def1;
thus (() | S1) . q = (() | the carrier of S1) . q by
.= |(q,p)| by ; :: thesis: verum
end;
consider f7 being Function of S1,R^1 such that
A86: ( ( for q being Point of S1
for r1, r2 being Real st (() | S1) . q = r1 & (f2 | S1) . q = r2 holds
f7 . q = r1 / r2 ) & f7 is continuous ) by ;
reconsider p1 = - p as Point of (TOP-REAL n1) ;
consider f8 being Function of S1,(TOP-REAL n1) such that
A87: ( ( for r being Point of S1 holds f8 . r = (f7 . r) * p1 ) & f8 is continuous ) by ;
consider f9 being Function of S,() such that
A88: ( ( for r being Point of S1 holds f9 . r = (f5 . r) + (f8 . r) ) & f9 is continuous ) by ;
A89: dom () = [#] S by FUNCT_2:def 1
.= dom f9 by FUNCT_2:def 1 ;
for x being object st x in dom () holds
() . x = f9 . x
proof
let x be object ; :: thesis: ( x in dom () implies () . x = f9 . x )
assume A90: x in dom () ; :: thesis: () . x = f9 . x
then reconsider qx = x as Point of () by A66;
A91: qx in S by A90;
reconsider r = qx as Point of S1 by A90;
A92: (f2 | S1) . r = 1 - |(qx,p)| by ;
A93: f4 . r = 1 / (1 - |(qx,p)|) by ;
A94: ((InnerProduct p) | S1) . r = |(qx,p)| by ;
A95: f8 . r = (f7 . r) * (- p) by A87
.= (|(qx,p)| / (1 - |(qx,p)|)) * (- p) by ;
f9 . x = (f5 . r) + (f8 . r) by A88
.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 * |(qx,p)|) / (1 - |(qx,p)|)) * (- p)) by
.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 / (1 - |(qx,p)|)) * |(qx,p)|) * (- p)) by XCMPLX_1:74
.= ((1 / (1 - |(qx,p)|)) * qx) + ((1 / (1 - |(qx,p)|)) * (|(qx,p)| * (- p))) by RLVECT_1:def 7
.= (1 / (1 - |(qx,p)|)) * (qx + (|(qx,p)| * (- p))) by RLVECT_1:def 5
.= (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by RLVECT_1:25 ;
hence (stereographic_projection (S,p)) . x = f9 . x by ; :: thesis: verum
end;
hence stereographic_projection (S,p) is continuous by ; :: thesis: verum
end;
A96: g is continuous
proof
consider g0 being Function of (TOP-REAL n1),R^1 such that
A98: ( ( for q being Point of (TOP-REAL n1) holds g0 . q = |.q.| ) & g0 is continuous ) by JORDAN2C:84;
consider g1 being Function of (),R^1 such that
A99: ( ( for q being Point of ()
for r1 being Real st g0 . q = r1 holds
g1 . q = r1 * r1 ) & g1 is continuous ) by ;
consider g2 being Function of (),R^1 such that
A100: ( ( for q being Point of ()
for r1 being Real st g1 . q = r1 holds
g2 . q = r1 + 1 ) & g2 is continuous ) by ;
consider g3 being Function of (),R^1 such that
A101: ( ( for q being Point of ()
for r1 being Real st g1 . q = r1 holds
g3 . q = r1 + (- 1) ) & g3 is continuous ) by ;
consider g4 being Function of (),R^1 such that
A102: ( ( for q being Point of () holds g4 . q = 2 ) & g4 is continuous ) by JGRAPH_2:20;
A103: for q being Point of () holds g2 . q <> 0
proof
let q be Point of (); :: thesis: g2 . q <> 0
g0 . q = |.q.| by A98;
then g1 . q = |.q.| * |.q.| by A99;
then g2 . q = () + 1 by A100;
hence g2 . q <> 0 ; :: thesis: verum
end;
then consider g5 being Function of (),R^1 such that
A104: ( ( for q being Point of ()
for r1, r2 being Real st g4 . q = r1 & g2 . q = r2 holds
g5 . q = r1 / r2 ) & g5 is continuous ) by ;
reconsider g6 = g5 | (TPlane (p,(0. ()))) as continuous Function of (TPlane (p,(0. ()))),R^1 by A104;
consider g7 being Function of (TPlane (p,(0. ()))),(TOP-REAL n1) such that
A105: ( ( for a being Point of (TPlane (p,(0. ())))
for b being Point of ()
for r being Real st a = b & g6 . a = r holds
g7 . b = r * b ) & g7 is continuous ) by MFOLD_1:2;
consider g8 being Function of (),R^1 such that
A106: ( ( for q being Point of ()
for r1, r2 being Real st g3 . q = r1 & g2 . q = r2 holds
g8 . q = r1 / r2 ) & g8 is continuous ) by ;
reconsider p1 = p as Point of (TOP-REAL n1) ;
reconsider g9 = g8 | (TPlane (p,(0. ()))) as continuous Function of (TPlane (p,(0. ()))),R^1 by A106;
consider g10 being Function of (TPlane (p,(0. ()))),(TOP-REAL n1) such that
A107: ( ( for r being Point of (TPlane (p,(0. ()))) holds g10 . r = (g9 . r) * p1 ) & g10 is continuous ) by JGRAPH_6:9;
consider g11 being Function of (TPlane (p,(0. ()))),(TOP-REAL n1) such that
A108: ( ( for r being Point of (TPlane (p,(0. ()))) holds g11 . r = (g7 . r) + (g10 . r) ) & g11 is continuous ) by ;
A109: dom g = [#] (TPlane (p,(0. ()))) by
.= dom g11 by FUNCT_2:def 1 ;
for x being object st x in dom g holds
g . x = g11 . x
proof
let x be object ; :: thesis: ( x in dom g implies g . x = g11 . x )
assume A110: x in dom g ; :: thesis: g . x = g11 . x
[#] (TPlane (p,(0. ()))) c= [#] () by PRE_TOPC:def 4;
then reconsider qx = x as Point of () by A110;
A112: qx in TPlane (p,(0. ())) by A110;
reconsider r = qx as Point of (TPlane (p,(0. ()))) by A110;
A113: [#] (TPlane (p,(0. ()))) c= [#] () by PRE_TOPC:def 4;
A114: g0 . qx = |.qx.| by A98;
A115: g1 . qx = |.qx.| * |.qx.| by
.= |.qx.| ^2 by SQUARE_1:def 1
.= |(qx,qx)| by EUCLID_2:4 ;
A116: g2 . qx = |(qx,qx)| + 1 by ;
A117: g4 . qx = 2 by A102;
A118: g6 . qx = (g5 | the carrier of (TPlane (p,(0. ())))) . qx by
.= g5 . qx by
.= 2 / (|(qx,qx)| + 1) by ;
A119: g3 . qx = |(qx,qx)| + (- 1) by ;
A120: g9 . qx = (g8 | the carrier of (TPlane (p,(0. ())))) . qx by
.= g8 . qx by
.= (|(qx,qx)| - 1) / (|(qx,qx)| + 1) by ;
A121: g7 . r = (2 / (|(qx,qx)| + 1)) * qx by ;
g11 . x = (g7 . r) + (g10 . r) by A108
.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 * (|(qx,qx)| - 1)) / (|(qx,qx)| + 1)) * p) by
.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74
.= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74
.= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 7
.= ((1 / (|(qx,qx)| + 1)) * (2 * qx)) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 7
.= (1 / (|(qx,qx)| + 1)) * ((2 * qx) + ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 5 ;
hence g . x = g11 . x by ; :: thesis: verum
end;
hence g is continuous by ; :: thesis: verum
end;
reconsider f2 = f1 as [#] (TPlane (p,(0. ()))) -valued Relation ;
f2 is onto by ;
then A122: f1 " = f1 " by ;
g1 = f1 " by ;
hence stereographic_projection (S,p) is being_homeomorphism by ; :: thesis: verum