Metamath Proof Explorer


Theorem lnfnaddmuli

Description: Sum/product property of a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 𝑇 ∈ LinFn
Assertion lnfnaddmuli ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 + ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝐴 · ( 𝑇𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 lnfnl.1 𝑇 ∈ LinFn
2 hvmulcl ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 · 𝐶 ) ∈ ℋ )
3 1 lnfnaddi ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 · 𝐶 ) ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 + ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
4 2 3 sylan2 ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) ) → ( 𝑇 ‘ ( 𝐵 + ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
5 4 3impb ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 + ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
6 5 3com12 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 + ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
7 1 lnfnmuli ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) = ( 𝐴 · ( 𝑇𝐶 ) ) )
8 7 3adant2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) = ( 𝐴 · ( 𝑇𝐶 ) ) )
9 8 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇𝐵 ) + ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝐴 · ( 𝑇𝐶 ) ) ) )
10 6 9 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 + ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) + ( 𝐴 · ( 𝑇𝐶 ) ) ) )