# Metamath Proof Explorer

## Theorem hosval

Description: Value of the sum 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 hosval
`|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S +op T ) ` A ) = ( ( S ` A ) +h ( T ` A ) ) )`

### Proof

Step Hyp Ref Expression
1 hosmval
` |-  ( ( 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 ) ) )`