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

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 ⊢ T ∈ LinOp
Assertion lnopaddi ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ B = T ⁡ A + ℎ T ⁡ B

Proof

Step Hyp Ref Expression
1 lnopl.1 ⊢ T ∈ LinOp
2 ax-1cn ⊢ 1 ∈ ℂ
3 1 lnopli ⊢ 1 ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = 1 ⋅ ℎ T ⁡ A + ℎ T ⁡ B
4 2 3 mp3an1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = 1 ⋅ ℎ T ⁡ A + ℎ T ⁡ B
5 ax-hvmulid ⊢ A ∈ ℋ → 1 ⋅ ℎ A = A
6 5 fvoveq1d ⊢ A ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = T ⁡ A + ℎ B
7 6 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = T ⁡ A + ℎ B
8 1 lnopfi ⊢ T : ℋ ⟶ ℋ
9 8 ffvelcdmi ⊢ A ∈ ℋ → T ⁡ A ∈ ℋ
10 ax-hvmulid ⊢ T ⁡ A ∈ ℋ → 1 ⋅ ℎ T ⁡ A = T ⁡ A
11 9 10 syl ⊢ A ∈ ℋ → 1 ⋅ ℎ T ⁡ A = T ⁡ A
12 11 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ → 1 ⋅ ℎ T ⁡ A = T ⁡ A
13 12 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → 1 ⋅ ℎ T ⁡ A + ℎ T ⁡ B = T ⁡ A + ℎ T ⁡ B
14 4 7 13 3eqtr3d ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ B = T ⁡ A + ℎ T ⁡ B