Metamath Proof Explorer

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hoaddid1 ${⊢}{T}:ℋ⟶ℋ\to {T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}$

Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to {T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}$
2 id ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to {T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
3 1 2 eqeq12d ${⊢}{T}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\to \left({T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}↔if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)\right)$
4 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
5 4 elimf ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
6 5 hoaddid1i ${⊢}if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}=if\left({T}:ℋ⟶ℋ,{T},{0}_{\mathrm{hop}}\right)$
7 3 6 dedth ${⊢}{T}:ℋ⟶ℋ\to {T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}$