Metamath Proof Explorer

Theorem lnfnmul

Description: Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( T ` ( A .h B ) ) = ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` ( A .h B ) ) )
2 fveq1 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( T ` B ) = ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` B ) )
3 2 oveq2d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( A x. ( T ` B ) ) = ( A x. ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` B ) ) )
4 1 3 eqeq12d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) <-> ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` ( A .h B ) ) = ( A x. ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` B ) ) ) )
5 4 imbi2d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) ) <-> ( ( A e. CC /\ B e. ~H ) -> ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` ( A .h B ) ) = ( A x. ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` B ) ) ) ) )
6 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
7 6 elimel 
 |-  if ( T e. LinFn , T , ( ~H X. { 0 } ) ) e. LinFn
8 7 lnfnmuli 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` ( A .h B ) ) = ( A x. ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` B ) ) )
9 5 8 dedth 
 |-  ( T e. LinFn -> ( ( A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) ) )
10 9 3impib 
 |-  ( ( T e. LinFn /\ A e. CC /\ B e. ~H ) -> ( T ` ( A .h B ) ) = ( A x. ( T ` B ) ) )