Metamath Proof Explorer


Theorem lnfnaddi

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

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

Proof

Step Hyp Ref Expression
1 lnfnl.1 𝑇 ∈ LinFn
2 ax-1cn 1 ∈ ℂ
3 1 lnfnli ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 · 𝐴 ) + 𝐵 ) ) = ( ( 1 · ( 𝑇𝐴 ) ) + ( 𝑇𝐵 ) ) )
4 2 3 mp3an1 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 · 𝐴 ) + 𝐵 ) ) = ( ( 1 · ( 𝑇𝐴 ) ) + ( 𝑇𝐵 ) ) )
5 ax-hvmulid ( 𝐴 ∈ ℋ → ( 1 · 𝐴 ) = 𝐴 )
6 5 fvoveq1d ( 𝐴 ∈ ℋ → ( 𝑇 ‘ ( ( 1 · 𝐴 ) + 𝐵 ) ) = ( 𝑇 ‘ ( 𝐴 + 𝐵 ) ) )
7 6 adantr ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 · 𝐴 ) + 𝐵 ) ) = ( 𝑇 ‘ ( 𝐴 + 𝐵 ) ) )
8 1 lnfnfi 𝑇 : ℋ ⟶ ℂ
9 8 ffvelrni ( 𝐴 ∈ ℋ → ( 𝑇𝐴 ) ∈ ℂ )
10 9 mulid2d ( 𝐴 ∈ ℋ → ( 1 · ( 𝑇𝐴 ) ) = ( 𝑇𝐴 ) )
11 10 adantr ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 1 · ( 𝑇𝐴 ) ) = ( 𝑇𝐴 ) )
12 11 oveq1d ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 1 · ( 𝑇𝐴 ) ) + ( 𝑇𝐵 ) ) = ( ( 𝑇𝐴 ) + ( 𝑇𝐵 ) ) )
13 4 7 12 3eqtr3d ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝑇𝐴 ) + ( 𝑇𝐵 ) ) )