hmopd

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

		Ref	Expression
	Assertion	hmopd	$⊢ (T \in HrmOp \land U \in HrmOp) \to T -_{op} U \in HrmOp$

Step	Hyp	Ref	Expression
1		hmopf	$⊢ T \in HrmOp \to T : ℋ ⟶ ℋ$
2		hmopf	$⊢ U \in HrmOp \to U : ℋ ⟶ ℋ$
3		honegsub	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (-1 \cdot_{op} U) = T -_{op} U$
4	1 2 3	syl2an	$⊢ (T \in HrmOp \land U \in HrmOp) \to T +_{op} (-1 \cdot_{op} U) = T -_{op} U$
5		neg1rr	$⊢ - 1 \in ℝ$
6		hmopm	$⊢ (- 1 \in ℝ \land U \in HrmOp) \to -1 \cdot_{op} U \in HrmOp$
7	5 6	mpan	$⊢ U \in HrmOp \to -1 \cdot_{op} U \in HrmOp$
8		hmops	$⊢ (T \in HrmOp \land -1 \cdot_{op} U \in HrmOp) \to T +_{op} (-1 \cdot_{op} U) \in HrmOp$
9	7 8	sylan2	$⊢ (T \in HrmOp \land U \in HrmOp) \to T +_{op} (-1 \cdot_{op} U) \in HrmOp$
10	4 9	eqeltrrd	$⊢ (T \in HrmOp \land U \in HrmOp) \to T -_{op} U \in HrmOp$

Metamath Proof Explorer