Theorem hoaddid1i

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hoaddid1.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hoaddid1i	$$⊢T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
3		hosval	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge 0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)\left(x\right)=T\left(x\right){+}_{ℎ}{0}_{\mathrm{hop}}\left(x\right)$$
4	1 2 3	mp3an12	$$⊢x\in \mathscr{H}\to \left(T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)\left(x\right)=T\left(x\right){+}_{ℎ}{0}_{\mathrm{hop}}\left(x\right)$$
5		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
6	5	oveq2d	$$⊢x\in \mathscr{H}\to T\left(x\right){+}_{ℎ}{0}_{\mathrm{hop}}\left(x\right)=T\left(x\right){+}_{ℎ}{0}_{ℎ}$$
7	1	ffvelrni	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
8		ax-hvaddid	$$⊢T\left(x\right)\in \mathscr{H}\to T\left(x\right){+}_{ℎ}{0}_{ℎ}=T\left(x\right)$$
9	7 8	syl	$$⊢x\in \mathscr{H}\to T\left(x\right){+}_{ℎ}{0}_{ℎ}=T\left(x\right)$$
10	4 6 9	3eqtrd	$$⊢x\in \mathscr{H}\to \left(T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)\left(x\right)=T\left(x\right)$$
11	10	rgen	$$⊢\forall x\in \mathscr{H}\left(T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)\left(x\right)=T\left(x\right)$$
12	1 2	hoaddcli	$$⊢\left(T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
13	12 1	hoeqi	$$⊢\forall x\in \mathscr{H}\left(T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right)\left(x\right)=T\left(x\right)\leftrightarrow T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$
14	11 13	mpbi	$$⊢T{+}_{\mathrm{op}}{0}_{\mathrm{hop}}=T$$