Description: The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hmopd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hmopf | |
|
2 | hmopf | |
|
3 | honegsub | |
|
4 | 1 2 3 | syl2an | |
5 | neg1rr | |
|
6 | hmopm | |
|
7 | 5 6 | mpan | |
8 | hmops | |
|
9 | 7 8 | sylan2 | |
10 | 4 9 | eqeltrrd | |