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
3 1 lnopaddmuli 
 |-  ( ( -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 ) ) )