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

Metamath Proof Explorer

Theorem honegsubdi2

Description: Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion honegsubdi2 ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 −op 𝑈 ) ) = ( 𝑈 −op 𝑇 ) )

Proof

Step Hyp Ref Expression
1 honegsubdi ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 −op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op 𝑈 ) )
2 neg1cn ⊢ - 1 ∈ ℂ
3 homulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
4 2 3 mpan ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
5 hoaddcom ⊢ ( ( ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( - 1 ·op 𝑇 ) +op 𝑈 ) = ( 𝑈 +op ( - 1 ·op 𝑇 ) ) )
6 4 5 sylan ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( - 1 ·op 𝑇 ) +op 𝑈 ) = ( 𝑈 +op ( - 1 ·op 𝑇 ) ) )
7 honegsub ⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑈 +op ( - 1 ·op 𝑇 ) ) = ( 𝑈 −op 𝑇 ) )
8 7 ancoms ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑈 +op ( - 1 ·op 𝑇 ) ) = ( 𝑈 −op 𝑇 ) )
9 1 6 8 3eqtrd ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 −op 𝑈 ) ) = ( 𝑈 −op 𝑇 ) )