set W = ComplexBoundedFunctions X;
set V = CAlgebra X;
for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v + u in ComplexBoundedFunctions X
proof
let v,
u be
Element of
(CAlgebra X);
( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v + u in ComplexBoundedFunctions X )
assume A1:
(
v in ComplexBoundedFunctions X &
u in ComplexBoundedFunctions X )
;
v + u in ComplexBoundedFunctions X
consider v1 being
Function of
X,
COMPLEX such that A2:
(
v1 = v &
v1 | X is
bounded )
by A1;
consider u1 being
Function of
X,
COMPLEX such that A3:
(
u1 = u &
u1 | X is
bounded )
by A1;
dom (v1 + u1) = X /\ X
by FUNCT_2:def 1;
then A4:
(
v1 + u1 is
Function of
X,
COMPLEX &
(v1 + u1) | X is
bounded )
by A2, A3, CFUNCT_1:75;
reconsider h =
v + u as
Element of
Funcs (
X,
COMPLEX) ;
A5:
ex
f being
Function st
(
h = f &
dom f = X &
rng f c= COMPLEX )
by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = X /\ (dom u1)
by FUNCT_2:def 1;
then A6:
(dom v1) /\ (dom u1) = X /\ X
by FUNCT_2:def 1;
for
x being
object st
x in dom h holds
h . x = (v1 . x) + (u1 . x)
by A2, A3, CFUNCDOM:1;
then
v + u = v1 + u1
by A6, A5, VALUED_1:def 1;
hence
v + u in ComplexBoundedFunctions X
by A4;
verum
end;
then A7:
ComplexBoundedFunctions X is add-closed
by IDEAL_1:def 1;
for v being Element of (CAlgebra X) st v in ComplexBoundedFunctions X holds
- v in ComplexBoundedFunctions X
then A14:
ComplexBoundedFunctions X is having-inverse
;
for a being Complex
for u being Element of (CAlgebra X) st u in ComplexBoundedFunctions X holds
a * u in ComplexBoundedFunctions X
hence
ComplexBoundedFunctions X is Cadditively-linearly-closed
by A7, A14; ComplexBoundedFunctions X is multiplicatively-closed
A20:
for v, u being Element of (CAlgebra X) st v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X holds
v * u in ComplexBoundedFunctions X
proof
let v,
u be
Element of
(CAlgebra X);
( v in ComplexBoundedFunctions X & u in ComplexBoundedFunctions X implies v * u in ComplexBoundedFunctions X )
assume A21:
(
v in ComplexBoundedFunctions X &
u in ComplexBoundedFunctions X )
;
v * u in ComplexBoundedFunctions X
consider v1 being
Function of
X,
COMPLEX such that A22:
(
v1 = v &
v1 | X is
bounded )
by A21;
consider u1 being
Function of
X,
COMPLEX such that A23:
(
u1 = u &
u1 | X is
bounded )
by A21;
dom (v1 (#) u1) = X /\ X
by FUNCT_2:def 1;
then A24:
(
v1 (#) u1 is
Function of
X,
COMPLEX &
(v1 (#) u1) | X is
bounded )
by A22, A23, CFUNCT_1:76;
reconsider h =
v * u as
Element of
Funcs (
X,
COMPLEX) ;
A25:
ex
f being
Function st
(
h = f &
dom f = X &
rng f c= COMPLEX )
by FUNCT_2:def 2;
(dom v1) /\ (dom u1) = X /\ (dom u1)
by FUNCT_2:def 1;
then A26:
(dom v1) /\ (dom u1) = X /\ X
by FUNCT_2:def 1;
for
x being
object st
x in dom h holds
h . x = (v1 . x) * (u1 . x)
by A22, A23, CFUNCDOM:2;
then
v * u = v1 (#) u1
by A26, A25, VALUED_1:def 4;
hence
v * u in ComplexBoundedFunctions X
by A24;
verum
end;
reconsider g = ComplexFuncUnit X as Function of X,COMPLEX ;
g | X is bounded
;
then
1. (CAlgebra X) in ComplexBoundedFunctions X
;
hence
ComplexBoundedFunctions X is multiplicatively-closed
by A20; verum