# 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 ${⊢}{T}:ℋ⟶ℋ\to 2{·}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}{T}$

### Proof

Step Hyp Ref Expression
1 df-2 ${⊢}2=1+1$
2 1 oveq1i ${⊢}2{·}_{\mathrm{op}}{T}=\left(1+1\right){·}_{\mathrm{op}}{T}$
3 ax-1cn ${⊢}1\in ℂ$
4 hoadddir ${⊢}\left(1\in ℂ\wedge 1\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left(1+1\right){·}_{\mathrm{op}}{T}=\left(1{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(1{·}_{\mathrm{op}}{T}\right)$
5 3 3 4 mp3an12 ${⊢}{T}:ℋ⟶ℋ\to \left(1+1\right){·}_{\mathrm{op}}{T}=\left(1{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(1{·}_{\mathrm{op}}{T}\right)$
6 2 5 syl5eq ${⊢}{T}:ℋ⟶ℋ\to 2{·}_{\mathrm{op}}{T}=\left(1{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(1{·}_{\mathrm{op}}{T}\right)$
7 hoadddi ${⊢}\left(1\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to 1{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{T}\right)=\left(1{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(1{·}_{\mathrm{op}}{T}\right)$
8 3 7 mp3an1 ${⊢}\left({T}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to 1{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{T}\right)=\left(1{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(1{·}_{\mathrm{op}}{T}\right)$
9 8 anidms ${⊢}{T}:ℋ⟶ℋ\to 1{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{T}\right)=\left(1{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(1{·}_{\mathrm{op}}{T}\right)$
10 hoaddcl ${⊢}\left({T}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({T}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
11 10 anidms ${⊢}{T}:ℋ⟶ℋ\to \left({T}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
12 homulid2 ${⊢}\left({T}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to 1{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{T}\right)={T}{+}_{\mathrm{op}}{T}$
13 11 12 syl ${⊢}{T}:ℋ⟶ℋ\to 1{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{T}\right)={T}{+}_{\mathrm{op}}{T}$
14 6 9 13 3eqtr2d ${⊢}{T}:ℋ⟶ℋ\to 2{·}_{\mathrm{op}}{T}={T}{+}_{\mathrm{op}}{T}$