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

Metamath Proof Explorer

Theorem lnfnmuli

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

Ref Expression
Hypothesis lnfnl.1 ⊢ 𝑇 ∈ LinFn
Assertion lnfnmuli ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ 𝑇 ∈ LinFn
2 ax-hv0cl ⊢ 0ℎ ∈ ℋ
3 1 lnfnli ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 0ℎ ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 0ℎ ) ) = ( ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) + ( 𝑇 ‘ 0ℎ ) ) )
4 2 3 mp3an3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 0ℎ ) ) = ( ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) + ( 𝑇 ‘ 0ℎ ) ) )
5 hvmulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ )
6 ax-hvaddid ⊢ ( ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ → ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 0ℎ ) = ( 𝐴 ·ℎ 𝐵 ) )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 0ℎ ) = ( 𝐴 ·ℎ 𝐵 ) )
8 7 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝐴 ·ℎ 𝐵 ) +ℎ 0ℎ ) ) = ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) )
9 1 lnfn0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0
10 9 oveq2i ⊢ ( ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) + ( 𝑇 ‘ 0ℎ ) ) = ( ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) + 0 )
11 1 lnfnfi ⊢ 𝑇 : ℋ ⟶ ℂ
12 11 ffvelcdmi ⊢ ( 𝐵 ∈ ℋ → ( 𝑇 ‘ 𝐵 ) ∈ ℂ )
13 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) ∈ ℂ )
14 12 13 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) ∈ ℂ )
15 14 addridd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) + 0 ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )
16 10 15 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) + ( 𝑇 ‘ 0ℎ ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )
17 4 8 16 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )