:: BHSP_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: BHSP_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Element of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p )
proof end;
uniqueness
for b1, b2 being Element of DX st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" p ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b2 = f "**" p ) holds
b1 = b2
proof end;
end;

:: deftheorem defines ++ BHSP_5:def 1 :
for DX being non empty set
for f being BinOp of DX st f is commutative & f is associative & f has_a_unity holds
for Y being finite Subset of DX
for b4 being Element of DX holds
( b4 = f ++ Y iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b4 = f "**" p ) );

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
coherence
( ( Y <> {} implies the add of X ++ Y is set ) & ( not Y <> {} implies 0. X is set ) )
;
consistency
for b1 being set holds verum
;
;
end;

:: deftheorem defines setop_SUM BHSP_5:def 2 :
for X being RealUnitarySpace
for Y being finite Subset of X holds
( ( Y <> {} implies setop_SUM Y,X = the add of X ++ Y ) & ( not Y <> {} implies setop_SUM Y,X = 0. X ) );

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
coherence
the scalar of X . [x,(p . i)] is set
;
;
end;

:: deftheorem defines PO BHSP_5:def 3 :
for X being RealUnitarySpace
for x being Point of X
for p being FinSequence
for i being Nat holds PO i,p,x = the scalar of X . [x,(p . i)];

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
coherence
F * p is FinSequence of DK
;
by FINSEQ_2:36;
end;

:: deftheorem defines Func_Seq BHSP_5:def 4 :
for DK, DX being non empty set
for F being Function of DX,DK
for p being FinSequence of DX holds Func_Seq F,p = F * p;

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
ex b1 being Element of DK ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq F,p) )
proof end;
uniqueness
for b1, b2 being Element of DK st ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b1 = f "**" (Func_Seq F,p) ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b2 = f "**" (Func_Seq F,p) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines setopfunc BHSP_5:def 5 :
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 Y being finite Subset of DX
for F being Function of DX,DK st Y c= dom F holds
for b6 being Element of DK holds
( b6 = setopfunc Y,DX,DK,F,f iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b6 = f "**" (Func_Seq F,p) ) );

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
ex b1 being Real 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 ) & b1 = addreal "**" q ) )
proof end;
uniqueness
for b1, b2 being Real st 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 ) & b1 = addreal "**" q ) ) & 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 ) & b2 = addreal "**" q ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines setop_xPre_PROD BHSP_5:def 6 :
for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X
for b4 being Real holds
( b4 = setop_xPre_PROD x,Y,X iff 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 ) & b4 = addreal "**" q ) ) );

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
coherence
( ( Y <> {} implies setop_xPre_PROD x,Y,X is Real ) & ( not Y <> {} implies 0 is Real ) )
;
consistency
for b1 being Real holds verum
;
;
end;

:: deftheorem defines setop_xPROD BHSP_5:def 7 :
for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X holds
( ( Y <> {} implies setop_xPROD x,Y,X = setop_xPre_PROD x,Y,X ) & ( not Y <> {} implies setop_xPROD x,Y,X = 0 ) );

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
ex b1 being Subset of X st
for x, y being Point of X st x in b1 & y in b1 & x <> y holds
x .|. y = 0
proof end;
end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :
for X being RealUnitarySpace
for b2 being Subset of X holds
( b2 is OrthogonalFamily of X iff for x, y being Point of X st x in b2 & y in b2 & x <> y holds
x .|. y = 0 );

theorem Th2: :: BHSP_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace holds {} is OrthogonalFamily of X
proof end;

registration
let X be RealUnitarySpace;
cluster finite OrthogonalFamily of X;
existence
ex b1 being OrthogonalFamily of X st b1 is finite
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
ex b1 being Subset of X st
( b1 is OrthogonalFamily of X & ( for x being Point of X st x in b1 holds
x .|. x = 1 ) )
proof end;
end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :
for X being RealUnitarySpace
for b2 being Subset of X holds
( b2 is OrthonormalFamily of X iff ( b2 is OrthogonalFamily of X & ( for x being Point of X st x in b2 holds
x .|. x = 1 ) ) );

theorem Th3: :: BHSP_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealUnitarySpace holds {} is OrthonormalFamily of X
proof end;

registration
let X be RealUnitarySpace;
cluster finite OrthonormalFamily of X;
existence
ex b1 being OrthonormalFamily of X st b1 is finite
proof end;
end;

theorem :: BHSP_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2
proof end;

theorem :: BHSP_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;