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 ∈ HrmOp ∧ U ∈ HrmOp → T - op U ∈ HrmOp

Proof

Step Hyp Ref Expression
1 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
2 hmopf ⊢ U ∈ HrmOp → U : ℋ ⟶ ℋ
3 honegsub ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ → T + op -1 · op U = T - op U
4 1 2 3 syl2an ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T + op -1 · op U = T - op U
5 neg1rr ⊢ − 1 ∈ ℝ
6 hmopm ⊢ − 1 ∈ ℝ ∧ U ∈ HrmOp → -1 · op U ∈ HrmOp
7 5 6 mpan ⊢ U ∈ HrmOp → -1 · op U ∈ HrmOp
8 hmops ⊢ T ∈ HrmOp ∧ -1 · op U ∈ HrmOp → T + op -1 · op U ∈ HrmOp
9 7 8 sylan2 ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T + op -1 · op U ∈ HrmOp
10 4 9 eqeltrrd ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T - op U ∈ HrmOp