Theorem hodmval

Description: Value of the difference of two Hilbert space operators. (Contributed by NM, 9-Nov-2000) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hodmval	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	|- ~H e. _V
2	1 1	elmap	|- ( S e. ( ~H ^m ~H ) <-> S : ~H --> ~H )
3	1 1	elmap	|- ( T e. ( ~H ^m ~H ) <-> T : ~H --> ~H )
4		fveq1	|- ( f = S -> ( f ` x ) = ( S ` x ) )
5	4	oveq1d	|- ( f = S -> ( ( f ` x ) -h ( g ` x ) ) = ( ( S ` x ) -h ( g ` x ) ) )
6	5	mpteq2dv	|- ( f = S -> ( x e. ~H |-> ( ( f ` x ) -h ( g ` x ) ) ) = ( x e. ~H |-> ( ( S ` x ) -h ( g ` x ) ) ) )
7		fveq1	|- ( g = T -> ( g ` x ) = ( T ` x ) )
8	7	oveq2d	|- ( g = T -> ( ( S ` x ) -h ( g ` x ) ) = ( ( S ` x ) -h ( T ` x ) ) )
9	8	mpteq2dv	|- ( g = T -> ( x e. ~H |-> ( ( S ` x ) -h ( g ` x ) ) ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )
10		df-hodif	|- -op = ( f e. ( ~H ^m ~H ) , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( ( f ` x ) -h ( g ` x ) ) ) )
11	1	mptex	|- ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) e. _V
12	6 9 10 11	ovmpo	|- ( ( S e. ( ~H ^m ~H ) /\ T e. ( ~H ^m ~H ) ) -> ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )
13	2 3 12	syl2anbr	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )