This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnopmulsubi

Description: Product/subtraction property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lnopl.1 
 |-  T e. LinOp
2 hvmulcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
3 1 lnopsubi 
 |-  ( ( ( A .h B ) e. ~H /\ C e. ~H ) -> ( T ` ( ( A .h B ) -h C ) ) = ( ( T ` ( A .h B ) ) -h ( T ` C ) ) )
4 2 3 stoic3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( ( A .h B ) -h C ) ) = ( ( T ` ( A .h B ) ) -h ( T ` C ) ) )
5 1 lnopmuli 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )
6 5 3adant3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )
7 6 oveq1d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( T ` ( A .h B ) ) -h ( T ` C ) ) = ( ( A .h ( T ` B ) ) -h ( T ` C ) ) )
8 4 7 eqtrd 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( T ` ( ( A .h B ) -h C ) ) = ( ( A .h ( T ` B ) ) -h ( T ` C ) ) )