:: MFOLD_2 semantic presentation
begin
registration
cluster {} -> {} -valued ;
correctness
coherence
{} is {} -valued ;
by FUNCTOR0:1;
cluster {} -> onto ;
correctness
coherence
{} is onto ;
proof
rng {} = {} ;
hence {} is onto by FUNCT_2:def_3; ::_thesis: verum
end;
end;
theorem Th1: :: MFOLD_2:1
for f being Function
for Y being set holds dom (Y |` f) = f " Y
proof
let f be Function; ::_thesis: for Y being set holds dom (Y |` f) = f " Y
let Y be set ; ::_thesis: dom (Y |` f) = f " Y
for x being set holds
( x in dom (Y |` f) iff x in f " Y )
proof
let x be set ; ::_thesis: ( x in dom (Y |` f) iff x in f " Y )
hereby ::_thesis: ( x in f " Y implies x in dom (Y |` f) )
assume x in dom (Y |` f) ; ::_thesis: x in f " Y
then consider y being set such that
A1: [x,y] in Y |` f by XTUPLE_0:def_12;
( y in Y & [x,y] in f ) by A1, RELAT_1:def_12;
hence x in f " Y by RELAT_1:def_14; ::_thesis: verum
end;
assume x in f " Y ; ::_thesis: x in dom (Y |` f)
then consider y being set such that
A2: ( [x,y] in f & y in Y ) by RELAT_1:def_14;
[x,y] in Y |` f by A2, RELAT_1:def_12;
hence x in dom (Y |` f) by XTUPLE_0:def_12; ::_thesis: verum
end;
hence dom (Y |` f) = f " Y by TARSKI:1; ::_thesis: verum
end;
theorem Th2: :: MFOLD_2:2
for f being Function
for Y1, Y2 being set st Y2 c= Y1 holds
(Y1 |` f) " Y2 = f " Y2
proof
let f be Function; ::_thesis: for Y1, Y2 being set st Y2 c= Y1 holds
(Y1 |` f) " Y2 = f " Y2
let Y1, Y2 be set ; ::_thesis: ( Y2 c= Y1 implies (Y1 |` f) " Y2 = f " Y2 )
assume A1: Y2 c= Y1 ; ::_thesis: (Y1 |` f) " Y2 = f " Y2
for x being set holds
( x in (Y1 |` f) " Y2 iff x in f " Y2 )
proof
let x be set ; ::_thesis: ( x in (Y1 |` f) " Y2 iff x in f " Y2 )
hereby ::_thesis: ( x in f " Y2 implies x in (Y1 |` f) " Y2 )
assume x in (Y1 |` f) " Y2 ; ::_thesis: x in f " Y2
then consider y being set such that
A2: ( [x,y] in Y1 |` f & y in Y2 ) by RELAT_1:def_14;
[x,y] in f by A2, RELAT_1:def_12;
hence x in f " Y2 by A2, RELAT_1:def_14; ::_thesis: verum
end;
assume x in f " Y2 ; ::_thesis: x in (Y1 |` f) " Y2
then consider y being set such that
A3: ( [x,y] in f & y in Y2 ) by RELAT_1:def_14;
[x,y] in Y1 |` f by A3, A1, RELAT_1:def_12;
hence x in (Y1 |` f) " Y2 by A3, RELAT_1:def_14; ::_thesis: verum
end;
hence (Y1 |` f) " Y2 = f " Y2 by TARSKI:1; ::_thesis: verum
end;
theorem Th3: :: MFOLD_2:3
for S, T being TopStruct
for f being Function of S,T st f is being_homeomorphism holds
f " is being_homeomorphism
proof
let S, T be TopStruct ; ::_thesis: for f being Function of S,T st f is being_homeomorphism holds
f " is being_homeomorphism
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f " is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: f " is being_homeomorphism
then A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) by TOPS_2:def_5;
percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
suppose ( not S is empty & not T is empty ) ; ::_thesis: f " is being_homeomorphism
hence f " is being_homeomorphism by A1, TOPS_2:56; ::_thesis: verum
end;
supposeA3: ( S is empty or T is empty ) ; ::_thesis: f " is being_homeomorphism
A4: f = {}
proof
percases ( S is empty or T is empty ) by A3;
suppose S is empty ; ::_thesis: f = {}
hence f = {} ; ::_thesis: verum
end;
suppose T is empty ; ::_thesis: f = {}
hence f = {} ; ::_thesis: verum
end;
end;
end;
reconsider g = f as one-to-one onto PartFunc of {},{} by A4, FUNCTOR0:1;
A5: f " = g " by A2;
A6: ( dom (f ") = [#] T & rng (f ") = [#] S ) by A2, A4;
reconsider g1 = f " as one-to-one onto PartFunc of {},{} by A5;
(f ") " = g1 " by A2, A4;
hence f " is being_homeomorphism by A4, A6, A2, TOPS_2:def_5; ::_thesis: verum
end;
end;
end;
definition
let S, T be TopStruct ;
:: original: are_homeomorphic
redefine predS,T are_homeomorphic ;
symmetry
for S, T being TopStruct st R91(b1,b2) holds
R91(b2,b1)
proof
let S, T be TopStruct ; ::_thesis: ( R91(S,T) implies R91(T,S) )
assume S,T are_homeomorphic ; ::_thesis: R91(T,S)
then consider f being Function of S,T such that
A1: f is being_homeomorphism by T_0TOPSP:def_1;
f " is being_homeomorphism by A1, Th3;
hence R91(T,S) by T_0TOPSP:def_1; ::_thesis: verum
end;
end;
theorem Th4: :: MFOLD_2:4
for T1, T2 being TopSpace
for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
proof
let T1, T2 be TopSpace; ::_thesis: for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
let A2 be Subset of T2; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
A2: ( dom f = [#] T1 & rng f = [#] T2 ) by A1, TOPS_2:def_5;
T1,T2 are_homeomorphic by A1, T_0TOPSP:def_1;
then ( T1 is empty iff T2 is empty ) by YELLOW14:18;
then A3: ( [#] T1 = {} iff [#] T2 = {} ) ;
A4: rng f = [#] T2 by A1, TOPS_2:def_5;
set A = f " A2;
let g be Function of (T1 | (f " A2)),(T2 | A2); ::_thesis: ( g = A2 |` f implies g is being_homeomorphism )
assume A5: g = A2 |` f ; ::_thesis: g is being_homeomorphism
A6: rng g = A2 by A2, A5, RELAT_1:89;
A7: f is one-to-one by A1, TOPS_2:def_5;
then A8: g is one-to-one by A5, FUNCT_1:58;
A9: dom g = f " A2 by A5, Th1;
set TA = T1 | (f " A2);
set TB = T2 | A2;
A10: [#] (T1 | (f " A2)) = f " A2 by PRE_TOPC:def_5;
A11: ( [#] (T1 | (f " A2)) = {} iff [#] (T2 | A2) = {} ) by A6;
A12: [#] (T2 | A2) = A2 by PRE_TOPC:def_5;
A13: f is continuous by A1, TOPS_2:def_5;
for P being Subset of (T2 | A2) st P is open holds
g " P is open
proof
let P be Subset of (T2 | A2); ::_thesis: ( P is open implies g " P is open )
assume P is open ; ::_thesis: g " P is open
then consider P1 being Subset of T2 such that
A14: P1 is open and
A15: P = P1 /\ A2 by A12, TSP_1:def_1;
A16: f " P1 is open by A3, A13, A14, TOPS_2:43;
g " P = f " P by A5, Th2, A15, XBOOLE_1:17
.= (f " P1) /\ the carrier of (T1 | (f " A2)) by A10, A15, FUNCT_1:68 ;
hence g " P is open by A16, TSP_1:def_1; ::_thesis: verum
end;
then A17: g is continuous by A11, TOPS_2:43;
A18: f " is continuous by A1, TOPS_2:def_5;
for P being Subset of (T1 | (f " A2)) st P is open holds
(g ") " P is open
proof
let P be Subset of (T1 | (f " A2)); ::_thesis: ( P is open implies (g ") " P is open )
assume P is open ; ::_thesis: (g ") " P is open
then consider P1 being Subset of T1 such that
A19: P1 is open and
A20: P = P1 /\ (f " A2) by A10, TSP_1:def_1;
A21: (f ") " P1 is open by A3, A18, A19, TOPS_2:43;
A2 = f .: (f " A2) by A2, FUNCT_1:77;
then A22: the carrier of (T2 | A2) = (f ") " (f " A2) by A12, A4, A7, TOPS_2:54;
(g ") " P = (A2 |` f) .: P by A5, A6, A8, A12, TOPS_2:54
.= (f .: P) /\ the carrier of (T2 | A2) by A12, FUNCT_1:67
.= ((f ") " (P1 /\ (f " A2))) /\ the carrier of (T2 | A2) by A4, A7, A20, TOPS_2:54
.= (((f ") " P1) /\ ((f ") " (f " A2))) /\ the carrier of (T2 | A2) by FUNCT_1:68
.= ((f ") " P1) /\ (((f ") " (f " A2)) /\ the carrier of (T2 | A2)) by XBOOLE_1:16
.= ((f ") " P1) /\ the carrier of (T2 | A2) by A22 ;
hence (g ") " P is open by A21, TSP_1:def_1; ::_thesis: verum
end;
then g " is continuous by A11, TOPS_2:43;
hence g is being_homeomorphism by A6, A9, A10, A8, A12, A17, TOPS_2:def_5; ::_thesis: verum
end;
theorem Th5: :: MFOLD_2:5
for T1, T2 being TopSpace
for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
f " A2,A2 are_homeomorphic
proof
let T1, T2 be TopSpace; ::_thesis: for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
f " A2,A2 are_homeomorphic
let A2 be Subset of T2; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
f " A2,A2 are_homeomorphic
let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies f " A2,A2 are_homeomorphic )
assume A1: f is being_homeomorphism ; ::_thesis: f " A2,A2 are_homeomorphic
A2: dom (A2 |` f) = f " A2 by Th1
.= [#] (T1 | (f " A2)) by PRE_TOPC:def_5 ;
rng f = [#] T2 by A1, TOPS_2:def_5;
then rng (A2 |` f) = A2 by RELAT_1:89
.= [#] (T2 | A2) by PRE_TOPC:def_5 ;
then reconsider g = A2 |` f as Function of (T1 | (f " A2)),(T2 | A2) by A2, FUNCT_2:1;
g is being_homeomorphism by A1, Th4;
then T1 | (f " A2),T2 | A2 are_homeomorphic by T_0TOPSP:def_1;
hence f " A2,A2 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum
end;
theorem :: MFOLD_2:6
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
A2,A1 are_homeomorphic
proof
let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
A2,A1 are_homeomorphic
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
A2,A1 are_homeomorphic
let A2 be Subset of T2; ::_thesis: ( A1,A2 are_homeomorphic implies A2,A1 are_homeomorphic )
assume A1,A2 are_homeomorphic ; ::_thesis: A2,A1 are_homeomorphic
then T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1;
hence A2,A1 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum
end;
theorem Th7: :: MFOLD_2:7
for T1, T2 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is empty iff A2 is empty )
proof
let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is empty iff A2 is empty )
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is empty iff A2 is empty )
let A2 be Subset of T2; ::_thesis: ( A1,A2 are_homeomorphic implies ( A1 is empty iff A2 is empty ) )
assume A1,A2 are_homeomorphic ; ::_thesis: ( A1 is empty iff A2 is empty )
then T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1;
then consider f being Function of (T1 | A1),(T2 | A2) such that
A1: f is being_homeomorphism by T_0TOPSP:def_1;
( dom f = [#] (T1 | A1) & rng f = [#] (T2 | A2) & f is one-to-one & f is continuous & f " is continuous ) by A1, TOPS_2:def_5;
hence ( A1 is empty iff A2 is empty ) by PRE_TOPC:def_5; ::_thesis: verum
end;
theorem Th8: :: MFOLD_2:8
for T1, T2, T3 being TopSpace
for A1 being Subset of T1
for A2 being Subset of T2
for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
proof
let T1, T2, T3 be TopSpace; ::_thesis: for A1 being Subset of T1
for A2 being Subset of T2
for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2
for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
let A2 be Subset of T2; ::_thesis: for A3 being Subset of T3 st A1,A2 are_homeomorphic & A2,A3 are_homeomorphic holds
A1,A3 are_homeomorphic
let A3 be Subset of T3; ::_thesis: ( A1,A2 are_homeomorphic & A2,A3 are_homeomorphic implies A1,A3 are_homeomorphic )
assume A1: A1,A2 are_homeomorphic ; ::_thesis: ( not A2,A3 are_homeomorphic or A1,A3 are_homeomorphic )
then A2: T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def_1;
assume A3: A2,A3 are_homeomorphic ; ::_thesis: A1,A3 are_homeomorphic
then A4: T2 | A2,T3 | A3 are_homeomorphic by METRIZTS:def_1;
percases ( not A2 is empty or A2 is empty ) ;
supposeA5: not A2 is empty ; ::_thesis: A1,A3 are_homeomorphic
then A6: ( not A1 is empty & not A3 is empty ) by A1, A3, Th7;
( not T1 is empty & not T2 is empty & not T3 is empty ) by A5, A1, A3, Th7;
then T1 | A1,T3 | A3 are_homeomorphic by A2, A4, A6, A5, BORSUK_3:3;
hence A1,A3 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum
end;
suppose A2 is empty ; ::_thesis: A1,A3 are_homeomorphic
then A7: ( A1 is empty & A3 is empty ) by A1, A3, Th7;
reconsider f = {} as Function ;
A8: ( the carrier of (T1 | A1) = {} & the carrier of (T3 | A3) = {} ) by A7;
( dom f = {} & rng f = {} ) ;
then reconsider f = f as Function of (T1 | A1),(T3 | A3) by A8, FUNCT_2:1;
A9: ( dom f = [#] (T1 | A1) & rng f = [#] (T3 | A3) ) by A8;
for P1 being Subset of (T3 | A3) st P1 is closed holds
f " P1 is closed ;
then A10: f is continuous by PRE_TOPC:def_6;
reconsider g = f as one-to-one onto PartFunc of {},{} by FUNCTOR0:1;
for P1 being Subset of (T1 | A1) st P1 is closed holds
(f ") " P1 is closed by A7;
then f " is continuous by PRE_TOPC:def_6;
then f is being_homeomorphism by A9, A10, TOPS_2:def_5;
then T1 | A1,T3 | A3 are_homeomorphic by T_0TOPSP:def_1;
hence A1,A3 are_homeomorphic by METRIZTS:def_1; ::_thesis: verum
end;
end;
end;
theorem Th9: :: MFOLD_2:9
for T1, T2 being TopSpace st T1 is second-countable & T1,T2 are_homeomorphic holds
T2 is second-countable
proof
let T1, T2 be TopSpace; ::_thesis: ( T1 is second-countable & T1,T2 are_homeomorphic implies T2 is second-countable )
assume T1 is second-countable ; ::_thesis: ( not T1,T2 are_homeomorphic or T2 is second-countable )
then A1: weight T1 c= omega by WAYBEL23:def_6;
assume T1,T2 are_homeomorphic ; ::_thesis: T2 is second-countable
then weight T1 = weight T2 by METRIZTS:4;
hence T2 is second-countable by A1, WAYBEL23:def_6; ::_thesis: verum
end;
theorem Th10: :: MFOLD_2:10
for M, N being non empty TopSpace st M is Hausdorff & M,N are_homeomorphic holds
N is Hausdorff
proof
let M, N be non empty TopSpace; ::_thesis: ( M is Hausdorff & M,N are_homeomorphic implies N is Hausdorff )
assume A1: M is Hausdorff ; ::_thesis: ( not M,N are_homeomorphic or N is Hausdorff )
assume M,N are_homeomorphic ; ::_thesis: N is Hausdorff
then consider f being Function of N,M such that
A2: f is being_homeomorphism by T_0TOPSP:def_1;
A3: ( dom f = [#] N & rng f = [#] M & f is one-to-one & f is continuous & f " is continuous ) by A2, TOPS_2:def_5;
for p, q being Point of N st p <> q holds
ex N1, N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
proof
let p, q be Point of N; ::_thesis: ( p <> q implies ex N1, N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) )
assume p <> q ; ::_thesis: ex N1, N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
then f . p <> f . q by A3, FUNCT_1:def_4;
then consider M1, M2 being Subset of M such that
A4: ( M1 is open & M2 is open & f . p in M1 & f . q in M2 & M1 misses M2 ) by A1, PRE_TOPC:def_10;
reconsider N1 = f " M1 as Subset of N ;
reconsider N2 = f " M2 as Subset of N ;
take N1 ; ::_thesis: ex N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
take N2 ; ::_thesis: ( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
thus ( N1 is open & N2 is open ) by A4, A3, TOPS_2:43; ::_thesis: ( p in N1 & q in N2 & N1 misses N2 )
thus ( p in N1 & q in N2 ) by A4, FUNCT_2:38; ::_thesis: N1 misses N2
thus N1 misses N2 by A4, FUNCT_1:71; ::_thesis: verum
end;
hence N is Hausdorff by PRE_TOPC:def_10; ::_thesis: verum
end;
theorem Th11: :: MFOLD_2:11
for n being Nat
for M, N being non empty TopSpace st M is n -locally_euclidean & M,N are_homeomorphic holds
N is n -locally_euclidean
proof
let n be Nat; ::_thesis: for M, N being non empty TopSpace st M is n -locally_euclidean & M,N are_homeomorphic holds
N is n -locally_euclidean
let M, N be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean & M,N are_homeomorphic implies N is n -locally_euclidean )
assume A1: M is n -locally_euclidean ; ::_thesis: ( not M,N are_homeomorphic or N is n -locally_euclidean )
assume M,N are_homeomorphic ; ::_thesis: N is n -locally_euclidean
then consider f being Function of N,M such that
A2: f is being_homeomorphism by T_0TOPSP:def_1;
A3: ( dom f = [#] N & rng f = [#] M & f is one-to-one & f is continuous & f " is continuous ) by A2, TOPS_2:def_5;
for q being Point of N ex U being a_neighborhood of q ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
proof
let q be Point of N; ::_thesis: ex U being a_neighborhood of q ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
set p = f . q;
consider U1 being a_neighborhood of f . q, S1 being open Subset of (TOP-REAL n) such that
A4: U1,S1 are_homeomorphic by A1, MFOLD_1:def_4;
consider U2 being open Subset of M, S being open Subset of (TOP-REAL n) such that
A5: ( U2 c= U1 & f . q in U2 & U2,S are_homeomorphic ) by A4, MFOLD_1:11;
A6: f " U2 is open by A3, TOPS_2:43;
q in f " U2 by A5, FUNCT_2:38;
then reconsider U = f " U2 as a_neighborhood of q by A6, CONNSP_2:6;
take U ; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S ; ::_thesis: U,S are_homeomorphic
U,U2 are_homeomorphic by A2, Th5;
hence U,S are_homeomorphic by A5, Th8; ::_thesis: verum
end;
hence N is n -locally_euclidean by MFOLD_1:def_4; ::_thesis: verum
end;
theorem Th12: :: MFOLD_2:12
for n being Nat
for M, N being non empty TopSpace st M is n -manifold & M,N are_homeomorphic holds
N is n -manifold
proof
let n be Nat; ::_thesis: for M, N being non empty TopSpace st M is n -manifold & M,N are_homeomorphic holds
N is n -manifold
let M, N be non empty TopSpace; ::_thesis: ( M is n -manifold & M,N are_homeomorphic implies N is n -manifold )
assume A1: M is n -manifold ; ::_thesis: ( not M,N are_homeomorphic or N is n -manifold )
assume A2: M,N are_homeomorphic ; ::_thesis: N is n -manifold
then A3: N is second-countable by A1, Th9;
A4: N is Hausdorff by A1, A2, Th10;
N is n -locally_euclidean by A1, A2, Th11;
hence N is n -manifold by A3, A4; ::_thesis: verum
end;
theorem Th13: :: MFOLD_2:13
for x1, x2 being FinSequence of REAL
for i being Element of NAT st i in dom (mlt (x1,x2)) holds
( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: for i being Element of NAT st i in dom (mlt (x1,x2)) holds
( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
let i be Element of NAT ; ::_thesis: ( i in dom (mlt (x1,x2)) implies ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) )
assume A1: i in dom (mlt (x1,x2)) ; ::_thesis: ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
A2: mlt (x1,x2) = multreal .: (x1,x2) by RVSUM_1:def_9;
( dom multreal = [:REAL,REAL:] & rng x1 c= REAL ) by FUNCT_2:def_1;
then [:(rng x1),(rng x2):] c= dom multreal by ZFMISC_1:96;
then A3: dom (mlt (x1,x2)) = (dom x1) /\ (dom x2) by A2, FUNCOP_1:69;
then i in dom x2 by A1, XBOOLE_0:def_4;
then A4: x2 /. i = x2 . i by PARTFUN1:def_6;
i in dom x1 by A1, A3, XBOOLE_0:def_4;
then x1 /. i = x1 . i by PARTFUN1:def_6;
hence (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) by A4, RVSUM_1:59; ::_thesis: (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i)
hence (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) by A1, PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th14: :: MFOLD_2:14
for x1, x2, y1, y2 being FinSequence of REAL st len x1 = len x2 & len y1 = len y2 holds
mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))
proof
let x1, x2, y1, y2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 & len y1 = len y2 implies mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) )
assume that
A1: len x1 = len x2 and
A2: len y1 = len y2 ; ::_thesis: mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))
A3: multreal .: ((x1 ^ y1),(x2 ^ y2)) = multreal * <:(x1 ^ y1),(x2 ^ y2):> by FUNCOP_1:def_3;
A4: dom (x1 ^ y1) = Seg (len (x1 ^ y1)) by FINSEQ_1:def_3;
( dom multreal = [:REAL,REAL:] & rng (x1 ^ y1) c= REAL ) by FUNCT_2:def_1;
then [:(rng (x1 ^ y1)),(rng (x2 ^ y2)):] c= dom multreal by ZFMISC_1:96;
then A5: dom (multreal * <:(x1 ^ y1),(x2 ^ y2):>) = (dom (x1 ^ y1)) /\ (dom (x2 ^ y2)) by A3, FUNCOP_1:69;
A6: len (x2 ^ y2) = (len x2) + (len y2) by FINSEQ_1:22;
dom (x2 ^ y2) = Seg (len (x2 ^ y2)) by FINSEQ_1:def_3;
then dom (x1 ^ y1) = dom (x2 ^ y2) by A1, A2, A6, A4, FINSEQ_1:22;
then A7: dom (mlt ((x1 ^ y1),(x2 ^ y2))) = dom (x1 ^ y1) by A3, A5, RVSUM_1:def_9;
A8: multreal .: (y1,y2) = multreal * <:y1,y2:> by FUNCOP_1:def_3;
A9: dom multreal = [:REAL,REAL:] by FUNCT_2:def_1;
then [:(rng y1),(rng y2):] c= dom multreal by ZFMISC_1:96;
then A10: dom (multreal * <:y1,y2:>) = (dom y1) /\ (dom y2) by A8, FUNCOP_1:69;
dom y2 = Seg (len y1) by A2, FINSEQ_1:def_3
.= dom y1 by FINSEQ_1:def_3 ;
then A11: dom (mlt (y1,y2)) = dom y1 by A8, A10, RVSUM_1:def_9;
then dom (mlt (y1,y2)) = Seg (len y1) by FINSEQ_1:def_3;
then A12: len (mlt (y1,y2)) = len y1 by FINSEQ_1:def_3;
A13: multreal .: (x1,x2) = multreal * <:x1,x2:> by FUNCOP_1:def_3;
[:(rng x1),(rng x2):] c= dom multreal by A9, ZFMISC_1:96;
then A14: dom (multreal * <:x1,x2:>) = (dom x1) /\ (dom x2) by A13, FUNCOP_1:69;
A15: len (x1 ^ y1) = (len x1) + (len y1) by FINSEQ_1:22;
dom x2 = Seg (len x1) by A1, FINSEQ_1:def_3
.= dom x1 by FINSEQ_1:def_3 ;
then A16: dom (mlt (x1,x2)) = dom x1 by A13, A14, RVSUM_1:def_9;
then A17: dom (mlt (x1,x2)) = Seg (len x1) by FINSEQ_1:def_3;
A18: for i being Nat st 1 <= i & i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) holds
(mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) implies (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i )
assume that
A19: 1 <= i and
A20: i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) ; ::_thesis: (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
i in Seg (len (mlt ((x1 ^ y1),(x2 ^ y2)))) by A19, A20, FINSEQ_1:1;
then A21: i in dom (mlt ((x1 ^ y1),(x2 ^ y2))) by FINSEQ_1:def_3;
then i <= len (x1 ^ y1) by A4, A7, FINSEQ_1:1;
then A22: (x1 ^ y1) /. i = (x1 ^ y1) . i by A19, FINSEQ_4:15;
i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1;
then A23: (x2 ^ y2) /. i = (x2 ^ y2) . i by A19, FINSEQ_4:15;
A24: i <= (len x1) + (len y1) by A15, A4, A7, A21, FINSEQ_1:1;
now__::_thesis:_((x1_^_y1)_/._i)_*_((x2_^_y2)_/._i)_=_((mlt_(x1,x2))_^_(mlt_(y1,y2)))_._i
percases ( i <= len x1 or i > len x1 ) ;
supposeA25: i <= len x1 ; ::_thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
then A26: i in Seg (len x1) by A19, FINSEQ_1:1;
then A27: i in dom x1 by FINSEQ_1:def_3;
i in dom x2 by A1, A26, FINSEQ_1:def_3;
then A28: (x2 ^ y2) . i = x2 . i by FINSEQ_1:def_7;
A29: i in dom (mlt (x1,x2)) by A16, A26, FINSEQ_1:def_3;
then A30: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (x1,x2)) . i by FINSEQ_1:def_7
.= (x1 /. i) * (x2 /. i) by A29, Th13 ;
( x1 /. i = x1 . i & x2 /. i = x2 . i ) by A1, A19, A25, FINSEQ_4:15;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A22, A23, A27, A28, A30, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA31: i > len x1 ; ::_thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1;
then A32: (x2 ^ y2) /. i = (x2 ^ y2) . i by A19, FINSEQ_4:15;
i <= len (x1 ^ y1) by A4, A7, A21, FINSEQ_1:1;
then A33: (x1 ^ y1) /. i = (x1 ^ y1) . i by A19, FINSEQ_4:15;
set k = i -' (len x1);
A34: i -' (len x1) = i - (len x1) by A31, XREAL_1:233;
then A35: i = (len x1) + (i -' (len x1)) ;
i - (len x1) <= ((len x1) + (len y1)) - (len x1) by A24, XREAL_1:13;
then A36: i -' (len x1) <= len y1 by A31, XREAL_1:233;
i -' (len x1) > 0 by A31, A34, XREAL_1:50;
then (i -' (len x1)) + 1 > 0 + 1 by XREAL_1:6;
then A37: 1 <= i -' (len x1) by NAT_1:13;
then A38: i -' (len x1) in Seg (len y1) by A36;
then A39: i -' (len x1) in dom (mlt (y1,y2)) by A11, FINSEQ_1:def_3;
i = (len (mlt (x1,x2))) + (i -' (len x1)) by A17, A35, FINSEQ_1:def_3;
then A40: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (y1,y2)) . (i -' (len x1)) by A39, FINSEQ_1:def_7
.= (y1 /. (i -' (len x1))) * (y2 /. (i -' (len x1))) by A39, Th13 ;
i -' (len x1) in dom y1 by A38, FINSEQ_1:def_3;
then A41: (x1 ^ y1) . i = y1 . (i -' (len x1)) by A35, FINSEQ_1:def_7;
i -' (len x1) in Seg (len y1) by A37, A36;
then A42: i -' (len x1) in dom y2 by A2, FINSEQ_1:def_3;
( y1 /. (i -' (len x1)) = y1 . (i -' (len x1)) & y2 /. (i -' (len x1)) = y2 . (i -' (len x1)) ) by A2, A37, A36, FINSEQ_4:15;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A1, A35, A42, A41, A33, A32, A40, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A21, Th13; ::_thesis: verum
end;
len (mlt ((x1 ^ y1),(x2 ^ y2))) = len (x1 ^ y1) by A4, A7, FINSEQ_1:def_3
.= (len x1) + (len y1) by FINSEQ_1:22 ;
then len (mlt ((x1 ^ y1),(x2 ^ y2))) = (len (mlt (x1,x2))) + (len (mlt (y1,y2))) by A17, A12, FINSEQ_1:def_3;
then len (mlt ((x1 ^ y1),(x2 ^ y2))) = len ((mlt (x1,x2)) ^ (mlt (y1,y2))) by FINSEQ_1:22;
hence mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) by A18, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th15: :: MFOLD_2:15
for x1, x2, y1, y2 being FinSequence of REAL st len x1 = len x2 & len y1 = len y2 holds
|((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|
proof
let x1, x2, y1, y2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 & len y1 = len y2 implies |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| )
A1: Sum ((mlt (x1,x2)) ^ (mlt (y1,y2))) = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by RVSUM_1:75;
assume ( len x1 = len x2 & len y1 = len y2 ) ; ::_thesis: |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|
then Sum (mlt ((x1 ^ y1),(x2 ^ y2))) = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by A1, Th14;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by RVSUM_1:def_16;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + |(y1,y2)| by RVSUM_1:def_16;
hence |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| by RVSUM_1:def_16; ::_thesis: verum
end;
Lm1: for n being Nat holds the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n)
proof
let n be Nat; ::_thesis: the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n)
reconsider D = REAL as non empty set ;
A1: Funcs ((Seg n),D) = REAL n by FINSEQ_2:93;
RealVectSpace (Seg n) = RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def_6;
hence the carrier of (RealVectSpace (Seg n)) = the carrier of (TOP-REAL n) by A1, EUCLID:22; ::_thesis: verum
end;
Lm2: for n being Nat holds 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n)
proof
let n be Nat; ::_thesis: 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n)
RealVectSpace (Seg n) = RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def_6;
hence 0. (RealVectSpace (Seg n)) = (Seg n) --> 0 by FUNCSDOM:def_4
.= 0* n by FINSEQ_2:def_2
.= 0. (TOP-REAL n) by EUCLID:70 ;
::_thesis: verum
end;
theorem Th16: :: MFOLD_2:16
for k, n being Nat
for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds
(p1 + p2) . k = (p1 . k) + (p2 . k)
proof
let k, n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds
(p1 + p2) . k = (p1 . k) + (p2 . k)
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) )
A1: dom (p1 + p2) = Seg n by FINSEQ_1:89;
thus ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) ) by A1, VALUED_1:def_1; ::_thesis: verum
end;
theorem Th17: :: MFOLD_2:17
for n being Nat
for X being set holds
( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n )
proof
let n be Nat; ::_thesis: for X being set holds
( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n )
let X be set ; ::_thesis: ( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n )
set V = RealVectSpace (Seg n);
set T = TOP-REAL n;
hereby ::_thesis: ( X is Linear_Combination of TOP-REAL n implies X is Linear_Combination of RealVectSpace (Seg n) )
assume X is Linear_Combination of RealVectSpace (Seg n) ; ::_thesis: X is Linear_Combination of TOP-REAL n
then reconsider L = X as Linear_Combination of RealVectSpace (Seg n) ;
consider S being finite Subset of (RealVectSpace (Seg n)) such that
A1: for v being Element of (RealVectSpace (Seg n)) st not v in S holds
L . v = 0 by RLVECT_2:def_3;
A2: now__::_thesis:_for_v_being_Element_of_(TOP-REAL_n)_st_not_v_in_S_holds_
0_=_L_._v
let v be Element of (TOP-REAL n); ::_thesis: ( not v in S implies 0 = L . v )
assume A3: not v in S ; ::_thesis: 0 = L . v
v is Element of (RealVectSpace (Seg n)) by Lm1;
hence 0 = L . v by A1, A3; ::_thesis: verum
end;
( L is Element of Funcs ( the carrier of (TOP-REAL n),REAL) & S is finite Subset of (TOP-REAL n) ) by Lm1;
hence X is Linear_Combination of TOP-REAL n by A2, RLVECT_2:def_3; ::_thesis: verum
end;
assume X is Linear_Combination of TOP-REAL n ; ::_thesis: X is Linear_Combination of RealVectSpace (Seg n)
then reconsider L = X as Linear_Combination of TOP-REAL n ;
consider S being finite Subset of (TOP-REAL n) such that
A4: for v being Element of (TOP-REAL n) st not v in S holds
L . v = 0 by RLVECT_2:def_3;
A5: now__::_thesis:_for_v_being_Element_of_(RealVectSpace_(Seg_n))_st_not_v_in_S_holds_
0_=_L_._v
let v be Element of (RealVectSpace (Seg n)); ::_thesis: ( not v in S implies 0 = L . v )
assume A6: not v in S ; ::_thesis: 0 = L . v
v is Element of (TOP-REAL n) by Lm1;
hence 0 = L . v by A4, A6; ::_thesis: verum
end;
( L is Element of Funcs ( the carrier of (RealVectSpace (Seg n)),REAL) & S is finite Subset of (RealVectSpace (Seg n)) ) by Lm1;
hence X is Linear_Combination of RealVectSpace (Seg n) by A5, RLVECT_2:def_3; ::_thesis: verum
end;
theorem Th18: :: MFOLD_2:18
for n being Nat
for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (RealVectSpace (Seg n))
for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
proof
let n be Nat; ::_thesis: for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (RealVectSpace (Seg n))
for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let F be FinSequence of (TOP-REAL n); ::_thesis: for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (RealVectSpace (Seg n))
for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fr be Function of (TOP-REAL n),REAL; ::_thesis: for Fv being FinSequence of (RealVectSpace (Seg n))
for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let Fv be FinSequence of (RealVectSpace (Seg n)); ::_thesis: for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fv be Function of (RealVectSpace (Seg n)),REAL; ::_thesis: ( fr = fv & F = Fv implies fr (#) F = fv (#) Fv )
assume that
A1: fr = fv and
A2: F = Fv ; ::_thesis: fr (#) F = fv (#) Fv
A3: len (fv (#) Fv) = len Fv by RLVECT_2:def_7;
A4: len (fr (#) F) = len F by RLVECT_2:def_7;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_F_holds_
(fr_(#)_F)_._i_=_(fv_(#)_Fv)_._i
reconsider T = TOP-REAL n as RealLinearSpace ;
let i be Nat; ::_thesis: ( 1 <= i & i <= len F implies (fr (#) F) . i = (fv (#) Fv) . i )
reconsider Fi = F /. i as FinSequence of REAL by EUCLID:24;
A5: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proof
thus the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22 ; ::_thesis: verum
end;
the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102;
then reconsider Fvi = Fv /. i as Element of n -tuples_on the carrier of F_Real by Lm1, A5;
reconsider Fii = F /. i as Element of T ;
assume A6: ( 1 <= i & i <= len F ) ; ::_thesis: (fr (#) F) . i = (fv (#) Fv) . i
then A7: i in dom (fv (#) Fv) by A2, A3, FINSEQ_3:25;
i in dom F by A6, FINSEQ_3:25;
then A8: F /. i = F . i by PARTFUN1:def_6;
i in dom Fv by A2, A6, FINSEQ_3:25;
then A9: Fv /. i = Fv . i by PARTFUN1:def_6;
i in dom (fr (#) F) by A4, A6, FINSEQ_3:25;
hence (fr (#) F) . i = (fr . Fii) * Fii by RLVECT_2:def_7
.= (fv . (Fv /. i)) * (Fv /. i) by A1, A2, A8, A9, EUCLID:65
.= (fv (#) Fv) . i by A7, RLVECT_2:def_7 ;
::_thesis: verum
end;
hence fr (#) F = fv (#) Fv by A2, A4, A3, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th19: :: MFOLD_2:19
for n being Nat
for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv
proof
let n be Nat; ::_thesis: for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv
set T = TOP-REAL n;
set V = RealVectSpace (Seg n);
let F be FinSequence of (TOP-REAL n); ::_thesis: for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv
let Fv be FinSequence of (RealVectSpace (Seg n)); ::_thesis: ( Fv = F implies Sum F = Sum Fv )
assume A1: Fv = F ; ::_thesis: Sum F = Sum Fv
reconsider T = TOP-REAL n as RealLinearSpace ;
consider f being Function of NAT, the carrier of T such that
A2: Sum F = f . (len F) and
A3: f . 0 = 0. T and
A4: for j being Element of NAT
for v being Element of T st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def_12;
consider fv being Function of NAT, the carrier of (RealVectSpace (Seg n)) such that
A5: Sum Fv = fv . (len Fv) and
A6: fv . 0 = 0. (RealVectSpace (Seg n)) and
A7: for j being Element of NAT
for v being Element of (RealVectSpace (Seg n)) st j < len Fv & v = Fv . (j + 1) holds
fv . (j + 1) = (fv . j) + v by RLVECT_1:def_12;
defpred S1[ Nat] means ( $1 <= len F implies f . $1 = fv . $1 );
A8: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; ::_thesis: S1[i + 1]
set i1 = i + 1;
A10: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proof
thus the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22 ; ::_thesis: verum
end;
the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102;
then reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by A10, Lm1;
reconsider Fi1 = F /. (i + 1) as Element of T ;
assume A11: i + 1 <= len F ; ::_thesis: f . (i + 1) = fv . (i + 1)
then A12: i < len F by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then A13: i + 1 in dom F by A11, FINSEQ_3:25;
then F . (i + 1) = F /. (i + 1) by PARTFUN1:def_6;
then A14: f . (i + 1) = (f . i) + Fi1 by A4, A12;
A15: Fv /. (i + 1) = Fv . (i + 1) by A1, A13, PARTFUN1:def_6;
then Fvi1 = F /. (i + 1) by A1, A13, PARTFUN1:def_6;
hence f . (i + 1) = (fv . i) + (Fv /. (i + 1)) by A9, A11, A14, EUCLID:64, NAT_1:13
.= fv . (i + 1) by A1, A7, A12, A15 ;
::_thesis: verum
end;
A16: S1[ 0 ] by A3, A6, Lm2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A8);
hence Sum F = Sum Fv by A1, A2, A5; ::_thesis: verum
end;
theorem Th20: :: MFOLD_2:20
for n being Nat
for Lv being Linear_Combination of RealVectSpace (Seg n)
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
proof
let n be Nat; ::_thesis: for Lv being Linear_Combination of RealVectSpace (Seg n)
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
set V = RealVectSpace (Seg n);
set T = TOP-REAL n;
let Lv be Linear_Combination of RealVectSpace (Seg n); ::_thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
let Lr be Linear_Combination of TOP-REAL n; ::_thesis: ( Lr = Lv implies Sum Lr = Sum Lv )
assume A1: Lr = Lv ; ::_thesis: Sum Lr = Sum Lv
consider F being FinSequence of the carrier of (TOP-REAL n) such that
A2: ( F is one-to-one & rng F = Carrier Lr ) and
A3: Sum Lr = Sum (Lr (#) F) by RLVECT_2:def_8;
reconsider F1 = F as FinSequence of the carrier of (RealVectSpace (Seg n)) by Lm1;
A4: Lr (#) F = Lv (#) F1 by A1, Th18;
thus Sum Lv = Sum (Lv (#) F1) by A1, A2, RLVECT_2:def_8
.= Sum Lr by A3, A4, Th19 ; ::_thesis: verum
end;
theorem Th21: :: MFOLD_2:21
for n being Nat
for Af being Subset of (RealVectSpace (Seg n))
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
proof
let n be Nat; ::_thesis: for Af being Subset of (RealVectSpace (Seg n))
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
set V = RealVectSpace (Seg n);
let AV be Subset of (RealVectSpace (Seg n)); ::_thesis: for Ar being Subset of (TOP-REAL n) st AV = Ar holds
( AV is linearly-independent iff Ar is linearly-independent )
set T = TOP-REAL n;
let AR be Subset of (TOP-REAL n); ::_thesis: ( AV = AR implies ( AV is linearly-independent iff AR is linearly-independent ) )
assume A1: AV = AR ; ::_thesis: ( AV is linearly-independent iff AR is linearly-independent )
hereby ::_thesis: ( AR is linearly-independent implies AV is linearly-independent )
assume A2: AV is linearly-independent ; ::_thesis: AR is linearly-independent
now__::_thesis:_for_L_being_Linear_Combination_of_AR_st_Sum_L_=_0._(TOP-REAL_n)_holds_
Carrier_L_=_{}
let L be Linear_Combination of AR; ::_thesis: ( Sum L = 0. (TOP-REAL n) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of RealVectSpace (Seg n) by Th17;
assume Sum L = 0. (TOP-REAL n) ; ::_thesis: Carrier L = {}
then A3: 0. (RealVectSpace (Seg n)) = Sum L by Lm2
.= Sum L1 by Th20 ;
Carrier L c= AR by RLVECT_2:def_6;
then L1 is Linear_Combination of AV by A1, RLVECT_2:def_6;
hence Carrier L = {} by A2, A3, RLVECT_3:def_1; ::_thesis: verum
end;
hence AR is linearly-independent by RLVECT_3:def_1; ::_thesis: verum
end;
assume A4: AR is linearly-independent ; ::_thesis: AV is linearly-independent
now__::_thesis:_for_L_being_Linear_Combination_of_AV_st_Sum_L_=_0._(RealVectSpace_(Seg_n))_holds_
Carrier_L_=_{}
let L be Linear_Combination of AV; ::_thesis: ( Sum L = 0. (RealVectSpace (Seg n)) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th17;
Carrier L c= AV by RLVECT_2:def_6;
then reconsider L1 = L1 as Linear_Combination of AR by A1, RLVECT_2:def_6;
assume Sum L = 0. (RealVectSpace (Seg n)) ; ::_thesis: Carrier L = {}
then 0. (TOP-REAL n) = Sum L by Lm2
.= Sum L1 by Th20 ;
hence Carrier L = {} by A4, RLVECT_3:def_1; ::_thesis: verum
end;
hence AV is linearly-independent by RLVECT_3:def_1; ::_thesis: verum
end;
theorem Th22: :: MFOLD_2:22
for n being Nat
for p being Point of (TOP-REAL n)
for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l
let p be Point of (TOP-REAL n); ::_thesis: for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l
let V be Subset of (TOP-REAL n); ::_thesis: ( V = RN_Base n implies ex l being Linear_Combination of V st p = Sum l )
assume A1: V = RN_Base n ; ::_thesis: ex l being Linear_Combination of V st p = Sum l
reconsider p0 = p as Element of (RealVectSpace (Seg n)) by Lm1;
reconsider V0 = V as Subset of (RealVectSpace (Seg n)) by Lm1;
consider l0 being Linear_Combination of V0 such that
A2: p0 = Sum l0 by A1, EUCLID_7:43;
reconsider l = l0 as Linear_Combination of TOP-REAL n by Th17;
Carrier l0 c= V0 by RLVECT_2:def_6;
then reconsider l = l as Linear_Combination of V by RLVECT_2:def_6;
take l ; ::_thesis: p = Sum l
thus p = Sum l by A2, Th20; ::_thesis: verum
end;
theorem :: MFOLD_2:23
for n being Nat holds RN_Base n is Basis of TOP-REAL n
proof
let n be Nat; ::_thesis: RN_Base n is Basis of TOP-REAL n
set A = RN_Base n;
set T = TOP-REAL n;
RN_Base n c= REAL n ;
then A1: RN_Base n c= the carrier of (TOP-REAL n) by EUCLID:22;
reconsider A = RN_Base n as finite Subset of (TOP-REAL n) by EUCLID:22;
reconsider B = RN_Base n as Subset of (RealVectSpace (Seg n)) by A1, Lm1;
B is Basis of RealVectSpace (Seg n) by EUCLID_7:45;
then B is linearly-independent by RLVECT_3:def_3;
then A2: A is linearly-independent by Th21;
reconsider V1 = (Omega). (TOP-REAL n) as RealLinearSpace ;
for v being VECTOR of (TOP-REAL n) st v in Lin A holds
v in V1
proof
let v be VECTOR of (TOP-REAL n); ::_thesis: ( v in Lin A implies v in V1 )
assume v in Lin A ; ::_thesis: v in V1
v in RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by STRUCT_0:def_5;
hence v in V1 by RLSUB_1:def_4; ::_thesis: verum
end;
then reconsider X = Lin A as Subspace of V1 by RLSUB_1:29;
for x being set holds
( x in the carrier of X iff x in the carrier of V1 )
proof
let x be set ; ::_thesis: ( x in the carrier of X iff x in the carrier of V1 )
hereby ::_thesis: ( x in the carrier of V1 implies x in the carrier of X )
assume x in the carrier of X ; ::_thesis: x in the carrier of V1
then x in X by STRUCT_0:def_5;
then x in V1 by RLSUB_1:9;
hence x in the carrier of V1 by STRUCT_0:def_5; ::_thesis: verum
end;
assume x in the carrier of V1 ; ::_thesis: x in the carrier of X
then x in (Omega). (TOP-REAL n) by STRUCT_0:def_5;
then x in RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by RLSUB_1:def_4;
then reconsider x0 = x as Element of (TOP-REAL n) by STRUCT_0:def_5;
ex l being Linear_Combination of A st x0 = Sum l by Th22;
then x in { (Sum l) where l is Linear_Combination of A : verum } ;
hence x in the carrier of X by RLVECT_3:def_2; ::_thesis: verum
end;
then the carrier of X = the carrier of V1 by TARSKI:1;
then Lin A = (Omega). (TOP-REAL n) by EUCLID_7:9;
then Lin A = RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) by RLSUB_1:def_4;
hence RN_Base n is Basis of TOP-REAL n by A2, RLVECT_3:def_3; ::_thesis: verum
end;
theorem Th24: :: MFOLD_2:24
for n being Nat
for V being Subset of (TOP-REAL n) holds
( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being real number st
( r > 0 & Ball (p,r) c= V ) )
proof
let n be Nat; ::_thesis: for V being Subset of (TOP-REAL n) holds
( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being real number st
( r > 0 & Ball (p,r) c= V ) )
let V be Subset of (TOP-REAL n); ::_thesis: ( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being real number st
( r > 0 & Ball (p,r) c= V ) )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
set T = TOP-REAL n;
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
A2: TopSpaceMetr (Euclid n) = TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) by PCOMPS_1:def_5;
reconsider V1 = V as Subset of (Euclid n) by EUCLID:67;
hereby ::_thesis: ( ( for p being Point of (TOP-REAL n) st p in V holds
ex r being real number st
( r > 0 & Ball (p,r) c= V ) ) implies V in the topology of (TOP-REAL n) )
assume A3: V in the topology of (TOP-REAL n) ; ::_thesis: for p being Point of (TOP-REAL n) st p in V holds
ex r being real number st
( r > 0 & Ball (p,r) c= V )
let p be Point of (TOP-REAL n); ::_thesis: ( p in V implies ex r being real number st
( r > 0 & Ball (p,r) c= V ) )
assume A4: p in V ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= V )
reconsider x = p as Element of (Euclid n) by EUCLID:67;
consider r being Real such that
A5: ( r > 0 & Ball (x,r) c= V1 ) by A3, A4, A1, A2, PCOMPS_1:def_4;
reconsider r = r as real number ;
take r = r; ::_thesis: ( r > 0 & Ball (p,r) c= V )
thus r > 0 by A5; ::_thesis: Ball (p,r) c= V
reconsider x1 = x as Point of (Euclid n1) ;
reconsider p1 = p as Point of (TOP-REAL n1) ;
Ball (x1,r) = Ball (p1,r) by TOPREAL9:13;
hence Ball (p,r) c= V by A5; ::_thesis: verum
end;
assume A6: for p being Point of (TOP-REAL n) st p in V holds
ex r being real number st
( r > 0 & Ball (p,r) c= V ) ; ::_thesis: V in the topology of (TOP-REAL n)
for x being Element of (Euclid n) st x in V1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= V1 )
proof
let x be Element of (Euclid n); ::_thesis: ( x in V1 implies ex r being Real st
( r > 0 & Ball (x,r) c= V1 ) )
assume A7: x in V1 ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= V1 )
reconsider p = x as Point of (TOP-REAL n) by EUCLID:67;
consider r being real number such that
A8: ( r > 0 & Ball (p,r) c= V ) by A6, A7;
reconsider r = r as Real by XREAL_0:def_1;
take r ; ::_thesis: ( r > 0 & Ball (x,r) c= V1 )
thus r > 0 by A8; ::_thesis: Ball (x,r) c= V1
reconsider x1 = x as Point of (Euclid n1) ;
reconsider p1 = p as Point of (TOP-REAL n1) ;
Ball (x1,r) = Ball (p1,r) by TOPREAL9:13;
hence Ball (x,r) c= V1 by A8; ::_thesis: verum
end;
hence V in the topology of (TOP-REAL n) by A1, A2, PCOMPS_1:def_4; ::_thesis: verum
end;
definition
let n be Nat;
let p be Point of (TOP-REAL n);
func InnerProduct p -> Function of (TOP-REAL n),R^1 means :Def1: :: MFOLD_2:def 1
for q being Point of (TOP-REAL n) holds it . q = |(p,q)|;
existence
ex b1 being Function of (TOP-REAL n),R^1 st
for q being Point of (TOP-REAL n) holds b1 . q = |(p,q)|
proof
defpred S1[ set , set ] means ex q being Point of (TOP-REAL n) st
( q = $1 & $2 = |(p,q)| );
A1: for x being set st x in the carrier of (TOP-REAL n) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL n) implies ex y being set st S1[x,y] )
assume x in the carrier of (TOP-REAL n) ; ::_thesis: ex y being set st S1[x,y]
then reconsider q3 = x as Point of (TOP-REAL n) ;
take |(p,q3)| ; ::_thesis: S1[x,|(p,q3)|]
thus S1[x,|(p,q3)|] ; ::_thesis: verum
end;
consider f1 being Function such that
A2: ( dom f1 = the carrier of (TOP-REAL n) & ( for x being set st x in the carrier of (TOP-REAL n) holds
S1[x,f1 . x] ) ) from CLASSES1:sch_1(A1);
rng f1 c= the carrier of R^1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f1 or z in the carrier of R^1 )
assume z in rng f1 ; ::_thesis: z in the carrier of R^1
then consider xz being set such that
A3: xz in dom f1 and
A4: z = f1 . xz by FUNCT_1:def_3;
ex q4 being Point of (TOP-REAL n) st
( q4 = xz & f1 . xz = |(p,q4)| ) by A2, A3;
hence z in the carrier of R^1 by A4, TOPMETR:17; ::_thesis: verum
end;
then reconsider f2 = f1 as Function of (TOP-REAL n),R^1 by A2, FUNCT_2:def_1, RELSET_1:4;
take f2 ; ::_thesis: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)|
for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)|
proof
let q be Point of (TOP-REAL n); ::_thesis: f1 . q = |(p,q)|
ex q2 being Point of (TOP-REAL n) st
( q2 = q & f1 . q = |(p,q2)| ) by A2;
hence f1 . q = |(p,q)| ; ::_thesis: verum
end;
hence for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b1 . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds b2 . q = |(p,q)| ) holds
b1 = b2
proof
let f1, f2 be Function of (TOP-REAL n),R^1; ::_thesis: ( ( for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| ) & ( for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ) implies f1 = f2 )
assume that
A5: for q being Point of (TOP-REAL n) holds f1 . q = |(p,q)| and
A6: for q being Point of (TOP-REAL n) holds f2 . q = |(p,q)| ; ::_thesis: f1 = f2
for q being Point of (TOP-REAL n) holds f1 . q = f2 . q
proof
let q be Point of (TOP-REAL n); ::_thesis: f1 . q = f2 . q
thus f1 . q = |(p,q)| by A5
.= f2 . q by A6 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines InnerProduct MFOLD_2:def_1_:_
for n being Nat
for p being Point of (TOP-REAL n)
for b3 being Function of (TOP-REAL n),R^1 holds
( b3 = InnerProduct p iff for q being Point of (TOP-REAL n) holds b3 . q = |(p,q)| );
registration
let n be Nat;
let p be Point of (TOP-REAL n);
cluster InnerProduct p -> continuous ;
correctness
coherence
InnerProduct p is continuous ;
proof
set f = InnerProduct p;
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider f1 = InnerProduct p as Function of (TopSpaceMetr (Euclid n)),(TopSpaceMetr RealSpace) by TOPMETR:def_6;
percases ( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ;
supposeA2: p = 0. (TOP-REAL n) ; ::_thesis: InnerProduct p is continuous
A3: for q being Point of (TOP-REAL n) holds (InnerProduct p) . q = 0
proof
let q be Point of (TOP-REAL n); ::_thesis: (InnerProduct p) . q = 0
(InnerProduct p) . q = |(q,p)| by Def1;
hence (InnerProduct p) . q = 0 by A2, EUCLID_2:32; ::_thesis: verum
end;
consider g being Function of (TOP-REAL n),R^1 such that
A4: ( ( for p being Point of (TOP-REAL n) holds g . p = 0 ) & g is continuous ) by JGRAPH_2:20;
for x being set st x in the carrier of (TOP-REAL n) holds
(InnerProduct p) . x = g . x
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL n) implies (InnerProduct p) . x = g . x )
assume x in the carrier of (TOP-REAL n) ; ::_thesis: (InnerProduct p) . x = g . x
then reconsider q = x as Point of (TOP-REAL n) ;
thus (InnerProduct p) . x = (InnerProduct p) . q
.= 0 by A3
.= g . q by A4
.= g . x ; ::_thesis: verum
end;
hence InnerProduct p is continuous by A4, FUNCT_2:12; ::_thesis: verum
end;
suppose p <> 0. (TOP-REAL n) ; ::_thesis: InnerProduct p is continuous
then A5: |.p.| > 0 by EUCLID_2:44;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_for_r_being_real_number_
for_u_being_Element_of_(Euclid_n)
for_u1_being_Element_of_RealSpace_st_r_>_0_&_u1_=_f1_._u_holds_
ex_s_being_real_number_st_
(_s_>_0_&_(_for_w_being_Element_of_(Euclid_n)
for_w1_being_Element_of_RealSpace_st_w1_=_f1_._w_&_dist_(u,w)_<_s_holds_
dist_(u1,w1)_<_r_)_)
let r be real number ; ::_thesis: for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u be Element of (Euclid n); ::_thesis: for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
let u1 be Element of RealSpace; ::_thesis: ( r > 0 & u1 = f1 . u implies ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
assume that
A6: r > 0 and
A7: u1 = f1 . u ; ::_thesis: ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
set s1 = r / |.p.|;
for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r / |.p.| holds
dist (u1,w1) < r
proof
let w be Element of (Euclid n); ::_thesis: for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r / |.p.| holds
dist (u1,w1) < r
let w1 be Element of RealSpace; ::_thesis: ( w1 = f1 . w & dist (u,w) < r / |.p.| implies dist (u1,w1) < r )
assume that
A8: w1 = f1 . w and
A9: dist (u,w) < r / |.p.| ; ::_thesis: dist (u1,w1) < r
reconsider tu = u1, tw = w1 as Real by METRIC_1:def_13;
reconsider qw = w, qu = u as Point of (TOP-REAL n1) by TOPREAL3:8;
A10: dist (u1,w1) = the distance of RealSpace . (u1,w1) by METRIC_1:def_1
.= abs (tu - tw) by METRIC_1:def_12, METRIC_1:def_13 ;
A11: w1 = |(qw,p)| by Def1, A8;
abs (tu - tw) = abs (|(qu,p)| - |(qw,p)|) by Def1, A7, A11
.= abs |((qu - qw),p)| by EUCLID_2:24 ;
then A12: dist (u1,w1) <= |.(qu - qw).| * |.p.| by A10, EUCLID_2:51;
A13: (dist (u,w)) * |.p.| = |.(qu - qw).| * |.p.| by JGRAPH_1:28;
(dist (u,w)) * |.p.| < (r / |.p.|) * |.p.| by A9, A5, XREAL_1:68;
then (dist (u,w)) * |.p.| < r / (|.p.| / |.p.|) by XCMPLX_1:82;
then (dist (u,w)) * |.p.| < r / 1 by A5, XCMPLX_1:60;
hence dist (u1,w1) < r by A13, A12, XXREAL_0:2; ::_thesis: verum
end;
hence ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) by A5, A6; ::_thesis: verum
end;
then f1 is continuous by UNIFORM1:3;
hence InnerProduct p is continuous by A1, PRE_TOPC:32, TOPMETR:def_6; ::_thesis: verum
end;
end;
end;
end;
begin
definition
let n be Nat;
let p, q be Point of (TOP-REAL n);
func Plane (p,q) -> Subset of (TOP-REAL n) equals :: MFOLD_2:def 2
{ y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;
correctness
coherence
{ y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } is Subset of (TOP-REAL n);
proof
set X = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;
now__::_thesis:_for_x_being_set_st_x_in__{__y_where_y_is_Point_of_(TOP-REAL_n)_:_|(p,(y_-_q))|_=_0__}__holds_
x_in_the_carrier_of_(TOP-REAL_n)
let x be set ; ::_thesis: ( x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } implies x in the carrier of (TOP-REAL n) )
assume x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; ::_thesis: x in the carrier of (TOP-REAL n)
then consider y being Point of (TOP-REAL n) such that
A1: ( x = y & |(p,(y - q))| = 0 ) ;
thus x in the carrier of (TOP-REAL n) by A1; ::_thesis: verum
end;
hence { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } is Subset of (TOP-REAL n) by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines Plane MFOLD_2:def_2_:_
for n being Nat
for p, q being Point of (TOP-REAL n) holds Plane (p,q) = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;
theorem Th25: :: MFOLD_2:25
for n being Nat
for p1, p, p2 being Point of (TOP-REAL n) holds (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
proof
let n be Nat; ::_thesis: for p1, p, p2 being Point of (TOP-REAL n) holds (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
let p1, p, p2 be Point of (TOP-REAL n); ::_thesis: (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2))
A1: now__::_thesis:_for_y_being_set_st_y_in_(transl_(p1,(TOP-REAL_n)))_.:_(Plane_(p,p2))_holds_
y_in_Plane_(p,(p1_+_p2))
let y be set ; ::_thesis: ( y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) implies y in Plane (p,(p1 + p2)) )
assume y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) ; ::_thesis: y in Plane (p,(p1 + p2))
then consider x being set such that
A2: ( [x,y] in transl (p1,(TOP-REAL n)) & x in Plane (p,p2) ) by RELAT_1:def_13;
consider x1 being Point of (TOP-REAL n) such that
A3: ( x = x1 & |(p,(x1 - p2))| = 0 ) by A2;
A4: y = (transl (p1,(TOP-REAL n))) . x1 by A2, A3, FUNCT_1:1
.= p1 + x1 by RLTOPSP1:def_10 ;
( x in dom (transl (p1,(TOP-REAL n))) & y = (transl (p1,(TOP-REAL n))) . x ) by A2, FUNCT_1:1;
then y in rng (transl (p1,(TOP-REAL n))) by FUNCT_1:3;
then reconsider y1 = y as Point of (TOP-REAL n) ;
x1 - p2 = (x1 - p2) + (0. (TOP-REAL n)) by EUCLID:27
.= (x1 - p2) + (p1 + (- p1)) by EUCLID:36
.= (x1 + (- p2)) + (p1 + (- p1)) by EUCLID:41
.= ((x1 + (- p2)) + p1) + (- p1) by EUCLID:26
.= (y1 + (- p2)) + (- p1) by A4, EUCLID:26
.= (y1 - p2) + (- p1) by EUCLID:41
.= (y1 - p2) - p1 by EUCLID:41
.= y1 - (p1 + p2) by EUCLID:46 ;
hence y in Plane (p,(p1 + p2)) by A3; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_Plane_(p,(p1_+_p2))_holds_
y_in_(transl_(p1,(TOP-REAL_n)))_.:_(Plane_(p,p2))
let y be set ; ::_thesis: ( y in Plane (p,(p1 + p2)) implies y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) )
assume y in Plane (p,(p1 + p2)) ; ::_thesis: y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2))
then consider y1 being Point of (TOP-REAL n) such that
A5: ( y = y1 & |(p,(y1 - (p1 + p2)))| = 0 ) ;
set x = y1 - p1;
y1 - p1 in the carrier of (TOP-REAL n) ;
then A6: y1 - p1 in dom (transl (p1,(TOP-REAL n))) by FUNCT_2:def_1;
p1 + (y1 - p1) = y1 by EUCLID:48;
then (transl (p1,(TOP-REAL n))) . (y1 - p1) = y1 by RLTOPSP1:def_10;
then A7: [(y1 - p1),y1] in transl (p1,(TOP-REAL n)) by A6, FUNCT_1:1;
(y1 - p1) - p2 = y1 - (p1 + p2) by EUCLID:46;
then y1 - p1 in Plane (p,p2) by A5;
hence y in (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) by A5, A7, RELAT_1:def_13; ::_thesis: verum
end;
hence (transl (p1,(TOP-REAL n))) .: (Plane (p,p2)) = Plane (p,(p1 + p2)) by A1, TARSKI:1; ::_thesis: verum
end;
theorem Th26: :: MFOLD_2:26
for n being Nat
for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) implies ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) )
assume A1: p <> 0. (TOP-REAL n) ; ::_thesis: ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
A2: 0. (TOP-REAL n) = - (0. (TOP-REAL n1)) by JGRAPH_5:10
.= - (0. (TOP-REAL n)) ;
set V1 = Plane (p,(0. (TOP-REAL n)));
|(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32;
then |(p,((0. (TOP-REAL n)) - (0. (TOP-REAL n))))| = 0 by EUCLID:42;
then A3: 0. (TOP-REAL n) in Plane (p,(0. (TOP-REAL n))) ;
A4: for v, u being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) holds
v + u in Plane (p,(0. (TOP-REAL n)))
proof
let v, u be VECTOR of (TOP-REAL n); ::_thesis: ( v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) implies v + u in Plane (p,(0. (TOP-REAL n))) )
assume v in Plane (p,(0. (TOP-REAL n))) ; ::_thesis: ( not u in Plane (p,(0. (TOP-REAL n))) or v + u in Plane (p,(0. (TOP-REAL n))) )
then consider v1 being Point of (TOP-REAL n) such that
A5: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ;
assume u in Plane (p,(0. (TOP-REAL n))) ; ::_thesis: v + u in Plane (p,(0. (TOP-REAL n)))
then consider u1 being Point of (TOP-REAL n) such that
A6: ( u = u1 & |(p,(u1 - (0. (TOP-REAL n))))| = 0 ) ;
|(p,((v1 + u1) - (0. (TOP-REAL n))))| = |(p,(v1 + (u1 - (0. (TOP-REAL n)))))| by EUCLID:45
.= |(p,v1)| + |(p,(u1 - (0. (TOP-REAL n))))| by EUCLID_2:26
.= |(p,(v1 + (0. (TOP-REAL n))))| by A6, EUCLID:27
.= 0 by A5, A2, EUCLID:41 ;
hence v + u in Plane (p,(0. (TOP-REAL n))) by A5, A6; ::_thesis: verum
end;
for a being Real
for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds
a * v in Plane (p,(0. (TOP-REAL n)))
proof
let a be Real; ::_thesis: for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds
a * v in Plane (p,(0. (TOP-REAL n)))
let v be VECTOR of (TOP-REAL n); ::_thesis: ( v in Plane (p,(0. (TOP-REAL n))) implies a * v in Plane (p,(0. (TOP-REAL n))) )
assume v in Plane (p,(0. (TOP-REAL n))) ; ::_thesis: a * v in Plane (p,(0. (TOP-REAL n)))
then consider v1 being Point of (TOP-REAL n) such that
A7: ( v = v1 & |(p,(v1 - (0. (TOP-REAL n))))| = 0 ) ;
|(p,(a * (v1 - (0. (TOP-REAL n)))))| = a * 0 by A7, EUCLID_2:20;
then |(p,((a * v1) - (a * (0. (TOP-REAL n)))))| = 0 by EUCLID:49;
then |(p,((a * v1) - (0. (TOP-REAL n))))| = 0 by EUCLID:28;
hence a * v in Plane (p,(0. (TOP-REAL n))) by A7; ::_thesis: verum
end;
then Plane (p,(0. (TOP-REAL n))) is linearly-closed by A4, RLSUB_1:def_1;
then consider W being strict Subspace of TOP-REAL n such that
A8: Plane (p,(0. (TOP-REAL n))) = the carrier of W by A3, RLSUB_1:35;
set A1 = the Basis of W;
A9: ( the Basis of W is linearly-independent & the carrier of (Lin the Basis of W) = the carrier of W ) by RLVECT_3:def_3;
A10: [#] (Lin the Basis of W) = Plane (p,(0. (TOP-REAL n))) by A8, RLVECT_3:def_3;
reconsider A = the Basis of W as linearly-independent Subset of (TOP-REAL n) by A9, RLVECT_5:14;
take A ; ::_thesis: ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
reconsider A2 = {p} as linearly-independent Subset of (TOP-REAL n) by A1, RLVECT_3:8;
A11: dim (Lin A2) = card A2 by RLVECT_5:29
.= 1 by CARD_1:30 ;
for v being VECTOR of (TOP-REAL n) ex v1, v2 being VECTOR of (TOP-REAL n) st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
proof
let v be VECTOR of (TOP-REAL n); ::_thesis: ex v1, v2 being VECTOR of (TOP-REAL n) st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
set a = |(p,v)| / |(p,p)|;
set v2 = (|(p,v)| / |(p,p)|) * p;
set v1 = v - ((|(p,v)| / |(p,p)|) * p);
reconsider v1 = v - ((|(p,v)| / |(p,p)|) * p), v2 = (|(p,v)| / |(p,p)|) * p as VECTOR of (TOP-REAL n) ;
take v1 ; ::_thesis: ex v2 being VECTOR of (TOP-REAL n) st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
take v2 ; ::_thesis: ( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
A12: |(p,p)| > 0 by A1, EUCLID_2:43;
|(p,v1)| = |(p,v)| - |(p,v2)| by EUCLID_2:27
.= |(p,v)| - ((|(p,v)| / |(p,p)|) * |(p,p)|) by EUCLID_2:20
.= |(p,v)| - |(p,v)| by A12, XCMPLX_1:87
.= 0 ;
then |(p,(v1 + (0. (TOP-REAL n))))| = 0 by EUCLID:27;
then |(p,(v1 - (0. (TOP-REAL n))))| = 0 by A2, EUCLID:41;
then v1 in [#] (Lin the Basis of W) by A10;
then v1 in Lin the Basis of W by STRUCT_0:def_5;
hence v1 in Lin A by RLVECT_5:20; ::_thesis: ( v2 in Lin A2 & v = v1 + v2 )
thus v2 in Lin A2 by RLVECT_4:8; ::_thesis: v = v1 + v2
thus v = v1 + v2 by EUCLID:48; ::_thesis: verum
end;
then A13: RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) = (Lin A) + (Lin A2) by RLSUB_2:44;
(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)
proof
for v being VECTOR of (TOP-REAL n) holds
( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )
proof
let v be VECTOR of (TOP-REAL n); ::_thesis: ( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )
hereby ::_thesis: ( v in (0). (TOP-REAL n) implies v in (Lin A) /\ (Lin A2) )
assume v in (Lin A) /\ (Lin A2) ; ::_thesis: v in (0). (TOP-REAL n)
then A14: ( v in Lin A & v in Lin A2 ) by RLSUB_2:3;
then consider a being Real such that
A15: v = a * p by RLVECT_4:8;
Lin the Basis of W = Lin A by RLVECT_5:20;
then v in Plane (p,(0. (TOP-REAL n))) by A10, A14, STRUCT_0:def_5;
then consider y being Point of (TOP-REAL n) such that
A16: ( y = v & |(p,(y - (0. (TOP-REAL n))))| = 0 ) ;
|(p,(v + (- (0. (TOP-REAL n)))))| = 0 by A16, EUCLID:41;
then |(p,v)| = 0 by A2, EUCLID:27;
then A17: a * |(p,p)| = 0 by A15, EUCLID_2:20;
|(p,p)| > 0 by A1, EUCLID_2:43;
then a = 0 by A17;
then v = 0. (TOP-REAL n) by A15, EUCLID:29;
hence v in (0). (TOP-REAL n) by RLVECT_3:29; ::_thesis: verum
end;
assume v in (0). (TOP-REAL n) ; ::_thesis: v in (Lin A) /\ (Lin A2)
then v = 0. (TOP-REAL n) by RLVECT_3:29;
hence v in (Lin A) /\ (Lin A2) by RLSUB_1:17; ::_thesis: verum
end;
hence (Lin A) /\ (Lin A2) = (0). (TOP-REAL n) by RLSUB_1:31; ::_thesis: verum
end;
then TOP-REAL n is_the_direct_sum_of Lin A, Lin A2 by A13, RLSUB_2:def_4;
then dim (TOP-REAL n) = (dim (Lin A)) + (dim (Lin A2)) by RLVECT_5:37;
then n = (dim (Lin A)) + 1 by A11, RLAFFIN3:4;
hence card A = n - 1 by RLVECT_5:29; ::_thesis: [#] (Lin A) = Plane (p,(0. (TOP-REAL n)))
thus [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) by A10, RLVECT_5:20; ::_thesis: verum
end;
theorem Th27: :: MFOLD_2:27
for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) holds
ex R being Function of (TOP-REAL n),(TOP-REAL n) st
( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) )
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) holds
ex R being Function of (TOP-REAL n),(TOP-REAL n) st
( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) )
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 <> 0. (TOP-REAL n) & p2 <> 0. (TOP-REAL n) implies ex R being Function of (TOP-REAL n),(TOP-REAL n) st
( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) )
assume p1 <> 0. (TOP-REAL n) ; ::_thesis: ( not p2 <> 0. (TOP-REAL n) or ex R being Function of (TOP-REAL n),(TOP-REAL n) st
( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) )
then consider B1 being linearly-independent Subset of (TOP-REAL n) such that
A1: ( card B1 = n - 1 & [#] (Lin B1) = Plane (p1,(0. (TOP-REAL n))) ) by Th26;
assume p2 <> 0. (TOP-REAL n) ; ::_thesis: ex R being Function of (TOP-REAL n),(TOP-REAL n) st
( R is being_homeomorphism & R .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) )
then consider B2 being linearly-independent Subset of (TOP-REAL n) such that
A2: ( card B2 = n - 1 & [#] (Lin B2) = Plane (p2,(0. (TOP-REAL n))) ) by Th26;
consider M being Matrix of n,F_Real such that
A3: ( M is invertible & (Mx2Tran M) .: ([#] (Lin B1)) = [#] (Lin B2) ) by A1, A2, MATRTOP2:22;
reconsider M = M as invertible Matrix of n,F_Real by A3;
take Mx2Tran M ; ::_thesis: ( Mx2Tran M is being_homeomorphism & (Mx2Tran M) .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) )
thus ( Mx2Tran M is being_homeomorphism & (Mx2Tran M) .: (Plane (p1,(0. (TOP-REAL n)))) = Plane (p2,(0. (TOP-REAL n))) ) by A1, A2, A3; ::_thesis: verum
end;
definition
let n be Nat;
let p, q be Point of (TOP-REAL n);
func TPlane (p,q) -> non empty SubSpace of TOP-REAL n equals :: MFOLD_2:def 3
(TOP-REAL n) | (Plane (p,q));
correctness
coherence
(TOP-REAL n) | (Plane (p,q)) is non empty SubSpace of TOP-REAL n;
proof
|(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32;
then |(p,(q - q))| = 0 by EUCLID:42;
then q in Plane (p,q) ;
hence (TOP-REAL n) | (Plane (p,q)) is non empty SubSpace of TOP-REAL n ; ::_thesis: verum
end;
end;
:: deftheorem defines TPlane MFOLD_2:def_3_:_
for n being Nat
for p, q being Point of (TOP-REAL n) holds TPlane (p,q) = (TOP-REAL n) | (Plane (p,q));
theorem Th28: :: MFOLD_2:28
for n being Nat holds Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*>
proof
let n be Nat; ::_thesis: Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*>
set N = Base_FinSeq ((n + 1),(n + 1));
set p = 0. (TOP-REAL n);
set q = <*1*>;
A1: dom (Base_FinSeq ((n + 1),(n + 1))) = Seg (n + 1) by FINSEQ_1:89
.= Seg (n + (len <*1*>)) by FINSEQ_1:39
.= Seg ((len (0. (TOP-REAL n))) + (len <*1*>)) by CARD_1:def_7 ;
A2: for k being Nat st k in dom (0. (TOP-REAL n)) holds
(Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k
proof
let k be Nat; ::_thesis: ( k in dom (0. (TOP-REAL n)) implies (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k )
assume k in dom (0. (TOP-REAL n)) ; ::_thesis: (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k
then k in Seg n by FINSEQ_1:89;
then A3: ( 1 <= k & k <= n ) by FINSEQ_1:1;
0 + n <= 1 + n by XREAL_1:6;
then A4: k <= n + 1 by A3, XXREAL_0:2;
A5: n + 1 <> k by A3, NAT_1:13;
thus (Base_FinSeq ((n + 1),(n + 1))) . k = 0 by A4, A3, A5, MATRIXR2:76
.= (0* n) . k
.= (0. (TOP-REAL n)) . k by EUCLID:70 ; ::_thesis: verum
end;
for k being Nat st k in dom <*1*> holds
(Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k
proof
let k be Nat; ::_thesis: ( k in dom <*1*> implies (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k )
assume k in dom <*1*> ; ::_thesis: (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k
then k in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A6: k = 1 by TARSKI:def_1;
A7: 0 + 1 <= n + 1 by XREAL_1:6;
thus (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = (Base_FinSeq ((n + 1),(n + 1))) . (n + 1) by A6, CARD_1:def_7
.= 1 by A7, MATRIXR2:75
.= <*1*> . k by A6, FINSEQ_1:40 ; ::_thesis: verum
end;
hence Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*> by A1, A2, FINSEQ_1:def_7; ::_thesis: verum
end;
Lm3: for n being Nat
for p0 being Point of (TOP-REAL (n + 1)) st p0 = Base_FinSeq ((n + 1),(n + 1)) holds
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
proof
let n be Nat; ::_thesis: for p0 being Point of (TOP-REAL (n + 1)) st p0 = Base_FinSeq ((n + 1),(n + 1)) holds
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
let p0 be Point of (TOP-REAL (n + 1)); ::_thesis: ( p0 = Base_FinSeq ((n + 1),(n + 1)) implies TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic )
assume A1: p0 = Base_FinSeq ((n + 1),(n + 1)) ; ::_thesis: TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
set T = TOP-REAL n;
set S = TPlane (p0,(0. (TOP-REAL (n + 1))));
defpred S1[ set , set ] means for p being Element of (TOP-REAL n) st $1 = p holds
$2 = p ^ <*0*>;
A2: for p being Element of (TOP-REAL n) holds p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))
proof
let p be Element of (TOP-REAL n); ::_thesis: p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1)))))
A3: len p = n by CARD_1:def_7;
A4: len (p ^ <*0*>) = n + 1 by CARD_1:def_7;
rng (p ^ <*0*>) c= REAL ;
then p ^ <*0*> in REAL (n + 1) by A4, FINSEQ_2:132;
then reconsider q = p ^ <*0*> as Point of (TOP-REAL (n + 1)) by EUCLID:22;
reconsider r0 = 0 as Real by INT_1:3;
( dom p0 = Seg (n + 1) & dom q = Seg (n + 1) ) by FINSEQ_1:89;
then (dom p0) /\ (dom q) = Seg (n + 1) ;
then A5: dom (mlt (p0,q)) = Seg (n + 1) by VALUED_1:def_4;
for y being set holds
( y in rng (mlt (p0,q)) iff y = r0 )
proof
let y be set ; ::_thesis: ( y in rng (mlt (p0,q)) iff y = r0 )
set f = mlt (p0,q);
A6: now__::_thesis:_for_x_being_set_st_x_in_Seg_(n_+_1)_holds_
(mlt_(p0,q))_._x_=_r0
let x be set ; ::_thesis: ( x in Seg (n + 1) implies (mlt (p0,q)) . b1 = r0 )
assume x in Seg (n + 1) ; ::_thesis: (mlt (p0,q)) . b1 = r0
then consider k being Element of NAT such that
A7: ( x = k & 1 <= k & k <= n + 1 ) ;
A8: (mlt (p0,q)) . x = (p0 . x) * (q . x) by VALUED_1:5;
percases ( k = n + 1 or k <> n + 1 ) ;
supposeA9: k = n + 1 ; ::_thesis: (mlt (p0,q)) . b1 = r0
1 <= len <*r0*> by FINSEQ_1:39;
then q . ((len p) + 1) = <*r0*> . 1 by FINSEQ_1:65
.= r0 by FINSEQ_1:40 ;
hence (mlt (p0,q)) . x = r0 by A8, A7, A9, A3; ::_thesis: verum
end;
suppose k <> n + 1 ; ::_thesis: (mlt (p0,q)) . b1 = r0
then p0 . x = 0 by A1, A7, MATRIXR2:76;
hence (mlt (p0,q)) . x = r0 by A8; ::_thesis: verum
end;
end;
end;
hereby ::_thesis: ( y = r0 implies y in rng (mlt (p0,q)) )
assume y in rng (mlt (p0,q)) ; ::_thesis: y = r0
then consider x being set such that
A10: ( x in dom (mlt (p0,q)) & y = (mlt (p0,q)) . x ) by FUNCT_1:def_3;
thus y = r0 by A10, A5, A6; ::_thesis: verum
end;
assume A11: y = r0 ; ::_thesis: y in rng (mlt (p0,q))
consider x being set such that
A12: x in Seg (n + 1) by XBOOLE_0:def_1;
y = (mlt (p0,q)) . x by A11, A12, A6;
hence y in rng (mlt (p0,q)) by A12, A5, FUNCT_1:def_3; ::_thesis: verum
end;
then A13: rng (mlt (p0,q)) = {r0} by TARSKI:def_1;
mlt (p0,q) = (Seg (n + 1)) --> r0 by A13, A5, FUNCOP_1:9;
then A14: mlt (p0,q) = (n + 1) |-> r0 by FINSEQ_2:def_2;
A15: |(p0,q)| = Sum (mlt (p0,q)) by RVSUM_1:def_16
.= (n + 1) * r0 by A14, RVSUM_1:80
.= 0 ;
|(p0,(q - (0. (TOP-REAL (n + 1)))))| = |(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))| by EUCLID_2:27
.= |(p0,q)| - 0 by EUCLID_2:32
.= 0 by A15 ;
then p ^ <*0*> in Plane (p0,(0. (TOP-REAL (n + 1)))) ;
then p ^ <*0*> in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def_5;
hence p ^ <*0*> is Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; ::_thesis: verum
end;
A16: for x being Element of (TOP-REAL n) ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y]
proof
let x be Element of (TOP-REAL n); ::_thesis: ex y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) st S1[x,y]
set y = x ^ <*0*>;
reconsider y = x ^ <*0*> as Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A2;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider f being Function of (TOP-REAL n),(TPlane (p0,(0. (TOP-REAL (n + 1))))) such that
A17: for x being Element of (TOP-REAL n) holds S1[x,f . x] from FUNCT_2:sch_3(A16);
A18: dom f = [#] (TOP-REAL n) by FUNCT_2:def_1;
A19: for y being set holds
( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being set st
( x in dom f & y = f . x ) )
proof
let y be set ; ::_thesis: ( y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) iff ex x being set st
( x in dom f & y = f . x ) )
hereby ::_thesis: ( ex x being set st
( x in dom f & y = f . x ) implies y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) )
assume y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
then y in Plane (p0,(0. (TOP-REAL (n + 1)))) by PRE_TOPC:def_5;
then consider q being Point of (TOP-REAL (n + 1)) such that
A20: ( y = q & |(p0,(q - (0. (TOP-REAL (n + 1)))))| = 0 ) ;
A21: ( len q = n + 1 & rng q c= REAL ) by CARD_1:def_7;
then reconsider q1 = q as FinSequence of REAL by FINSEQ_1:def_4;
set p = q1 | n;
reconsider x = q1 | n as set ;
take x = x; ::_thesis: ( x in dom f & y = f . x )
0 + n <= 1 + n by XREAL_1:6;
then A22: len (q1 | n) = n by A21, FINSEQ_1:59;
A23: rng (q1 | n) c= REAL ;
A24: q1 | n in REAL n by A22, A23, FINSEQ_2:132;
hence x in dom f by A18, EUCLID:22; ::_thesis: y = f . x
reconsider x1 = x as Element of (TOP-REAL n) by A24, EUCLID:22;
S1[x1,f . x1] by A17;
then A25: f . x = (q1 | n) ^ <*0*> ;
A26: q = (q1 | n) ^ <*(q . (n + 1))*> by A21, FINSEQ_3:55;
A27: |(p0,(q - (0. (TOP-REAL (n + 1)))))| = |(p0,q)| - |(p0,(0. (TOP-REAL (n + 1))))| by EUCLID_2:27
.= |(p0,q)| - 0 by EUCLID_2:32
.= |(p0,q)| ;
reconsider f0 = 0. (TOP-REAL n) as FinSequence of REAL by EUCLID:24;
rng <*1*> c= REAL ;
then reconsider f1 = <*1*> as FinSequence of REAL by FINSEQ_1:def_4;
reconsider f3 = <*(q . (n + 1))*> as FinSequence of REAL ;
q1 | n in REAL n by A22, A23, FINSEQ_2:132;
then reconsider p1 = q1 | n as Point of (TOP-REAL n) by EUCLID:22;
A28: |((f0 ^ f1),((q1 | n) ^ f3))| = 0 by A1, A26, A27, A20, Th28;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
0. (TOP-REAL n) in the carrier of (TOP-REAL n) ;
then f0 in REAL n by EUCLID:22;
then f0 in Funcs ((Seg n1),REAL) by FINSEQ_2:93;
then consider g being Function such that
A29: ( f0 = g & dom g = Seg n1 & rng g c= REAL ) by FUNCT_2:def_2;
A30: len f0 = len (q1 | n) by A22, A29, FINSEQ_1:def_3;
len f1 = 1 by FINSEQ_1:39
.= len f3 by FINSEQ_1:39 ;
then |((0. (TOP-REAL n)),p1)| + |(f1,f3)| = 0 by A28, A30, Th15;
then 0 + |(f1,f3)| = 0 by EUCLID_2:33;
then Sum (mlt (f1,f3)) = 0 by RVSUM_1:def_16;
then Sum <*(1 * (q . (n + 1)))*> = 0 by RVSUM_1:62;
hence y = f . x by A20, A25, A26, RVSUM_1:73; ::_thesis: verum
end;
given x being set such that A31: ( x in dom f & y = f . x ) ; ::_thesis: y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))
reconsider p = x as Element of (TOP-REAL n) by A31;
S1[p,f . p] by A17;
hence y in [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A31; ::_thesis: verum
end;
then A32: rng f = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by FUNCT_1:def_3;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A33: ( x1 in dom f & x2 in dom f ) ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
assume A34: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Element of (TOP-REAL n) by A33;
( f . p1 = p1 ^ <*0*> & f . p2 = p2 ^ <*0*> ) by A17;
hence x1 = x2 by A34, FINSEQ_1:33; ::_thesis: verum
end;
then A35: f is one-to-one by FUNCT_1:def_4;
set T1 = TOP-REAL (n + 1);
A36: for p1 being Point of (TOP-REAL n) holds f . p1 is Point of (TOP-REAL (n + 1))
proof
let p1 be Point of (TOP-REAL n); ::_thesis: f . p1 is Point of (TOP-REAL (n + 1))
[#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) c= [#] (TOP-REAL (n + 1)) by PRE_TOPC:def_4;
hence f . p1 is Point of (TOP-REAL (n + 1)) by TARSKI:def_3; ::_thesis: verum
end;
A37: for p1 being Point of (TOP-REAL n)
for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds
|.p1.| = |.q1.|
proof
let p1 be Point of (TOP-REAL n); ::_thesis: for q1 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 holds
|.p1.| = |.q1.|
let q1 be Point of (TOP-REAL (n + 1)); ::_thesis: ( q1 = f . p1 implies |.p1.| = |.q1.| )
assume q1 = f . p1 ; ::_thesis: |.p1.| = |.q1.|
then A38: q1 = p1 ^ <*0*> by A17;
reconsider x = q1 as Element of REAL (n + 1) by EUCLID:22;
A39: ( len p1 = n & rng p1 c= REAL ) by CARD_1:def_7;
A40: x | n = (p1 ^ <*0*>) | (dom p1) by A38, FINSEQ_1:89
.= p1 by FINSEQ_1:21 ;
A41: x . (n + 1) = 0 by A38, A39, FINSEQ_1:42;
A42: |.q1.| ^2 = (|.p1.| ^2) + (0 ^2) by A40, A41, REAL_NS1:10
.= (|.p1.| ^2) + (0 * 0) by SQUARE_1:def_1
.= |.p1.| ^2 ;
|.q1.| * |.q1.| >= 0 ;
then A43: |.q1.| ^2 >= 0 by SQUARE_1:def_1;
|.p1.| * |.p1.| >= 0 ;
then |.p1.| ^2 >= 0 by SQUARE_1:def_1;
hence |.p1.| = sqrt (|.q1.| ^2) by A42, SQUARE_1:def_2
.= |.q1.| by A43, SQUARE_1:def_2 ;
::_thesis: verum
end;
A44: for p1, p2 being Point of (TOP-REAL n)
for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds
f . (p1 - p2) = q1 - q2
proof
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for q1, q2 being Point of (TOP-REAL (n + 1)) st q1 = f . p1 & q2 = f . p2 holds
f . (p1 - p2) = q1 - q2
let q1, q2 be Point of (TOP-REAL (n + 1)); ::_thesis: ( q1 = f . p1 & q2 = f . p2 implies f . (p1 - p2) = q1 - q2 )
assume q1 = f . p1 ; ::_thesis: ( not q2 = f . p2 or f . (p1 - p2) = q1 - q2 )
then A45: q1 = p1 ^ <*0*> by A17;
assume q2 = f . p2 ; ::_thesis: f . (p1 - p2) = q1 - q2
then A46: q2 = p2 ^ <*0*> by A17;
A47: f . (p1 - p2) = (p1 - p2) ^ <*0*> by A17;
reconsider qa = f . (p1 - p2) as Point of (TOP-REAL (n + 1)) by A36;
A48: dom ((p1 - p2) ^ <*0*>) = Seg (n + 1) by FINSEQ_1:89
.= dom (q1 - q2) by FINSEQ_1:89 ;
for k being Nat st k in dom (q1 - q2) holds
(q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k
proof
let k be Nat; ::_thesis: ( k in dom (q1 - q2) implies (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k )
assume k in dom (q1 - q2) ; ::_thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k
then A49: k in Seg (n + 1) by FINSEQ_1:89;
A50: (q1 - q2) . k = (q1 + (- q2)) . k by ALGSTR_0:def_14
.= (q1 . k) + ((- q2) . k) by A49, Th16
.= (q1 . k) + (((- 1) * q2) . k) by EUCLID:39
.= (q1 . k) + ((- 1) * (q2 . k)) by VALUED_1:6 ;
A51: k in (Seg n) \/ {(n + 1)} by A49, FINSEQ_1:9;
percases ( k in Seg n or k in {(n + 1)} ) by A51, XBOOLE_0:def_3;
supposeA52: k in Seg n ; ::_thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k
then ( k in dom p1 & k in dom p2 ) by FINSEQ_1:89;
then A53: ( q1 . k = p1 . k & q2 . k = p2 . k ) by A45, A46, FINSEQ_1:def_7;
k in dom (p1 - p2) by A52, FINSEQ_1:89;
then ((p1 - p2) ^ <*0*>) . k = (p1 - p2) . k by FINSEQ_1:def_7
.= (p1 + (- p2)) . k by ALGSTR_0:def_14
.= (p1 . k) + ((- p2) . k) by A52, Th16
.= (p1 . k) + (((- 1) * p2) . k) by EUCLID:39
.= (p1 . k) + ((- 1) * (p2 . k)) by VALUED_1:6 ;
hence (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k by A50, A53; ::_thesis: verum
end;
suppose k in {(n + 1)} ; ::_thesis: (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k
then A54: k = n + 1 by TARSKI:def_1;
( len p1 = n & len p2 = n ) by CARD_1:def_7;
then A55: ( q1 . k = 0 & q2 . k = 0 ) by A45, A46, A54, FINSEQ_1:42;
len (p1 - p2) = n by CARD_1:def_7;
hence (q1 - q2) . k = ((p1 - p2) ^ <*0*>) . k by A50, A55, A54, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence f . (p1 - p2) = q1 - q2 by A47, A48, FINSEQ_1:13; ::_thesis: verum
end;
A56: f .: ([#] (TOP-REAL n)) = [#] (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A32, RELSET_1:22;
for P being Subset of (TOP-REAL n) holds
( P is closed iff f .: P is closed )
proof
let P be Subset of (TOP-REAL n); ::_thesis: ( P is closed iff f .: P is closed )
hereby ::_thesis: ( f .: P is closed implies P is closed )
assume P is closed ; ::_thesis: f .: P is closed
then ([#] (TOP-REAL n)) \ P is open by PRE_TOPC:def_3;
then A57: ([#] (TOP-REAL n)) \ P in the topology of (TOP-REAL n) by PRE_TOPC:def_2;
set FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ;
for x being set st x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } holds
x in bool ([#] (TOP-REAL (n + 1)))
proof
let x be set ; ::_thesis: ( x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } implies x in bool ([#] (TOP-REAL (n + 1))) )
assume x in { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } ; ::_thesis: x in bool ([#] (TOP-REAL (n + 1)))
then consider q being Point of (TOP-REAL (n + 1)), r being Real such that
A58: ( x = Ball (q,r) & ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ;
thus x in bool ([#] (TOP-REAL (n + 1))) by A58; ::_thesis: verum
end;
then reconsider FQ = { (Ball (q,r)) where q is Point of (TOP-REAL (n + 1)), r is Real : ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) } as Subset-Family of (TOP-REAL (n + 1)) by TARSKI:def_3;
for Q being Subset of (TOP-REAL (n + 1)) st Q in FQ holds
Q is open
proof
let Q be Subset of (TOP-REAL (n + 1)); ::_thesis: ( Q in FQ implies Q is open )
assume Q in FQ ; ::_thesis: Q is open
then consider q being Point of (TOP-REAL (n + 1)), r being Real such that
A59: ( Q = Ball (q,r) & ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) ) ;
thus Q is open by A59; ::_thesis: verum
end;
then A60: FQ is open by TOPS_2:def_1;
set Q = union FQ;
union FQ is open by A60, TOPS_2:19;
then A61: union FQ in the topology of (TOP-REAL (n + 1)) by PRE_TOPC:def_2;
for y being Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))) holds
( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )
proof
let y be Element of (TPlane (p0,(0. (TOP-REAL (n + 1))))); ::_thesis: ( y in f .: (([#] (TOP-REAL n)) \ P) iff y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) )
hereby ::_thesis: ( y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) implies y in f .: (([#] (TOP-REAL n)) \ P) )
assume y in f .: (([#] (TOP-REAL n)) \ P) ; ::_thesis: y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1))))))
then consider x being set such that
A62: ( x in dom f & x in ([#] (TOP-REAL n)) \ P & y = f . x ) by FUNCT_1:def_6;
reconsider p = x as Point of (TOP-REAL n) by A62;
reconsider q = y as Point of (TOP-REAL (n + 1)) by A62, A36;
consider r being real number such that
A63: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A62, A57, Th24;
reconsider r = r as Real by XREAL_0:def_1;
A64: Ball (q,r) in FQ by A62, A63;
y in Ball (q,r) by A63, JORDAN:16;
then y in union FQ by A64, TARSKI:def_4;
hence y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by XBOOLE_0:def_4; ::_thesis: verum
end;
assume y in (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ; ::_thesis: y in f .: (([#] (TOP-REAL n)) \ P)
then y in union FQ by XBOOLE_0:def_4;
then consider Y being set such that
A65: ( y in Y & Y in FQ ) by TARSKI:def_4;
consider q being Point of (TOP-REAL (n + 1)), r being Real such that
A66: Y = Ball (q,r) and
A67: ex p being Point of (TOP-REAL n) st
( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A65;
consider p being Point of (TOP-REAL n) such that
A68: ( q = f . p & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) by A67;
consider x being set such that
A69: ( x in dom f & y = f . x ) by A19;
reconsider p1 = x as Point of (TOP-REAL n) by A69;
reconsider q1 = y as Point of (TOP-REAL (n + 1)) by A69, A36;
q1 in { qy where qy is Point of (TOP-REAL (n + 1)) : |.(qy - q).| < r } by A65, A66, TOPREAL9:def_1;
then consider qy being Point of (TOP-REAL (n + 1)) such that
A70: ( qy = q1 & |.(qy - q).| < r ) ;
f . (p1 - p) = q1 - q by A69, A68, A44;
then |.(p1 - p).| < r by A70, A37;
then p1 in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r } ;
then p1 in Ball (p,r) by TOPREAL9:def_1;
hence y in f .: (([#] (TOP-REAL n)) \ P) by A69, A68, FUNCT_1:def_6; ::_thesis: verum
end;
then A71: f .: (([#] (TOP-REAL n)) \ P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by SUBSET_1:3;
([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = (union FQ) /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by A71, A35, A56, FUNCT_1:64;
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by A61, PRE_TOPC:def_4;
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) is open by PRE_TOPC:def_2;
hence f .: P is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
assume f .: P is closed ; ::_thesis: P is closed
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) is open by PRE_TOPC:def_3;
then ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) in the topology of (TPlane (p0,(0. (TOP-REAL (n + 1))))) by PRE_TOPC:def_2;
then consider Q being Subset of (TOP-REAL (n + 1)) such that
A72: ( Q in the topology of (TOP-REAL (n + 1)) & ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) = Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) ) by PRE_TOPC:def_4;
for p being Point of (TOP-REAL n) st p in ([#] (TOP-REAL n)) \ P holds
ex r being real number st
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )
proof
let p be Point of (TOP-REAL n); ::_thesis: ( p in ([#] (TOP-REAL n)) \ P implies ex r being real number st
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P ) )
assume p in ([#] (TOP-REAL n)) \ P ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )
then f . p in f .: (([#] (TOP-REAL n)) \ P) by A18, FUNCT_1:def_6;
then A73: f . p in ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) \ (f .: P) by A56, A35, FUNCT_1:64;
reconsider q = f . p as Point of (TOP-REAL (n + 1)) by A36;
q in Q by A72, A73, XBOOLE_0:def_4;
then consider r being real number such that
A74: ( r > 0 & Ball (q,r) c= Q ) by A72, Th24;
take r ; ::_thesis: ( r > 0 & Ball (p,r) c= ([#] (TOP-REAL n)) \ P )
thus r > 0 by A74; ::_thesis: Ball (p,r) c= ([#] (TOP-REAL n)) \ P
for x being set st x in Ball (p,r) holds
x in ([#] (TOP-REAL n)) \ P
proof
let x be set ; ::_thesis: ( x in Ball (p,r) implies x in ([#] (TOP-REAL n)) \ P )
assume x in Ball (p,r) ; ::_thesis: x in ([#] (TOP-REAL n)) \ P
then x in { px where px is Point of (TOP-REAL n) : |.(px - p).| < r } by TOPREAL9:def_1;
then consider p1 being Point of (TOP-REAL n) such that
A75: ( x = p1 & |.(p1 - p).| < r ) ;
reconsider q1 = f . p1 as Point of (TOP-REAL (n + 1)) by A36;
f . (p1 - p) = q1 - q by A44;
then |.(q1 - q).| < r by A75, A37;
then q1 in { qx where qx is Point of (TOP-REAL (n + 1)) : |.(qx - q).| < r } ;
then q1 in Ball (q,r) by TOPREAL9:def_1;
then q1 in Q /\ ([#] (TPlane (p0,(0. (TOP-REAL (n + 1)))))) by A74, XBOOLE_0:def_4;
then not q1 in f .: P by A72, XBOOLE_0:def_5;
then not x in P by A18, A75, FUNCT_1:def_6;
hence x in ([#] (TOP-REAL n)) \ P by A75, XBOOLE_0:def_5; ::_thesis: verum
end;
hence Ball (p,r) c= ([#] (TOP-REAL n)) \ P by TARSKI:def_3; ::_thesis: verum
end;
then ([#] (TOP-REAL n)) \ P in the topology of (TOP-REAL n) by Th24;
then ([#] (TOP-REAL n)) \ P is open by PRE_TOPC:def_2;
hence P is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
then f is being_homeomorphism by A18, A32, A35, TOPS_2:58;
hence TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;
theorem Th29: :: MFOLD_2:29
for n being Nat
for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TOP-REAL n, TPlane (p,q) are_homeomorphic
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TOP-REAL n, TPlane (p,q) are_homeomorphic
set T1 = TOP-REAL (n + 1);
let p, q be Point of (TOP-REAL (n + 1)); ::_thesis: ( p <> 0. (TOP-REAL (n + 1)) implies TOP-REAL n, TPlane (p,q) are_homeomorphic )
assume A1: p <> 0. (TOP-REAL (n + 1)) ; ::_thesis: TOP-REAL n, TPlane (p,q) are_homeomorphic
reconsider p0 = Base_FinSeq ((n + 1),(n + 1)) as Point of (TOP-REAL (n + 1)) by EUCLID:22;
A2: p0 <> 0. (TOP-REAL (n + 1))
proof
assume A3: p0 = 0. (TOP-REAL (n + 1)) ; ::_thesis: contradiction
0 + 1 <= n + 1 by XREAL_1:6;
then |.p0.| = 1 by EUCLID_7:28;
hence contradiction by A3, EUCLID_2:39; ::_thesis: verum
end;
A4: TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by Lm3;
ex R being Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st
( R is being_homeomorphism & R .: (Plane (p0,(0. (TOP-REAL (n + 1))))) = Plane (p,(0. (TOP-REAL (n + 1)))) ) by A1, A2, Th27;
then Plane (p0,(0. (TOP-REAL (n + 1)))), Plane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by METRIZTS:3;
then TPlane (p0,(0. (TOP-REAL (n + 1)))), TPlane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by METRIZTS:def_1;
then A5: TOP-REAL n, TPlane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by A4, BORSUK_3:3;
(transl (q,(TOP-REAL (n + 1)))) .: (Plane (p,(0. (TOP-REAL (n + 1))))) = Plane (p,((0. (TOP-REAL (n + 1))) + q)) by Th25
.= Plane (p,q) by EUCLID:27 ;
then Plane (p,(0. (TOP-REAL (n + 1)))), Plane (p,q) are_homeomorphic by METRIZTS:3;
then (TOP-REAL (n + 1)) | (Plane (p,(0. (TOP-REAL (n + 1))))),(TOP-REAL (n + 1)) | (Plane (p,q)) are_homeomorphic by METRIZTS:def_1;
hence TOP-REAL n, TPlane (p,q) are_homeomorphic by A5, BORSUK_3:3; ::_thesis: verum
end;
theorem :: MFOLD_2:30
for n being Nat
for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TPlane (p,q) is n -manifold
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TPlane (p,q) is n -manifold
let p, q be Point of (TOP-REAL (n + 1)); ::_thesis: ( p <> 0. (TOP-REAL (n + 1)) implies TPlane (p,q) is n -manifold )
assume p <> 0. (TOP-REAL (n + 1)) ; ::_thesis: TPlane (p,q) is n -manifold
then TOP-REAL n, TPlane (p,q) are_homeomorphic by Th29;
hence TPlane (p,q) is n -manifold by Th12; ::_thesis: verum
end;
begin
definition
let n be Nat;
func TUnitSphere n -> TopSpace equals :: MFOLD_2:def 4
Tunit_circle (n + 1);
correctness
coherence
Tunit_circle (n + 1) is TopSpace;
;
end;
:: deftheorem defines TUnitSphere MFOLD_2:def_4_:_
for n being Nat holds TUnitSphere n = Tunit_circle (n + 1);
registration
let n be Nat;
cluster TUnitSphere n -> non empty ;
correctness
coherence
not TUnitSphere n is empty ;
;
end;
definition
let n be Nat;
let p be Point of (TOP-REAL n);
let S be SubSpace of TOP-REAL n;
assume A1: p in Sphere ((0. (TOP-REAL n)),1) ;
func stereographic_projection (S,p) -> Function of S,(TPlane (p,(0. (TOP-REAL n)))) means :Def5: :: MFOLD_2:def 5
for q being Point of (TOP-REAL n) st q in S holds
it . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));
existence
ex b1 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st
for q being Point of (TOP-REAL n) st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
proof
set T = TPlane (p,(0. (TOP-REAL n)));
defpred S1[ set , set ] means for q being Point of (TOP-REAL n) st q = $1 & q in S holds
$2 = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));
A2: for x being set st x in [#] S holds
ex y being set st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [#] S implies ex y being set st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,y] ) )
assume A3: x in [#] S ; ::_thesis: ex y being set st
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,y] )
[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider q = x as Point of (TOP-REAL n) by A3;
set y = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p));
take (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ; ::_thesis: ( (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) & S1[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))] )
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 A1, TOPREAL9:9;
then |.(p1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41;
then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39;
then |.(p1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28;
then |.p.| = 1 by EUCLID:27;
then |(p,p)| = 1 ^2 by EUCLID_2:4;
then A4: |(p,p)| = 1 * 1 by SQUARE_1:def_1;
A5: |(p,(|(q,p)| * p))| = |(q,p)| * |(p,p)| by EUCLID_2:20
.= |(p,q)| by A4 ;
|(p,((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))))| = (1 / (1 - |(q,p)|)) * |(p,(q - (|(q,p)| * p)))| by EUCLID_2:20
.= (1 / (1 - |(q,p)|)) * (|(p,q)| - |(p,(|(q,p)| * p))|) by EUCLID_2:27
.= 0 by A5 ;
then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + (0. (TOP-REAL n))))| = 0 by EUCLID:27;
then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + ((- 1) * (0. (TOP-REAL n)))))| = 0 by EUCLID:28;
then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) + (- (0. (TOP-REAL n)))))| = 0 by EUCLID:39;
then |(p,(((1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))) - (0. (TOP-REAL n))))| = 0 by EUCLID:41;
then (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in Plane (p,(0. (TOP-REAL n))) ;
hence (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) in [#] (TPlane (p,(0. (TOP-REAL n)))) by PRE_TOPC:def_5; ::_thesis: S1[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))]
thus S1[x,(1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))] ; ::_thesis: verum
end;
consider f being Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) such that
A6: for x being set st x in [#] S holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
reconsider f = f as Function of S,(TPlane (p,(0. (TOP-REAL n)))) ;
take f ; ::_thesis: for q being Point of (TOP-REAL n) st q in S holds
f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
let q be Point of (TOP-REAL n); ::_thesis: ( q in S implies f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) )
assume A7: q in S ; ::_thesis: f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p))
then q in [#] S by STRUCT_0:def_5;
hence f . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A6, A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) st ( for q being Point of (TOP-REAL n) st q in S holds
b1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds
b2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) holds
b1 = b2
proof
let f1, f2 be Function of S,(TPlane (p,(0. (TOP-REAL n)))); ::_thesis: ( ( for q being Point of (TOP-REAL n) st q in S holds
f1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds
f2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) implies f1 = f2 )
assume that
A8: for q being Point of (TOP-REAL n) st q in S holds
f1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) and
A9: for q being Point of (TOP-REAL n) st q in S holds
f2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ; ::_thesis: f1 = f2
for x being set st x in [#] S holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in [#] S implies f1 . x = f2 . x )
assume A10: x in [#] S ; ::_thesis: f1 . x = f2 . x
[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider q = x as Point of (TOP-REAL n) by A10;
A11: q in S by A10, STRUCT_0:def_5;
thus f1 . x = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A11, A8
.= f2 . x by A11, A9 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines stereographic_projection MFOLD_2:def_5_:_
for n being Nat
for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st p in Sphere ((0. (TOP-REAL n)),1) holds
for b4 being Function of S,(TPlane (p,(0. (TOP-REAL n)))) holds
( b4 = stereographic_projection (S,p) iff for q being Point of (TOP-REAL n) st q in S holds
b4 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) );
theorem Th31: :: MFOLD_2:31
for n being Nat
for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds
stereographic_projection (S,p) is being_homeomorphism
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds
stereographic_projection (S,p) is being_homeomorphism
let p be Point of (TOP-REAL n); ::_thesis: for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds
stereographic_projection (S,p) is being_homeomorphism
let S be SubSpace of TOP-REAL n; ::_thesis: ( [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) implies stereographic_projection (S,p) is being_homeomorphism )
assume A1: [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} ; ::_thesis: ( not p in Sphere ((0. (TOP-REAL n)),1) or stereographic_projection (S,p) is being_homeomorphism )
assume A2: p in Sphere ((0. (TOP-REAL n)),1) ; ::_thesis: stereographic_projection (S,p) is being_homeomorphism
set f = stereographic_projection (S,p);
set T = TPlane (p,(0. (TOP-REAL n)));
A3: dom (stereographic_projection (S,p)) = [#] 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 A2, TOPREAL9:9;
then |.(p1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41;
then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39;
then |.(p1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28;
then A4: |.p.| = 1 by EUCLID:27;
then |(p,p)| = 1 ^2 by EUCLID_2:4;
then A5: |(p,p)| = 1 * 1 by SQUARE_1:def_1;
defpred S1[ set , set ] means for q being Point of (TOP-REAL n) st q = $1 & q in TPlane (p,(0. (TOP-REAL n))) holds
$2 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));
A6: for x being set st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds
ex y being set st
( y in [#] S & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [#] (TPlane (p,(0. (TOP-REAL n)))) implies ex y being set st
( y in [#] S & S1[x,y] ) )
assume A7: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ; ::_thesis: ex y being set st
( y in [#] S & S1[x,y] )
[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider q = x as Point of (TOP-REAL n) 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. (TOP-REAL n))) by A7, PRE_TOPC:def_5;
then consider x1 being Point of (TOP-REAL n) such that
A8: ( x1 = q & |(p,(x1 - (0. (TOP-REAL n))))| = 0 ) ;
|(p,(q + (- (0. (TOP-REAL n)))))| = 0 by A8, EUCLID:41;
then |(p,(q + ((- 1) * (0. (TOP-REAL n)))))| = 0 by EUCLID:39;
then |(p,(q + (0. (TOP-REAL n))))| = 0 by EUCLID:28;
then A9: |(p,q)| = 0 by EUCLID:27;
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 A5, A12, TARSKI:def_1
.= ((|(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 A10, XCMPLX_1:60 ;
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 A14, EUCLID_2:25
.= (|(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 A16, A17
.= ((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 A10, XCMPLX_1:60
.= (|(q,q)| + 1) / (|(q,q)| + 1) by XCMPLX_1:99
.= 1 by A10, XCMPLX_1:60 ;
then |.((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))).| = 1 by EUCLID_2:5, SQUARE_1:18;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (0. (TOP-REAL n))).| = 1 by EUCLID:27;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by EUCLID:28;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (- (0. (TOP-REAL n)))).| = 1 by EUCLID:39;
then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) - (0. (TOP-REAL n))).| = 1 by EUCLID:41;
then y1 in Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:9;
hence (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S by A1, A11, XBOOLE_0:def_5; ::_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. (TOP-REAL n))))),([#] S) such that
A18: for x being set st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds
S1[x,g1 . x] from FUNCT_2:sch_1(A6);
reconsider g = g1 as Function of (TPlane (p,(0. (TOP-REAL n)))),S ;
reconsider f1 = stereographic_projection (S,p) as Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) ;
|.(0. (TOP-REAL n)).| <> |.p.| by A4, EUCLID_2:39;
then 0. (TOP-REAL n) <> (1 + 1) * p by EUCLID:31;
then 0. (TOP-REAL n) <> (1 * p) + (1 * p) by EUCLID:33;
then 0. (TOP-REAL n) <> (1 * p) + p by EUCLID:29;
then 0. (TOP-REAL n) <> p + p by EUCLID:29;
then p + (- p) <> p + p by EUCLID:36;
then A19: not - p in {p} by TARSKI:def_1;
|.(- p).| = 1 by A4, EUCLID:71;
then |.((- p) + (0. (TOP-REAL n))).| = 1 by EUCLID:27;
then |.((- p) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by EUCLID:28;
then |.((- p) + (- (0. (TOP-REAL n)))).| = 1 by EUCLID:39;
then |.((- p) - (0. (TOP-REAL n))).| = 1 by EUCLID:41;
then A20: - p in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;
then A21: [#] S <> {} by A1, A19, XBOOLE_0:def_5;
A22: for y, x being set holds
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )
proof
let y, x be set ; ::_thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )
hereby ::_thesis: ( x in [#] S & f1 . x = y implies ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) )
assume A23: y in [#] (TPlane (p,(0. (TOP-REAL n)))) ; ::_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 A23, A21, FUNCT_2:5; ::_thesis: f1 . x = y
[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qx = x as Point of (TOP-REAL n) by A25;
[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qy = y as Point of (TOP-REAL n) by A23;
qy in TPlane (p,(0. (TOP-REAL n))) by A23, STRUCT_0:def_5;
then A26: qx = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A23, A18, A24;
qx in S by A25, STRUCT_0:def_5;
then A27: (stereographic_projection (S,p)) . qx = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A2, Def5;
qy in Plane (p,(0. (TOP-REAL n))) by A23, PRE_TOPC:def_5;
then consider y1 being Point of (TOP-REAL n) such that
A28: ( y1 = qy & |(p,(y1 - (0. (TOP-REAL n))))| = 0 ) ;
|(p,(qy + (- (0. (TOP-REAL n)))))| = 0 by A28, EUCLID:41;
then |(p,(qy + ((- 1) * (0. (TOP-REAL n)))))| = 0 by EUCLID:39;
then |(p,(qy + (0. (TOP-REAL n))))| = 0 by EUCLID:28;
then A29: |(p,qy)| = 0 by EUCLID:27;
A30: |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| = (2 * |(qy,p)|) + ((|(qy,qy)| - 1) * |(p,p)|) by EUCLID_2:25
.= |(qy,qy)| - 1 by A5, A29 ;
A31: |(qx,p)| = (1 / (|(qy,qy)| + 1)) * |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| by A26, EUCLID_2:19
.= ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) * 1 by A30, XCMPLX_1:75 ;
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 A31, A32, XCMPLX_1:60
.= ((|(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 A33, XCMPLX_1:57;
A35: ((|(qy,qy)| + 1) / 2) * qx = (((|(qy,qy)| + 1) / 2) * (1 / (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A26, EUCLID:30
.= (((|(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 A32, XCMPLX_1:60
.= ((1 / 2) * (2 * qy)) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by EUCLID:32
.= (((1 / 2) * 2) * qy) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by EUCLID:30
.= (1 * qy) + (((1 / 2) * (|(qy,qy)| - 1)) * p) by EUCLID:30
.= qy + (((|(qy,qy)| - 1) / 2) * p) by EUCLID:29 ;
A36: ((|(qy,qy)| + 1) / 2) * |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) / 2) by A31, XCMPLX_1:85
.= 1 * ((|(qy,qy)| - 1) / 2) by A32, XCMPLX_1:60
.= (|(qy,qy)| - 1) / 2 ;
thus f1 . x = (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| + 1) / 2) * (|(qx,p)| * p)) by A27, A34, EUCLID:49
.= (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| - 1) / 2) * p) by A36, EUCLID:30
.= y by A35, EUCLID:48 ; ::_thesis: verum
end;
assume A37: x in [#] S ; ::_thesis: ( not f1 . x = y or ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) )
assume A38: f1 . x = y ; ::_thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x )
hence A39: y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A37, FUNCT_2:5; ::_thesis: g1 . y = x
[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qx = x as Point of (TOP-REAL n) by A37;
qx in S by A37, STRUCT_0:def_5;
then A40: y = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A38, A2, Def5;
then reconsider qy = y as Point of (TOP-REAL n) ;
A41: qy in TPlane (p,(0. (TOP-REAL n))) by A39, STRUCT_0:def_5;
A42: g1 . qy = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A41, A39, A18;
reconsider qx1 = qx as Point of (TOP-REAL n1) ;
qx1 in Sphere ((0. (TOP-REAL n)),1) by A37, A1, XBOOLE_0:def_5;
then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;
then |.(qx1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41;
then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39;
then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28;
then |.qx.| = 1 by EUCLID:27;
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 A43, EUCLID_2:20 ;
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 A45, A44 ;
|(qx,p)| <> 1
proof
assume A47: |(qx,p)| = 1 ; ::_thesis: contradiction
A48: not qx in {p} by A1, A37, XBOOLE_0:def_5;
|(qx,p)| - |(qx,qx)| = 0 by A43, A47;
then A49: |(qx,(p - qx))| = 0 by EUCLID_2:27;
|(p,p)| - |(qx,p)| = 0 by A5, A47;
then A50: |((p - qx),p)| = 0 by EUCLID_2:24;
|((p - qx),(p - qx))| = 0 - 0 by A49, A50, EUCLID_2:24;
then p - qx = 0. (TOP-REAL n) by EUCLID_2:41;
then p = qx by EUCLID:43;
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 A40, EUCLID_2:19
.= (1 / (1 - |(qx,p)|)) * ((1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))|) by A40, EUCLID_2:19
.= ((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 A53, A52, XCMPLX_1:60
.= ((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 A51, XCMPLX_1:60
.= (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 A53, A52, XCMPLX_1:60
.= ((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 A51, XCMPLX_1:60
.= ((2 * |(qx,p)|) * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;
A56: 1 / (|(qy,qy)| + 1) = (1 - |(qx,p)|) / 2 by A54, XCMPLX_1:57;
A57: (|(qy,qy)| - 1) / (|(qy,qy)| + 1) = (2 * |(qx,p)|) / ((1 - |(qx,p)|) * (2 / (1 - |(qx,p)|))) by A54, A55, XCMPLX_1:78
.= (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 A51, XCMPLX_1:60
.= |(qx,p)| ;
A58: (1 - |(qx,p)|) * qy = ((1 - |(qx,p)|) * (1 / (1 - |(qx,p)|))) * (qx - (|(qx,p)| * p)) by A40, EUCLID:30
.= (((1 - |(qx,p)|) * 1) / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by XCMPLX_1:74
.= 1 * (qx - (|(qx,p)| * p)) by A51, XCMPLX_1:60
.= qx - (|(qx,p)| * p) by EUCLID:29 ;
thus g1 . y = ((1 / (|(qy,qy)| + 1)) * (2 * qy)) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by A42, EUCLID:32
.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by EUCLID:30
.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + (((1 / (|(qy,qy)| + 1)) * (|(qy,qy)| - 1)) * p) by EUCLID:30
.= ((1 - |(qx,p)|) * qy) + (((1 * (|(qy,qy)| - 1)) / (|(qy,qy)| + 1)) * p) by A56, XCMPLX_1:74
.= qx - ((|(qx,p)| * p) - (|(qx,p)| * p)) by A57, A58, EUCLID:47
.= qx - (0. (TOP-REAL n)) by EUCLID:42
.= qx + (- (0. (TOP-REAL n))) by EUCLID:41
.= qx + ((- 1) * (0. (TOP-REAL n))) by EUCLID:39
.= qx + (0. (TOP-REAL n)) by EUCLID:28
.= x by EUCLID:27 ; ::_thesis: verum
end;
for y being set holds
( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being set st
( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) )
proof
let y be set ; ::_thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being set st
( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) )
hereby ::_thesis: ( ex x being set st
( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) implies y in [#] (TPlane (p,(0. (TOP-REAL n)))) )
assume A59: y in [#] (TPlane (p,(0. (TOP-REAL n)))) ; ::_thesis: ex x being set st
( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )
set x = g . y;
take x = g . y; ::_thesis: ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )
thus x in dom (stereographic_projection (S,p)) by A22, A3, A59; ::_thesis: y = (stereographic_projection (S,p)) . x
thus y = (stereographic_projection (S,p)) . x by A59, A22; ::_thesis: verum
end;
given x being set such that A60: ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) ; ::_thesis: y in [#] (TPlane (p,(0. (TOP-REAL n))))
thus y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A60, FUNCT_2:5; ::_thesis: verum
end;
then A61: rng (stereographic_projection (S,p)) = [#] (TPlane (p,(0. (TOP-REAL n)))) by FUNCT_1:def_3;
A62: stereographic_projection (S,p) is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (stereographic_projection (S,p)) or not x2 in dom (stereographic_projection (S,p)) or not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 )
assume A63: ( x1 in dom (stereographic_projection (S,p)) & x2 in dom (stereographic_projection (S,p)) ) ; ::_thesis: ( not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 )
assume A64: (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 ; ::_thesis: x1 = x2
( g1 . ((stereographic_projection (S,p)) . x1) = x1 & g1 . ((stereographic_projection (S,p)) . x2) = x2 ) by A63, A22;
hence x1 = x2 by A64; ::_thesis: verum
end;
A65: stereographic_projection (S,p) is continuous
proof
A66: [#] S c= [#] (TOP-REAL n) 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 (TOP-REAL n) holds f1 . q = 1 ) & f1 is continuous ) by JGRAPH_2:20;
consider f2 being Function of (TOP-REAL n),R^1 such that
A68: ( ( for q being Point of (TOP-REAL n)
for r1, r2 being real number st f1 . q = r1 & (InnerProduct p) . q = r2 holds
f2 . q = r1 - r2 ) & f2 is continuous ) by A67, JGRAPH_2:21;
reconsider f2 = f2 as continuous Function of (TOP-REAL n),R^1 by A68;
reconsider S1 = S as non empty TopSpace by A20, A1, A19, XBOOLE_0:def_5;
set f3 = f2 | S1;
A69: for q being Point of (TOP-REAL n) st q in S1 holds
(f2 | S1) . q = 1 - |(q,p)|
proof
let q be Point of (TOP-REAL n); ::_thesis: ( q in S1 implies (f2 | S1) . q = 1 - |(q,p)| )
assume q in S1 ; ::_thesis: (f2 | S1) . q = 1 - |(q,p)|
then A70: q in the carrier of S1 by STRUCT_0:def_5;
A71: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
( (InnerProduct p) . q = |(q,p)| & f1 . q = 1 ) by Def1, A67;
then A72: f2 . q = 1 - |(q,p)| by A68;
thus (f2 | S1) . q = (f2 | the carrier of S1) . q by A71, TMAP_1:def_3
.= 1 - |(q,p)| by A72, A70, FUNCT_1:49 ; ::_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
q in [#] S ;
then reconsider qx = q as Point of (TOP-REAL n) by A66;
reconsider qx1 = qx as Point of (TOP-REAL n1) ;
qx1 in Sphere ((0. (TOP-REAL n)),1) by A1, XBOOLE_0:def_5;
then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;
then |.(qx1 + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:41;
then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:39;
then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by EUCLID:28;
then |.qx.| = 1 by EUCLID:27;
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 A1, XBOOLE_0:def_5;
|(qx,p)| - |(qx,qx)| = 0 by A74, A75;
then A77: |(qx,(p - qx))| = 0 by EUCLID_2:27;
|(p,p)| - |(qx,p)| = 0 by A5, A75;
then A78: |((p - qx),p)| = 0 by EUCLID_2:24;
|((p - qx),(p - qx))| = 0 - 0 by A77, A78, EUCLID_2:24;
then p - qx = 0. (TOP-REAL n) by EUCLID_2:41;
then p = qx by EUCLID:43;
hence contradiction by A76, TARSKI:def_1; ::_thesis: verum
end;
then A79: 1 - |(qx,p)| <> 0 ;
qx in S1 by STRUCT_0:def_5;
hence (f2 | S1) . q <> 0 by A69, A79; ::_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 number 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 (TOP-REAL n)
for r being real number st a = b & f4 . a = r holds
f5 . b = r * b ) & f5 is continuous ) by A80, MFOLD_1:2;
set f6 = (InnerProduct p) | S1;
A82: for q being Point of (TOP-REAL n) st q in S1 holds
((InnerProduct p) | S1) . q = |(q,p)|
proof
let q be Point of (TOP-REAL n); ::_thesis: ( q in S1 implies ((InnerProduct p) | S1) . q = |(q,p)| )
assume q in S1 ; ::_thesis: ((InnerProduct p) | S1) . q = |(q,p)|
then A83: q in the carrier of S1 by STRUCT_0:def_5;
A84: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
A85: (InnerProduct p) . q = |(q,p)| by Def1;
thus ((InnerProduct p) | S1) . q = ((InnerProduct p) | the carrier of S1) . q by A84, TMAP_1:def_3
.= |(q,p)| by A85, A83, FUNCT_1:49 ; ::_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 number st ((InnerProduct p) | S1) . q = r1 & (f2 | S1) . q = r2 holds
f7 . q = r1 / r2 ) & f7 is continuous ) by A73, JGRAPH_2:27;
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 A86, JGRAPH_6:9;
consider f9 being Function of S,(TOP-REAL n) such that
A88: ( ( for r being Point of S1 holds f9 . r = (f5 . r) + (f8 . r) ) & f9 is continuous ) by A87, A81, JGRAPH_6:12;
A89: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def_1
.= dom f9 by FUNCT_2:def_1 ;
for x being set st x in dom (stereographic_projection (S,p)) holds
(stereographic_projection (S,p)) . x = f9 . x
proof
let x be set ; ::_thesis: ( x in dom (stereographic_projection (S,p)) implies (stereographic_projection (S,p)) . x = f9 . x )
assume A90: x in dom (stereographic_projection (S,p)) ; ::_thesis: (stereographic_projection (S,p)) . x = f9 . x
then x in [#] S ;
then reconsider qx = x as Point of (TOP-REAL n) by A66;
A91: qx in S by A90, STRUCT_0:def_5;
reconsider r = qx as Point of S1 by A90;
A92: (f2 | S1) . r = 1 - |(qx,p)| by A69, A91;
A93: f4 . r = 1 / (1 - |(qx,p)|) by A92, A80;
A94: ((InnerProduct p) | S1) . r = |(qx,p)| by A82, A91;
A95: f8 . r = (f7 . r) * (- p) by A87
.= (|(qx,p)| / (1 - |(qx,p)|)) * (- p) by A92, A94, A86 ;
f9 . x = (f5 . r) + (f8 . r) by A88
.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 * |(qx,p)|) / (1 - |(qx,p)|)) * (- p)) by A93, A81, A95
.= ((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 EUCLID:30
.= (1 / (1 - |(qx,p)|)) * (qx + (|(qx,p)| * (- p))) by EUCLID:32
.= (1 / (1 - |(qx,p)|)) * (qx + (- (|(qx,p)| * p))) by EUCLID:40
.= (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by EUCLID:41 ;
hence (stereographic_projection (S,p)) . x = f9 . x by A91, A2, Def5; ::_thesis: verum
end;
hence stereographic_projection (S,p) is continuous by A88, A89, FUNCT_1:2, PRE_TOPC:27; ::_thesis: verum
end;
A96: g is continuous
proof
A97: for q being Point of (TOP-REAL n) st q in TPlane (p,(0. (TOP-REAL n))) holds
g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))
proof
let q be Point of (TOP-REAL n); ::_thesis: ( q in TPlane (p,(0. (TOP-REAL n))) implies g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) )
assume A98: q in TPlane (p,(0. (TOP-REAL n))) ; ::_thesis: g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))
then q in [#] (TPlane (p,(0. (TOP-REAL n)))) by STRUCT_0:def_5;
hence g . q = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) by A18, A98; ::_thesis: verum
end;
consider g0 being Function of (TOP-REAL n1),R^1 such that
A99: ( ( for q being Point of (TOP-REAL n1) holds g0 . q = |.q.| ) & g0 is continuous ) by JORDAN2C:84;
consider g1 being Function of (TOP-REAL n),R^1 such that
A100: ( ( for q being Point of (TOP-REAL n)
for r1 being real number st g0 . q = r1 holds
g1 . q = r1 * r1 ) & g1 is continuous ) by A99, JGRAPH_2:22;
consider g2 being Function of (TOP-REAL n),R^1 such that
A101: ( ( for q being Point of (TOP-REAL n)
for r1 being real number st g1 . q = r1 holds
g2 . q = r1 + 1 ) & g2 is continuous ) by A100, JGRAPH_2:24;
consider g3 being Function of (TOP-REAL n),R^1 such that
A102: ( ( for q being Point of (TOP-REAL n)
for r1 being real number st g1 . q = r1 holds
g3 . q = r1 + (- 1) ) & g3 is continuous ) by A100, JGRAPH_2:24;
consider g4 being Function of (TOP-REAL n),R^1 such that
A103: ( ( for q being Point of (TOP-REAL n) holds g4 . q = 2 ) & g4 is continuous ) by JGRAPH_2:20;
A104: for q being Point of (TOP-REAL n) holds g2 . q <> 0
proof
let q be Point of (TOP-REAL n); ::_thesis: g2 . q <> 0
g0 . q = |.q.| by A99;
then g1 . q = |.q.| * |.q.| by A100;
then g2 . q = (|.q.| * |.q.|) + 1 by A101;
hence g2 . q <> 0 ; ::_thesis: verum
end;
then consider g5 being Function of (TOP-REAL n),R^1 such that
A105: ( ( for q being Point of (TOP-REAL n)
for r1, r2 being real number st g4 . q = r1 & g2 . q = r2 holds
g5 . q = r1 / r2 ) & g5 is continuous ) by A103, A101, JGRAPH_2:27;
reconsider g6 = g5 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A105;
consider g7 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that
A106: ( ( for a being Point of (TPlane (p,(0. (TOP-REAL n))))
for b being Point of (TOP-REAL n)
for r being real number st a = b & g6 . a = r holds
g7 . b = r * b ) & g7 is continuous ) by MFOLD_1:2;
consider g8 being Function of (TOP-REAL n),R^1 such that
A107: ( ( for q being Point of (TOP-REAL n)
for r1, r2 being real number st g3 . q = r1 & g2 . q = r2 holds
g8 . q = r1 / r2 ) & g8 is continuous ) by A104, A101, A102, JGRAPH_2:27;
reconsider p1 = p as Point of (TOP-REAL n1) ;
reconsider g9 = g8 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A107;
consider g10 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that
A108: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g10 . r = (g9 . r) * p1 ) & g10 is continuous ) by JGRAPH_6:9;
consider g11 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that
A109: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g11 . r = (g7 . r) + (g10 . r) ) & g11 is continuous ) by A106, A108, JGRAPH_6:12;
A110: dom g = [#] (TPlane (p,(0. (TOP-REAL n)))) by A21, FUNCT_2:def_1
.= dom g11 by FUNCT_2:def_1 ;
for x being set st x in dom g holds
g . x = g11 . x
proof
let x be set ; ::_thesis: ( x in dom g implies g . x = g11 . x )
assume A111: x in dom g ; ::_thesis: g . x = g11 . x
then A112: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ;
[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qx = x as Point of (TOP-REAL n) by A112;
A113: qx in TPlane (p,(0. (TOP-REAL n))) by A111, STRUCT_0:def_5;
reconsider r = qx as Point of (TPlane (p,(0. (TOP-REAL n)))) by A111;
A114: [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
A115: g0 . qx = |.qx.| by A99;
A116: g1 . qx = |.qx.| * |.qx.| by A100, A115
.= |.qx.| ^2 by SQUARE_1:def_1
.= |(qx,qx)| by EUCLID_2:4 ;
A117: g2 . qx = |(qx,qx)| + 1 by A101, A116;
A118: g4 . qx = 2 by A103;
A119: g6 . qx = (g5 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A114, TMAP_1:def_3
.= g5 . qx by A111, FUNCT_1:49
.= 2 / (|(qx,qx)| + 1) by A105, A118, A117 ;
A120: g3 . qx = |(qx,qx)| + (- 1) by A102, A116;
A121: g9 . qx = (g8 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A114, TMAP_1:def_3
.= g8 . qx by A111, FUNCT_1:49
.= (|(qx,qx)| - 1) / (|(qx,qx)| + 1) by A117, A120, A107 ;
A122: g7 . r = (2 / (|(qx,qx)| + 1)) * qx by A106, A119;
g11 . x = (g7 . r) + (g10 . r) by A109
.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 * (|(qx,qx)| - 1)) / (|(qx,qx)| + 1)) * p) by A121, A108, A122
.= (((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 EUCLID:30
.= ((1 / (|(qx,qx)| + 1)) * (2 * qx)) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by EUCLID:30
.= (1 / (|(qx,qx)| + 1)) * ((2 * qx) + ((|(qx,qx)| - 1) * p)) by EUCLID:32 ;
hence g . x = g11 . x by A97, A113; ::_thesis: verum
end;
hence g is continuous by A109, A110, FUNCT_1:2, PRE_TOPC:27; ::_thesis: verum
end;
reconsider f2 = f1 as [#] (TPlane (p,(0. (TOP-REAL n)))) -valued Relation ;
f2 is onto by A61, FUNCT_2:def_3;
then A123: f1 " = f1 " by A62, TOPS_2:def_4;
g1 = f1 " by A61, A62, A22, A21, FUNCT_2:28;
hence stereographic_projection (S,p) is being_homeomorphism by A3, A61, A62, A65, A96, A123, TOPS_2:def_5; ::_thesis: verum
end;
registration
let n be Nat;
cluster TUnitSphere n -> second-countable ;
correctness
coherence
TUnitSphere n is second-countable ;
proof
(TOP-REAL (n + 1)) | (Sphere ((0. (TOP-REAL (n + 1))),1)) is second-countable ;
then Tcircle ((0. (TOP-REAL (n + 1))),1) is second-countable by TOPREALB:def_6;
hence TUnitSphere n is second-countable by TOPREALB:def_7; ::_thesis: verum
end;
cluster TUnitSphere n -> n -locally_euclidean ;
correctness
coherence
TUnitSphere n is n -locally_euclidean ;
proof
set M = TUnitSphere n;
for p being Point of (TUnitSphere n) ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
proof
let p be Point of (TUnitSphere n); ::_thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
reconsider n1 = n + 1 as Element of NAT ;
A1: p in the carrier of (Tunit_circle (n + 1)) ;
[#] (Tunit_circle (n + 1)) c= [#] (TOP-REAL (n + 1)) by PRE_TOPC:def_4;
then reconsider p1 = p as Point of (TOP-REAL n1) by A1;
A2: |.p1.| = 1 by TOPREALB:12;
A3: |.(- p1).| = sqrt |((- p1),(- p1))| by EUCLID_2:37
.= sqrt |(p1,p1)| by EUCLID_2:23
.= 1 by A2, EUCLID_2:37 ;
then |.((- p1) + (0. (TOP-REAL n1))).| = 1 by EUCLID:27;
then |.((- p1) + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by EUCLID:28;
then |.((- p1) + (- (0. (TOP-REAL n1)))).| = 1 by EUCLID:39;
then |.((- p1) - (0. (TOP-REAL n1))).| = 1 by EUCLID:41;
then A4: - p1 in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;
then - p1 in [#] ((TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1))) by PRE_TOPC:def_5;
then - p1 in the carrier of (Tcircle ((0. (TOP-REAL n1)),1)) by TOPREALB:def_6;
then - p1 in the carrier of (Tunit_circle n1) by TOPREALB:def_7;
then reconsider A = {(- p1)} as Subset of (TUnitSphere n) by ZFMISC_1:31;
reconsider U1 = ([#] (TUnitSphere n)) \ A as Subset of (TUnitSphere n) ;
|.(0. (TOP-REAL n1)).| <> |.(- p1).| by A3, EUCLID_2:39;
then 0. (TOP-REAL n1) <> (1 + 1) * (- p1) by EUCLID:31;
then 0. (TOP-REAL n1) <> (1 * (- p1)) + (1 * (- p1)) by EUCLID:33;
then 0. (TOP-REAL n1) <> (1 * (- p1)) + (- p1) by EUCLID:29;
then 0. (TOP-REAL n1) <> (- p1) + (- p1) by EUCLID:29;
then (- p1) + (- (- p1)) <> (- p1) + (- p1) by EUCLID:36;
then A5: not p1 in {(- p1)} by TARSKI:def_1;
then p1 in U1 by XBOOLE_0:def_5;
then reconsider U = U1 as a_neighborhood of p by CONNSP_2:3, FRECHET:4;
take U ; ::_thesis: U, [#] (TOP-REAL n) are_homeomorphic
reconsider m = n + 1 as Nat ;
A6: TUnitSphere n = Tcircle ((0. (TOP-REAL m)),1) by TOPREALB:def_7
.= (TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)) by TOPREALB:def_6 ;
reconsider S = Sphere ((0. (TOP-REAL m)),1) as Subset of (TOP-REAL m) ;
reconsider U11 = U1 as Subset of ((TOP-REAL m) | S) by A6;
U1 c= [#] (Tunit_circle m) ;
then A7: U1 c= Sphere ((0. (TOP-REAL m)),1) by A6, PRE_TOPC:def_5;
then reconsider V = U11 as non empty Subset of (TOP-REAL m) by A5, XBOOLE_0:def_5, XBOOLE_1:1;
(TUnitSphere n) | U = (TOP-REAL m) | V by A6, A7, PRE_TOPC:7;
then reconsider U2 = (TUnitSphere n) | U as non empty SubSpace of TOP-REAL m ;
reconsider p2 = - p1 as Point of (TOP-REAL m) ;
p2 <> 0. (TOP-REAL m) by A3, EUCLID_2:39;
then A8: TOP-REAL n, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by Th29;
A9: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
A10: TOP-REAL n, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by YELLOW14:19;
[#] U2 = U by PRE_TOPC:def_5
.= the carrier of (Tcircle ((0. (TOP-REAL m)),1)) \ {p2} by TOPREALB:def_7
.= ([#] ((TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)))) \ {p2} by TOPREALB:def_6
.= (Sphere ((0. (TOP-REAL m)),1)) \ {p2} by PRE_TOPC:def_5 ;
then stereographic_projection (U2,p2) is being_homeomorphism by A4, Th31;
then U2, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by T_0TOPSP:def_1;
then TOP-REAL n,U2 are_homeomorphic by A8, BORSUK_3:3;
then U2, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A10, BORSUK_3:3;
hence U, [#] (TOP-REAL n) are_homeomorphic by A9, METRIZTS:def_1; ::_thesis: verum
end;
hence TUnitSphere n is n -locally_euclidean by MFOLD_1:13; ::_thesis: verum
end;
cluster TUnitSphere n -> n -manifold ;
correctness
coherence
TUnitSphere n is n -manifold ;
;
end;