# Metamath Proof Explorer

## Theorem lnopsubi

Description: Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1
`|- T e. LinOp`
Assertion lnopsubi
`|- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) ) )`

### Proof

Step Hyp Ref Expression
1 lnopl.1
` |-  T e. LinOp`
2 neg1cn
` |-  -u 1 e. CC`
` |-  ( ( -u 1 e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( A +h ( -u 1 .h B ) ) ) = ( ( T ` A ) +h ( -u 1 .h ( T ` B ) ) ) )`
4 2 3 mp3an1
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h ( -u 1 .h B ) ) ) = ( ( T ` A ) +h ( -u 1 .h ( T ` B ) ) ) )`
5 hvsubval
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )`
6 5 fveq2d
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( T ` ( A +h ( -u 1 .h B ) ) ) )`
7 1 lnopfi
` |-  T : ~H --> ~H`
8 7 ffvelrni
` |-  ( A e. ~H -> ( T ` A ) e. ~H )`
9 7 ffvelrni
` |-  ( B e. ~H -> ( T ` B ) e. ~H )`
10 hvsubval
` |-  ( ( ( T ` A ) e. ~H /\ ( T ` B ) e. ~H ) -> ( ( T ` A ) -h ( T ` B ) ) = ( ( T ` A ) +h ( -u 1 .h ( T ` B ) ) ) )`
11 8 9 10 syl2an
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( T ` A ) -h ( T ` B ) ) = ( ( T ` A ) +h ( -u 1 .h ( T ` B ) ) ) )`
12 4 6 11 3eqtr4d
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) -h ( T ` B ) ) )`