Theorem honegneg

Description: Double negative of a Hilbert space operator. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	honegneg	$$⊢T:\mathscr{H}⟶\mathscr{H}\to -1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		neg1mulneg1e1	$$⊢-1-1=1$$
2	1	oveq1i	$$⊢-1-1{·}_{\mathrm{op}}T=1{·}_{\mathrm{op}}T$$
3		neg1cn	$$⊢-1\in ℂ$$
4		homulass	$$⊢\left(-1\in ℂ\wedge -1\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to -1-1{·}_{\mathrm{op}}T=-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)$$
5	3 3 4	mp3an12	$$⊢T:\mathscr{H}⟶\mathscr{H}\to -1-1{·}_{\mathrm{op}}T=-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)$$
6		homullid	$$⊢T:\mathscr{H}⟶\mathscr{H}\to 1{·}_{\mathrm{op}}T=T$$
7	2 5 6	3eqtr3a	$$⊢T:\mathscr{H}⟶\mathscr{H}\to -1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=T$$