Metamath Proof Explorer


Theorem lnopaddi

Description: Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 𝑇 ∈ LinOp
Assertion lnopaddi ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝑇𝐴 ) + ( 𝑇𝐵 ) ) )

Proof

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