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

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