# 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 ( ( 𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 fveq1 ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 · 𝐵 ) ) )
2 fveq1 ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇𝐵 ) = ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) )
3 2 oveq2d ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝐴 · ( 𝑇𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) )
4 1 3 eqeq12d ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) ↔ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) ) )
5 4 imbi2d ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) ) ) )
6 0lnfn ( ℋ × { 0 } ) ∈ LinFn
7 6 elimel if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
8 7 lnfnmuli ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 𝐵 ) ) )
9 5 8 dedth ( 𝑇 ∈ LinFn → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) ) )
10 9 3impib ( ( 𝑇 ∈ LinFn ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( 𝑇𝐵 ) ) )