let a be Complex; :: thesis: for X being non empty TopSpace
for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty TopSpace; :: thesis: for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (C_Normed_Space_of_C_0_Functions X); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1: ( ||.F.|| = 0 iff F = 0. (C_Normed_Space_of_C_0_Functions X) )
proof
reconsider FB = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th42;
A2: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A3: 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) = X --> 0 by CC0SP1:18;
A4: 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 by Th45;
( ||.FB.|| = 0 iff FB = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25;
hence ( ||.F.|| = 0 iff F = 0. (C_Normed_Space_of_C_0_Functions X) ) by A2, A3, A4; :: thesis: verum
end;
A5: ||.(a * F).|| = |.a.| * ||.F.||
proof
reconsider FB = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th42;
A6: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A7: a * FB = a * F by Lm14;
reconsider aFB = a * FB as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = a * F as Point of (C_Normed_Space_of_C_0_Functions X) ;
A8: ||.aFB.|| = ||.aF.|| by A7, FUNCT_1:49;
||.(a * FB).|| = |.a.| * ||.FB.|| by CC0SP1:25;
hence ||.(a * F).|| = |.a.| * ||.F.|| by A6, A8; :: thesis: verum
end;
||.(F + G).|| <= ||.F.|| + ||.G.||
proof
A9: ( F in ComplexBoundedFunctions the carrier of X & G in ComplexBoundedFunctions the carrier of X ) by Th42;
reconsider FB = F, GB = G as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by A9;
A10: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49;
FB + GB = F + G by Lm13;
then A11: ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1:49;
reconsider aFB = FB + GB as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = F, aG = G as Point of (C_Normed_Space_of_C_0_Functions X) ;
||.(FB + GB).|| <= ||.FB.|| + ||.GB.|| by CC0SP1:25;
hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A10; :: thesis: verum
end;
hence ( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A5; :: thesis: verum