# 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 ) ) )`