Theorem ho2times

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

	Ref	Expression
Assertion	ho2times	$$⊢T:\mathscr{H}⟶\mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\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	eqtrid	$$⊢T:\mathscr{H}⟶\mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\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:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(T{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
11	10	anidms	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(T{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
12		homullid	$$⊢\left(T{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\to 1{·}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}T\right)=T{+}_{\mathrm{op}}T$$
13	11 12	syl	$$⊢T:\mathscr{H}⟶\mathscr{H}\to 1{·}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}T\right)=T{+}_{\mathrm{op}}T$$
14	6 9 13	3eqtr2d	$$⊢T:\mathscr{H}⟶\mathscr{H}\to 2{·}_{\mathrm{op}}T=T{+}_{\mathrm{op}}T$$