# 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
`|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T -op U ) e. HrmOp )`

### Proof

Step Hyp Ref Expression
1 hmopf
` |-  ( T e. HrmOp -> T : ~H --> ~H )`
2 hmopf
` |-  ( U e. HrmOp -> U : ~H --> ~H )`
3 honegsub
` |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )`
4 1 2 3 syl2an
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )`
5 neg1rr
` |-  -u 1 e. RR`
6 hmopm
` |-  ( ( -u 1 e. RR /\ U e. HrmOp ) -> ( -u 1 .op U ) e. HrmOp )`
7 5 6 mpan
` |-  ( U e. HrmOp -> ( -u 1 .op U ) e. HrmOp )`
8 hmops
` |-  ( ( T e. HrmOp /\ ( -u 1 .op U ) e. HrmOp ) -> ( T +op ( -u 1 .op U ) ) e. HrmOp )`
9 7 8 sylan2
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op ( -u 1 .op U ) ) e. HrmOp )`
10 4 9 eqeltrrd
` |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T -op U ) e. HrmOp )`