This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 −op 𝑈 ) ∈ HrmOp )

Proof

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