Theorem hmopd

Description: The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hmopd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 −op 𝑈 ) ∈ HrmOp )

Proof

Step	Hyp	Ref	Expression
1		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
2		hmopf	⊢ ( 𝑈 ∈ HrmOp → 𝑈 : ℋ ⟶ ℋ )
3		honegsub	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 −op 𝑈 ) )
4	1 2 3	syl2an	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 −op 𝑈 ) )
5		neg1rr	⊢ - 1 ∈ ℝ
6		hmopm	⊢ ( ( - 1 ∈ ℝ ∧ 𝑈 ∈ HrmOp ) → ( - 1 ·op 𝑈 ) ∈ HrmOp )
7	5 6	mpan	⊢ ( 𝑈 ∈ HrmOp → ( - 1 ·op 𝑈 ) ∈ HrmOp )
8		hmops	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( - 1 ·op 𝑈 ) ∈ HrmOp ) → ( 𝑇 +op ( - 1 ·op 𝑈 ) ) ∈ HrmOp )
9	7 8	sylan2	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 +op ( - 1 ·op 𝑈 ) ) ∈ HrmOp )
10	4 9	eqeltrrd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 −op 𝑈 ) ∈ HrmOp )