Theorem honegneg

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

	Ref	Expression
Assertion	honegneg	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( - 1 ·op ( - 1 ·op 𝑇 ) ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
2	1	oveq1i	⊢ ( ( - 1 · - 1 ) ·op 𝑇 ) = ( 1 ·op 𝑇 )
3		neg1cn	⊢ - 1 ∈ ℂ
4		homulass	⊢ ( ( - 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( - 1 · - 1 ) ·op 𝑇 ) = ( - 1 ·op ( - 1 ·op 𝑇 ) ) )
5	3 3 4	mp3an12	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( - 1 · - 1 ) ·op 𝑇 ) = ( - 1 ·op ( - 1 ·op 𝑇 ) ) )
6		homulid2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op 𝑇 ) = 𝑇 )
7	2 5 6	3eqtr3a	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( - 1 ·op ( - 1 ·op 𝑇 ) ) = 𝑇 )