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 F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) 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, 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,REAL,H,addreal) )
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 F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) 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, 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,REAL,H,addreal)
let x be Point of X; for S being finite OrthonormalFamily of X st not S is empty holds
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) 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, 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,REAL,H,addreal)
let S be finite OrthonormalFamily of X; ( not S is empty implies for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) 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, 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,REAL,H,addreal) )
assume A3:
not S is empty
; for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) 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, 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,REAL,H,addreal)
let F be Function of the carrier of X, the carrier of X; ( S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) 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, 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,REAL,H,addreal) )
assume that
A4:
S c= dom F
and
A5:
for y being Point of X st y in S holds
F . y = (x .|. y) * y
; 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, 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,REAL,H,addreal)
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, 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,REAL,H,addreal) )
assume that
A6:
S c= dom H
and
A7:
for y being Point of X st y in S holds
H . y = (x .|. y) ^2
; (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,REAL,H,addreal)
consider p being FinSequence of the carrier of X such that
A8:
p is one-to-one
and
A9:
rng p = S
and
A10:
setopfunc (S, the carrier of X, the carrier of X,F, the addF of X) = the addF of X "**" (Func_Seq (F,p))
by A1, A2, Def5;
A11:
for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0
proof
let y1,
y2 be
Point of
X;
( y1 in S & y2 in S & y1 <> y2 implies the scalar of X . [(F . y1),(F . y2)] = 0 )
assume that A12:
y1 in S
and A13:
y2 in S
and A14:
y1 <> y2
;
the scalar of X . [(F . y1),(F . y2)] = 0
set z1 =
x .|. y1;
set z2 =
x .|. y2;
S is
OrthogonalFamily of
X
by Def9;
then A15:
y1 .|. y2 = 0
by A12, A13, A14, Def8;
the
scalar of
X . [(F . y1),(F . y2)] =
the
scalar of
X . [((x .|. y1) * y1),(F . y2)]
by A5, A12
.=
the
scalar of
X . [((x .|. y1) * y1),((x .|. y2) * y2)]
by A5, A13
.=
((x .|. y1) * y1) .|. ((x .|. y2) * y2)
by BHSP_1:def 1
.=
(x .|. y2) * (y2 .|. ((x .|. y1) * y1))
by BHSP_1:3
.=
(x .|. y2) * ((x .|. y1) * (y2 .|. y1))
by BHSP_1:3
.=
0
by A15
;
hence
the
scalar of
X . [(F . y1),(F . y2)] = 0
;
verum
end;
A16:
for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)]
(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)) =
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))]
by A10, BHSP_1:def 1
.=
addreal "**" (Func_Seq (H,p))
by A3, A4, A6, A8, A9, A11, A16, Th9
.=
setopfunc (S, the carrier of X,REAL,H,addreal)
by A8, A9, Def5
;
hence
(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,REAL,H,addreal)
; verum