:: by Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura

::

:: Received January 30, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

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 ) )

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 that

A1: ( f is commutative & f is associative ) and

A2: f is having_a_unity ;

let Y be finite Subset of DX;

ex b_{1} being Element of DX ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{1} = f "**" p )

for b_{1}, b_{2} being Element of DX st ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{1} = f "**" p ) & ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{2} = f "**" p ) holds

b_{1} = b_{2}

end;
let f be BinOp of DX;

assume that

A1: ( f is commutative & f is associative ) and

A2: f is having_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 p being FinSequence of DX st

( p is one-to-one & rng p = Y & it = f "**" p );

ex b

( p is one-to-one & rng p = Y & b

proof end;

uniqueness for b

( p is one-to-one & rng p = Y & b

( p is one-to-one & rng p = Y & b

b

proof 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 is having_a_unity holds

for Y being finite Subset of DX

for b_{4} being Element of DX holds

( b_{4} = f ++ Y iff ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{4} = f "**" p ) );

for DX being non empty set

for f being BinOp of DX st f is commutative & f is associative & f is having_a_unity holds

for Y being finite Subset of DX

for b

( b

( p is one-to-one & rng p = Y & b

definition

let X be RealUnitarySpace;

let Y be finite Subset of X;

correctness

coherence

( ( Y <> {} implies the addF of X ++ Y is set ) & ( not Y <> {} implies 0. X is set ) );

consistency

for b_{1} being set holds verum;

;

end;
let Y be finite Subset of X;

correctness

coherence

( ( Y <> {} implies the addF of X ++ Y is set ) & ( not Y <> {} implies 0. X is set ) );

consistency

for b

;

:: 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 addF of X ++ Y ) & ( not Y <> {} implies setop_SUM (Y,X) = 0. X ) );

for X being RealUnitarySpace

for Y being finite Subset of X holds

( ( Y <> {} implies setop_SUM (Y,X) = the addF 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;

correctness

coherence

the scalar of X . [x,(p . i)] is set ;

;

end;
let x be Point of X;

let p be FinSequence;

let i be Nat;

correctness

coherence

the scalar of X . [x,(p . i)] is set ;

;

:: 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)];

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;

correctness

coherence

F * p is FinSequence of DK;

by FINSEQ_2:32;

end;
let F be Function of DX,DK;

let p be FinSequence of DX;

correctness

coherence

F * p is FinSequence of DK;

by FINSEQ_2:32;

:: 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;

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 that

A1: ( f is commutative & f is associative ) and

A2: f is having_a_unity ;

let Y be finite Subset of DX;

let F be Function of DX,DK;

A3: dom F = DX by FUNCT_2:def 1;

ex b_{1} being Element of DK ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{1} = f "**" (Func_Seq (F,p)) )

for b_{1}, b_{2} being Element of DK st ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{1} = f "**" (Func_Seq (F,p)) ) & ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{2} = f "**" (Func_Seq (F,p)) ) holds

b_{1} = b_{2}

end;
let f be BinOp of DK;

assume that

A1: ( f is commutative & f is associative ) and

A2: f is having_a_unity ;

let Y be finite Subset of DX;

let F be Function of DX,DK;

A3: dom F = DX by FUNCT_2:def 1;

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 p being FinSequence of DX st

( p is one-to-one & rng p = Y & it = f "**" (Func_Seq (F,p)) );

ex b

( p is one-to-one & rng p = Y & b

proof end;

uniqueness for b

( p is one-to-one & rng p = Y & b

( p is one-to-one & rng p = Y & b

b

proof 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 is having_a_unity holds

for Y being finite Subset of DX

for F being Function of DX,DK

for b_{6} being Element of DK holds

( b_{6} = setopfunc (Y,DX,DK,F,f) iff ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & b_{6} = f "**" (Func_Seq (F,p)) ) );

for DK, DX being non empty set

for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds

for Y being finite Subset of DX

for F being Function of DX,DK

for b

( b

( p is one-to-one & rng p = Y & b

definition

let X be RealUnitarySpace;

let x be Point of X;

let Y be finite Subset of X;

ex b_{1} 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) ) & b_{1} = addreal "**" q ) )

for b_{1}, b_{2} 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) ) & b_{1} = 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) ) & b_{2} = addreal "**" q ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

( 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) ) & b

proof end;

uniqueness for b

( 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) ) & b

( 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) ) & b

b

proof 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 b_{4} being Real holds

( b_{4} = 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) ) & b_{4} = addreal "**" q ) ) );

for X being RealUnitarySpace

for x being Point of X

for Y being finite Subset of X

for b

( b

( 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) ) & b

definition

let X be RealUnitarySpace;

let x be Point of X;

let Y be finite Subset of X;

coherence

( ( Y <> {} implies setop_xPre_PROD (x,Y,X) is Real ) & ( not Y <> {} implies 0 is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
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 setop_xPre_PROD (x,Y,X) if Y <> {}

otherwise 0 ;

coherence

( ( Y <> {} implies setop_xPre_PROD (x,Y,X) is Real ) & ( not Y <> {} implies 0 is Real ) );

consistency

for b

;

:: 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 ) );

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;

ex b_{1} being Subset of X st

for x, y being Point of X st x in b_{1} & y in b_{1} & x <> y holds

x .|. y = 0

end;
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 for x, y being Point of X st x in it & y in it & x <> y holds

x .|. y = 0 ;

ex b

for x, y being Point of X st x in b

x .|. y = 0

proof end;

:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :

for X being RealUnitarySpace

for b_{2} being Subset of X holds

( b_{2} is OrthogonalFamily of X iff for x, y being Point of X st x in b_{2} & y in b_{2} & x <> y holds

x .|. y = 0 );

for X being RealUnitarySpace

for b

( b

x .|. y = 0 );

registration

let X be RealUnitarySpace;

existence

ex b_{1} being OrthogonalFamily of X st b_{1} is finite

end;
existence

ex b

proof end;

definition

let X be RealUnitarySpace;

ex b_{1} being Subset of X st

( b_{1} is OrthogonalFamily of X & ( for x being Point of X st x in b_{1} holds

x .|. x = 1 ) )

end;
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 ( it is OrthogonalFamily of X & ( for x being Point of X st x in it holds

x .|. x = 1 ) );

ex b

( b

x .|. x = 1 ) )

proof end;

:: deftheorem Def9 defines OrthonormalFamily BHSP_5:def 9 :

for X being RealUnitarySpace

for b_{2} being Subset of X holds

( b_{2} is OrthonormalFamily of X iff ( b_{2} is OrthogonalFamily of X & ( for x being Point of X st x in b_{2} holds

x .|. x = 1 ) ) );

for X being RealUnitarySpace

for b

( b

x .|. x = 1 ) ) );

registration

let X be RealUnitarySpace;

existence

ex b_{1} being OrthonormalFamily of X st b_{1} is finite

end;
existence

ex b

proof 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 )

for x being Point of X holds

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

proof end;

:: parallelogram law

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))

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

proof end;

:: The Pythagorean theorem

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)

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 addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q

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 addF of X "**" p) .|. ( the addF 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 addF of X "**" p) = addreal "**" q

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 addF 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 addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))

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 addF of X "**" (Func_Seq (F,p))),( the addF 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 addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))

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 addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))

proof end;

theorem Th11: :: BHSP_5:11

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

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 addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)

proof end;

theorem Th12: :: BHSP_5:12

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_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 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)

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)

proof end;

theorem :: BHSP_5:13

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_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

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

for DK, DX being non empty set

for f being BinOp of DK st f is commutative & f is associative & f is having_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)))

for f being BinOp of DK st f is commutative & f is associative & f is having_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;