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 ⊢ 𝑇 ∈ 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 ffvelcdmi ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
10 ax-hvmulid ⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → ( 1 ·ℎ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑇 ‘ 𝐴 ) )
11 9 10 syl ⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑇 ‘ 𝐴 ) )
12 11 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 1 ·ℎ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑇 ‘ 𝐴 ) )
13 12 oveq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 1 ·ℎ ( 𝑇 ‘ 𝐴 ) ) +ℎ ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) )
14 4 7 13 3eqtr3d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( 𝑇 ‘ 𝐵 ) ) )