Metamath Proof Explorer

Theorem lnopmul

Description: Multiplicative property of a linear Hilbert space operator. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopmul 
|- ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 lnopl 
 |-  ( ( ( T e. LinOp /\ A e. CC ) /\ ( B e. ~H /\ 0h e. ~H ) ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( ( A .h ( T ` B ) ) +h ( T ` 0h ) ) )
3 1 2 mpanr2 
 |-  ( ( ( T e. LinOp /\ A e. CC ) /\ B e. ~H ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( ( A .h ( T ` B ) ) +h ( T ` 0h ) ) )
4 3 3impa 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( ( A .h ( T ` B ) ) +h ( T ` 0h ) ) )
5 hvmulcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
6 ax-hvaddid 
 |-  ( ( A .h B ) e. ~H -> ( ( A .h B ) +h 0h ) = ( A .h B ) )
7 5 6 syl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( ( A .h B ) +h 0h ) = ( A .h B ) )
8 7 3adant1 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( ( A .h B ) +h 0h ) = ( A .h B ) )
9 8 fveq2d 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( T ` ( ( A .h B ) +h 0h ) ) = ( T ` ( A .h B ) ) )
10 lnop0 
 |-  ( T e. LinOp -> ( T ` 0h ) = 0h )
11 10 oveq2d 
 |-  ( T e. LinOp -> ( ( A .h ( T ` B ) ) +h ( T ` 0h ) ) = ( ( A .h ( T ` B ) ) +h 0h ) )
12 11 3ad2ant1 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( ( A .h ( T ` B ) ) +h ( T ` 0h ) ) = ( ( A .h ( T ` B ) ) +h 0h ) )
13 lnopf 
 |-  ( T e. LinOp -> T : ~H --> ~H )
14 13 ffvelcdmda 
 |-  ( ( T e. LinOp /\ B e. ~H ) -> ( T ` B ) e. ~H )
15 hvmulcl 
 |-  ( ( A e. CC /\ ( T ` B ) e. ~H ) -> ( A .h ( T ` B ) ) e. ~H )
16 14 15 sylan2 
 |-  ( ( A e. CC /\ ( T e. LinOp /\ B e. ~H ) ) -> ( A .h ( T ` B ) ) e. ~H )
17 16 3impb 
 |-  ( ( A e. CC /\ T e. LinOp /\ B e. ~H ) -> ( A .h ( T ` B ) ) e. ~H )
18 17 3com12 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( A .h ( T ` B ) ) e. ~H )
19 ax-hvaddid 
 |-  ( ( A .h ( T ` B ) ) e. ~H -> ( ( A .h ( T ` B ) ) +h 0h ) = ( A .h ( T ` B ) ) )
20 18 19 syl 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( ( A .h ( T ` B ) ) +h 0h ) = ( A .h ( T ` B ) ) )
21 12 20 eqtrd 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( ( A .h ( T ` B ) ) +h ( T ` 0h ) ) = ( A .h ( T ` B ) ) )
22 4 9 21 3eqtr3d 
 |-  ( ( T e. LinOp /\ A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A .h ( T ` B ) ) )