Metamath Proof Explorer

Theorem hodval

Description: Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hodmval 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )
2 1 fveq1d 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( S -op T ) ` A ) = ( ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) ` A ) )
3 fveq2 
 |-  ( x = A -> ( S ` x ) = ( S ` A ) )
4 fveq2 
 |-  ( x = A -> ( T ` x ) = ( T ` A ) )
5 3 4 oveq12d 
 |-  ( x = A -> ( ( S ` x ) -h ( T ` x ) ) = ( ( S ` A ) -h ( T ` A ) ) )
6 eqid 
 |-  ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) )
7 ovex 
 |-  ( ( S ` A ) -h ( T ` A ) ) e. _V
8 5 6 7 fvmpt 
 |-  ( A e. ~H -> ( ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) ` A ) = ( ( S ` A ) -h ( T ` A ) ) )
9 2 8 sylan9eq 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S -op T ) ` A ) = ( ( S ` A ) -h ( T ` A ) ) )
10 9 3impa 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S -op T ) ` A ) = ( ( S ` A ) -h ( T ` A ) ) )