Theorem hoaddid1

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:\mathscr{H}⟶\mathscr{H}\to T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$

Proof

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