let X be RealUnitarySpace; ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 )
assume that
A1:
( the addF of X is commutative & the addF of X is associative )
and
A2:
the addF of X is having_a_unity
; for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
let x be Point of X; for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
let S be finite OrthonormalFamily of X; ( not S is empty implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 )
assume A3:
not S is empty
; for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
let H be Function of the carrier of X,REAL; ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) implies setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2 )
assume that
A4:
S c= dom H
and
A5:
for y being Point of X st y in S holds
H . y = (x .|. y) ^2
; setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
now 0 <= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal))deffunc H1(
object )
-> set = the
Mult of
X . [( the scalar of X . [x,$1]),$1];
A6:
for
y being
object st
y in the
carrier of
X holds
H1(
y)
in the
carrier of
X
ex
F0 being
Function of the
carrier of
X, the
carrier of
X st
for
y being
object st
y in the
carrier of
X holds
F0 . y = H1(
y)
from FUNCT_2:sch 2(A6);
then consider F0 being
Function of the
carrier of
X, the
carrier of
X such that A8:
for
y being
object st
y in the
carrier of
X holds
F0 . y = the
Mult of
X . [( the scalar of X . [x,y]),y]
;
A9:
dom F0 = the
carrier of
X
by FUNCT_2:def 1;
then consider F being
Function of the
carrier of
X, the
carrier of
X such that A10:
S c= dom F
and A11:
for
y being
Point of
X st
y in S holds
F . y = (x .|. y) * y
by A9;
set z =
setopfunc (
S, the
carrier of
X, the
carrier of
X,
F, the
addF of
X);
(setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. x = setopfunc (
S, the
carrier of
X,
REAL,
H,
addreal)
by A1, A2, A3, A4, A5, A10, A11, Th11;
then
x .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) = (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X))
by A1, A2, A3, A4, A5, A10, A11, Th12;
then (x - (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X))) .|. (x - (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X))) =
(((x .|. x) - ((setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)))) - ((setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)))) + ((setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,F, the addF of X)))
by BHSP_1:13
.=
(x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal))
by A1, A2, A3, A4, A5, A10, A11, Th12
;
hence
0 <= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal))
by BHSP_1:def 2;
verum end;
then A12:
0 + (setopfunc (S, the carrier of X,REAL,H,addreal)) <= x .|. x
by XREAL_1:19;
0 <= x .|. x
by BHSP_1:def 2;
then
setopfunc (S, the carrier of X,REAL,H,addreal) <= (sqrt (x .|. x)) ^2
by A12, SQUARE_1:def 2;
hence
setopfunc (S, the carrier of X,REAL,H,addreal) <= ||.x.|| ^2
by BHSP_1:def 4; verum