# Metamath Proof Explorer

## 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 ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\to {T}{-}_{\mathrm{op}}{U}\in \mathrm{HrmOp}$

### Proof

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