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 THrmOpUHrmOpT-opUHrmOp

Proof

Step Hyp Ref Expression
1 hmopf THrmOpT:
2 hmopf UHrmOpU:
3 honegsub T:U:T+op-1·opU=T-opU
4 1 2 3 syl2an THrmOpUHrmOpT+op-1·opU=T-opU
5 neg1rr 1
6 hmopm 1UHrmOp-1·opUHrmOp
7 5 6 mpan UHrmOp-1·opUHrmOp
8 hmops THrmOp-1·opUHrmOpT+op-1·opUHrmOp
9 7 8 sylan2 THrmOpUHrmOpT+op-1·opUHrmOp
10 4 9 eqeltrrd THrmOpUHrmOpT-opUHrmOp