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 )