:: BHSP_5 semantic presentation

theorem Th1: :: BHSP_5:1

for D being set
for p1, p2 being FinSequence of D st p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 holds
( dom p1 = dom p2 & ex P being Permutation of dom p1 st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )

proof end;

definition

let DX be non empty set ;
let f be BinOp of DX;
assume A1: ( f is commutative & f is associative & f has_a_unity ) ;
let Y be finite Subset of DX;
func f ++ Y -> Element of DX means :: BHSP_5:def 1
ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & it = f "**" p );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines ++ BHSP_5:def 1 :

definition

let X be RealUnitarySpace;
let Y be finite Subset of X;
func setop_SUM Y,X -> set equals :: BHSP_5:def 2
the add of X ++ Y if Y <> {}
otherwise 0. X;
correctness ;

end;

:: deftheorem defines setop_SUM BHSP_5:def 2 :

definition

let X be RealUnitarySpace;
let x be Point of X;
let p be FinSequence;
let i be Nat;
func PO i,p,x -> set equals :: BHSP_5:def 3
the scalar of X . [x,(p . i)];
correctness ;

end;

:: deftheorem defines PO BHSP_5:def 3 :

definition

let DK, DX be non empty set ;
let F be Function of DX,DK;
let p be FinSequence of DX;
func Func_Seq F,p -> FinSequence of DK equals :: BHSP_5:def 4
F * p;
correctness by FINSEQ_2:36;

end;

:: deftheorem defines Func_Seq BHSP_5:def 4 :

definition

let DK, DX be non empty set ;
let f be BinOp of DK;
assume A1: ( f is commutative & f is associative & f has_a_unity ) ;
let Y be finite Subset of DX;
let F be Function of DX,DK;
assume A2: Y c= dom F ;
func setopfunc Y,DX,DK,F,f -> Element of DK means :Def5: :: BHSP_5:def 5
ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & it = f "**" (Func_Seq F,p) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines setopfunc BHSP_5:def 5 :

definition

let X be RealUnitarySpace;
let x be Point of X;
let Y be finite Subset of X;
func setop_xPre_PROD x,Y,X -> Real means :: BHSP_5:def 6
ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO i,p,x ) & it = addreal "**" q ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines setop_xPre_PROD BHSP_5:def 6 :

definition

let X be RealUnitarySpace;
let x be Point of X;
let Y be finite Subset of X;
func setop_xPROD x,Y,X -> Real equals :: BHSP_5:def 7
setop_xPre_PROD x,Y,X if Y <> {}
otherwise 0;
correctness ;

end;

:: deftheorem defines setop_xPROD BHSP_5:def 7 :

definition

let X be RealUnitarySpace;
mode OrthogonalFamily of X -> Subset of X means :Def8: :: BHSP_5:def 8
for x, y being Point of X st x in it & y in it & x <> y holds
x .|. y = 0;
existence

proof end;

end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :

theorem Th2: :: BHSP_5:2

for X being RealUnitarySpace holds {} is OrthogonalFamily of X

proof end;

registration

let X be RealUnitarySpace;
cluster finite OrthogonalFamily of X;
existence

proof end;

end;

definition

let X be RealUnitarySpace;
mode OrthonormalFamily of X -> Subset of X means :Def9: :: BHSP_5:def 9
( it is OrthogonalFamily of X & ( for x being Point of X st x in it holds
x .|. x = 1 ) );
existence

proof end;

end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :

theorem Th3: :: BHSP_5:3

for X being RealUnitarySpace holds {} is OrthonormalFamily of X

proof end;

registration

let X be RealUnitarySpace;
cluster finite OrthonormalFamily of X;
existence

proof end;

end;

theorem :: BHSP_5:4

for X being RealUnitarySpace
for x being Point of X holds
( x = 0. X iff for y being Point of X holds x .|. y = 0 )

proof end;

theorem :: BHSP_5:5

for X being RealUnitarySpace
for x, y being Point of X holds (||.(x + y).|| ^2 ) + (||.(x - y).|| ^2 ) = (2 * (||.x.|| ^2 )) + (2 * (||.y.|| ^2 ))

proof end;

theorem :: BHSP_5:6

for X being RealUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2 ) + (||.y.|| ^2 )

proof end;

theorem Th7: :: BHSP_5:7

for X being RealUnitarySpace
for p being FinSequence of the carrier of X st len p >= 1 & ( for i, j being Nat st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = the scalar of X . [(p . i),(p . i)] ) holds
(the add of X "**" p) .|. (the add of X "**" p) = addreal "**" q

proof end;

theorem Th8: :: BHSP_5:8

for X being RealUnitarySpace
for x being Point of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. (the add of X "**" p) = addreal "**" q

proof end;

theorem Th9: :: BHSP_5:9

for X being RealUnitarySpace
for S being non empty finite Subset of X
for F being Function of the carrier of X,the carrier of X st S c= dom F & ( 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 ) 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 = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [(the add of X "**" (Func_Seq F,p)),(the add of X "**" (Func_Seq F,p))] = addreal "**" (Func_Seq H,p)

proof end;

theorem Th10: :: BHSP_5:10

for X being RealUnitarySpace
for x being Point of X
for S being non empty finite Subset of X
for F being Function of the carrier of X,the carrier of X st S c= dom F 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 = the scalar of X . [x,(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [x,(the add of X "**" (Func_Seq F,p))] = addreal "**" (Func_Seq H,p)

proof end;

theorem Th11: :: BHSP_5:11

for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_a_unity holds
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
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
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the add of X) = setopfunc S,the carrier of X,REAL ,H,addreal

proof end;

theorem Th12: :: BHSP_5:12

for X being RealUnitarySpace st the add of X is commutative & the add of X is associative & the add of X has_a_unity holds
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 add of X) .|. (setopfunc S,the carrier of X,the carrier of X,F,the add of X) = setopfunc S,the carrier of X,REAL ,H,addreal

proof end;

theorem :: BHSP_5:13

proof end;

theorem :: BHSP_5:14

for DK, DX being non empty set
for f being BinOp of DK st f is commutative & f is associative & f has_a_unity holds
for Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc Z,DX,DK,F,f = f . (setopfunc Y1,DX,DK,F,f),(setopfunc Y2,DX,DK,F,f)

proof end;