Metamath Proof Explorer

Theorem ho2times

Description: Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion ho2times ( 𝑇 : ℋ ⟶ ℋ → ( 2 ·op 𝑇 ) = ( 𝑇 +op 𝑇 ) )

Proof

Step Hyp Ref Expression
1 df-2 ⊢ 2 = ( 1 + 1 )
2 1 oveq1i ⊢ ( 2 ·op 𝑇 ) = ( ( 1 + 1 ) ·op 𝑇 )
3 ax-1cn ⊢ 1 ∈ ℂ
4 hoadddir ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 1 + 1 ) ·op 𝑇 ) = ( ( 1 ·op 𝑇 ) +op ( 1 ·op 𝑇 ) ) )
5 3 3 4 mp3an12 ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( 1 + 1 ) ·op 𝑇 ) = ( ( 1 ·op 𝑇 ) +op ( 1 ·op 𝑇 ) ) )
6 2 5 eqtrid ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 2 ·op 𝑇 ) = ( ( 1 ·op 𝑇 ) +op ( 1 ·op 𝑇 ) ) )
7 hoadddi ⊢ ( ( 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 1 ·op ( 𝑇 +op 𝑇 ) ) = ( ( 1 ·op 𝑇 ) +op ( 1 ·op 𝑇 ) ) )
8 3 7 mp3an1 ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 1 ·op ( 𝑇 +op 𝑇 ) ) = ( ( 1 ·op 𝑇 ) +op ( 1 ·op 𝑇 ) ) )
9 8 anidms ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op ( 𝑇 +op 𝑇 ) ) = ( ( 1 ·op 𝑇 ) +op ( 1 ·op 𝑇 ) ) )
10 hoaddcl ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑇 +op 𝑇 ) : ℋ ⟶ ℋ )
11 10 anidms ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 +op 𝑇 ) : ℋ ⟶ ℋ )
12 homullid ⊢ ( ( 𝑇 +op 𝑇 ) : ℋ ⟶ ℋ → ( 1 ·op ( 𝑇 +op 𝑇 ) ) = ( 𝑇 +op 𝑇 ) )
13 11 12 syl ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op ( 𝑇 +op 𝑇 ) ) = ( 𝑇 +op 𝑇 ) )
14 6 9 13 3eqtr2d ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 2 ·op 𝑇 ) = ( 𝑇 +op 𝑇 ) )