Theorem hhlnoi

Description: The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlno.1	|- U = <. <. +h , .h >. , normh >.
	hhlno.2	|- L = ( U LnOp U )
Assertion	hhlnoi	|- LinOp = L

Proof

Step	Hyp	Ref	Expression
1		hhlno.1	|- U = <. <. +h , .h >. , normh >.
2		hhlno.2	|- L = ( U LnOp U )
3		df-lnop	|- LinOp = { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) }
4	1	hhnv	|- U e. NrmCVec
5	1	hhba	|- ~H = ( BaseSet ` U )
6	1	hhva	|- +h = ( +v ` U )
7	1	hhsm	|- .h = ( .sOLD ` U )
8	5 5 6 6 7 7 2	lnoval	|- ( ( U e. NrmCVec /\ U e. NrmCVec ) -> L = { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) } )
9	4 4 8	mp2an	|- L = { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) }
10	3 9	eqtr4i	|- LinOp = L