:: BHSP_5 semantic presentation

theorem Th1: :: BHSP_5:1

for b₁ being set
for b₂, b₃ being FinSequence of b₁ st b₂ is one-to-one & b₃ is one-to-one & rng b₂ = rng b₃ holds
( dom b₂ = dom b₃ & ex b₄ being Permutation of dom b₂ st
( b₃ = b₂ * b₄ & dom b₄ = dom b₂ & rng b₄ = dom b₂ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
assume E2: ( c₂ is commutative & c₂ is associative & c₂ has_a_unity ) ;
let c₃ be finite Subset of c₁;
func c₂ ++ c₃ -> Element of a₁ means :: BHSP_5:def 1
ex b₁ being FinSequence of a₁ st
( b₁ is one-to-one & rng b₁ = a₃ & a₄ = a₂ "**" b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ++ BHSP_5:def 1 :

definition

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

end;

:: deftheorem Def2 defines setop_SUM BHSP_5:def 2 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be FinSequence;
let c₄ be Nat;
func PO c₄,c₃,c₂ -> set equals :: BHSP_5:def 3
the scalar of a₁ . [a₂,(a₃ . a₄)];
correctness ;

end;

:: deftheorem Def3 defines PO BHSP_5:def 3 :

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₂,c₁;
let c₄ be FinSequence of c₂;
func Func_Seq c₃,c₄ -> FinSequence of a₁ equals :: BHSP_5:def 4
a₃ * a₄;
correctness by FINSEQ_2:36;

end;

:: deftheorem Def4 defines Func_Seq BHSP_5:def 4 :

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
assume E2: ( c₃ is commutative & c₃ is associative & c₃ has_a_unity ) ;
let c₄ be finite Subset of c₂;
let c₅ be Function of c₂,c₁;
assume E3: c₄ c= dom c₅ ;
func setopfunc c₄,c₂,c₁,c₅,c₃ -> Element of a₁ means :Def5: :: BHSP_5:def 5
ex b₁ being FinSequence of a₂ st
( b₁ is one-to-one & rng b₁ = a₄ & a₆ = a₃ "**" (Func_Seq a₅,b₁) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines setopfunc BHSP_5:def 5 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be finite Subset of c₁;
func setop_xPre_PROD c₂,c₃,c₁ -> Real means :: BHSP_5:def 6
ex b₁ being FinSequence of the carrier of a₁ st
( b₁ is one-to-one & rng b₁ = a₃ & ex b₂ being FinSequence of REAL st
( dom b₂ = dom b₁ & ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = PO b₃,b₁,a₂ ) & a₄ = addreal "**" b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines setop_xPre_PROD BHSP_5:def 6 :

definition

let c₁ be RealUnitarySpace;
let c₂ be Point of c₁;
let c₃ be finite Subset of c₁;
func setop_xPROD c₂,c₃,c₁ -> Real equals :: BHSP_5:def 7
setop_xPre_PROD a₂,a₃,a₁ if a₃ <> {}
otherwise 0;
correctness ;

end;

:: deftheorem Def7 defines setop_xPROD BHSP_5:def 7 :

definition

let c₁ be RealUnitarySpace;
mode OrthogonalFamily of c₁ -> Subset of a₁ means :Def8: :: BHSP_5:def 8
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ holds
b₁ .|. b₂ = 0;
existence

proof end;

end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :

theorem Th2: :: BHSP_5:2

for b₁ being RealUnitarySpace holds {} is OrthogonalFamily of b₁

proof end;

registration

let c₁ be RealUnitarySpace;
cluster finite OrthogonalFamily of a₁;
existence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :

theorem Th3: :: BHSP_5:3

for b₁ being RealUnitarySpace holds {} is OrthonormalFamily of b₁

proof end;

registration

let c₁ be RealUnitarySpace;
cluster finite OrthonormalFamily of a₁;
existence

proof end;

end;

theorem Th4: :: BHSP_5:4

for b₁ being RealUnitarySpace
for b₂ being Point of b₁ holds
( b₂ = 0. b₁ iff for b₃ being Point of b₁ holds b₂ .|. b₃ = 0 )

proof end;

theorem Th5: :: BHSP_5:5

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ holds (||.(b₂ + b₃).|| ^2 ) + (||.(b₂ - b₃).|| ^2 ) = (2 * (||.b₂.|| ^2 )) + (2 * (||.b₃.|| ^2 ))

proof end;

theorem Th6: :: BHSP_5:6

for b₁ being RealUnitarySpace
for b₂, b₃ being Point of b₁ st b₂,b₃ are_orthogonal holds
||.(b₂ + b₃).|| ^2 = (||.b₂.|| ^2 ) + (||.b₃.|| ^2 )

proof end;

theorem Th7: :: BHSP_5:7

for b₁ being RealUnitarySpace
for b₂ being FinSequence of the carrier of b₁ st len b₂ >= 1 & ( for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom b₂ & b₃ <> b₄ holds
the scalar of b₁ . [(b₂ . b₃),(b₂ . b₄)] = 0 ) holds
for b₃ being FinSequence of REAL st dom b₂ = dom b₃ & ( for b₄ being Nat st b₄ in dom b₃ holds
b₃ . b₄ = the scalar of b₁ . [(b₂ . b₄),(b₂ . b₄)] ) holds
(the add of b₁ "**" b₂) .|. (the add of b₁ "**" b₂) = addreal "**" b₃

proof end;

theorem Th8: :: BHSP_5:8

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being FinSequence of the carrier of b₁ st len b₃ >= 1 holds
for b₄ being FinSequence of REAL st dom b₃ = dom b₄ & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ = the scalar of b₁ . [b₂,(b₃ . b₅)] ) holds
b₂ .|. (the add of b₁ "**" b₃) = addreal "**" b₄

proof end;

theorem Th9: :: BHSP_5:9

for b₁ being RealUnitarySpace
for b₂ being non empty finite Subset of b₁
for b₃ being Function of the carrier of b₁,the carrier of b₁ st b₂ c= dom b₃ & ( for b₄, b₅ being Point of b₁ st b₄ in b₂ & b₅ in b₂ & b₄ <> b₅ holds
the scalar of b₁ . [(b₃ . b₄),(b₃ . b₅)] = 0 ) holds
for b₄ being Function of the carrier of b₁, REAL st b₂ c= dom b₄ & ( for b₅ being Point of b₁ st b₅ in b₂ holds
b₄ . b₅ = the scalar of b₁ . [(b₃ . b₅),(b₃ . b₅)] ) holds
for b₅ being FinSequence of the carrier of b₁ st b₅ is one-to-one & rng b₅ = b₂ holds
the scalar of b₁ . [(the add of b₁ "**" (Func_Seq b₃,b₅)),(the add of b₁ "**" (Func_Seq b₃,b₅))] = addreal "**" (Func_Seq b₄,b₅)

proof end;

theorem Th10: :: BHSP_5:10

for b₁ being RealUnitarySpace
for b₂ being Point of b₁
for b₃ being non empty finite Subset of b₁
for b₄ being Function of the carrier of b₁,the carrier of b₁ st b₃ c= dom b₄ holds
for b₅ being Function of the carrier of b₁, REAL st b₃ c= dom b₅ & ( for b₆ being Point of b₁ st b₆ in b₃ holds
b₅ . b₆ = the scalar of b₁ . [b₂,(b₄ . b₆)] ) holds
for b₆ being FinSequence of the carrier of b₁ st b₆ is one-to-one & rng b₆ = b₃ holds
the scalar of b₁ . [b₂,(the add of b₁ "**" (Func_Seq b₄,b₆))] = addreal "**" (Func_Seq b₅,b₆)

proof end;

theorem Th11: :: BHSP_5:11

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂ being Point of b₁
for b₃ being finite OrthonormalFamily of b₁ st not b₃ is empty holds
for b₄ being Function of the carrier of b₁, REAL st b₃ c= dom b₄ & ( for b₅ being Point of b₁ st b₅ in b₃ holds
b₄ . b₅ = (b₂ .|. b₅) ^2 ) holds
for b₅ being Function of the carrier of b₁,the carrier of b₁ st b₃ c= dom b₅ & ( for b₆ being Point of b₁ st b₆ in b₃ holds
b₅ . b₆ = (b₂ .|. b₆) * b₆ ) holds
b₂ .|. (setopfunc b₃,the carrier of b₁,the carrier of b₁,b₅,the add of b₁) = setopfunc b₃,the carrier of b₁,REAL ,b₄,addreal

proof end;

theorem Th12: :: BHSP_5:12

for b₁ being RealUnitarySpace st the add of b₁ is commutative & the add of b₁ is associative & the add of b₁ has_a_unity holds
for b₂ being Point of b₁
for b₃ being finite OrthonormalFamily of b₁ st not b₃ is empty holds
for b₄ being Function of the carrier of b₁,the carrier of b₁ st b₃ c= dom b₄ & ( for b₅ being Point of b₁ st b₅ in b₃ holds
b₄ . b₅ = (b₂ .|. b₅) * b₅ ) holds
for b₅ being Function of the carrier of b₁, REAL st b₃ c= dom b₅ & ( for b₆ being Point of b₁ st b₆ in b₃ holds
b₅ . b₆ = (b₂ .|. b₆) ^2 ) holds
(setopfunc b₃,the carrier of b₁,the carrier of b₁,b₄,the add of b₁) .|. (setopfunc b₃,the carrier of b₁,the carrier of b₁,b₄,the add of b₁) = setopfunc b₃,the carrier of b₁,REAL ,b₅,addreal

proof end;

theorem Th13: :: BHSP_5:13

proof end;

theorem Th14: :: BHSP_5:14

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁ st b₃ is commutative & b₃ is associative & b₃ has_a_unity holds
for b₄, b₅ being finite Subset of b₂ st b₄ misses b₅ holds
for b₆ being Function of b₂,b₁ st b₄ c= dom b₆ & b₅ c= dom b₆ holds
for b₇ being finite Subset of b₂ st b₇ = b₄ \/ b₅ holds
setopfunc b₇,b₂,b₁,b₆,b₃ = b₃ . (setopfunc b₄,b₂,b₁,b₆,b₃),(setopfunc b₅,b₂,b₁,b₆,b₃)

proof end;