honegsubdi2

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

		Ref	Expression
	Assertion	honegsubdi2	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T -_{op} U) = U -_{op} T$

Step	Hyp	Ref	Expression
1		honegsubdi	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T -_{op} U) = (-1 \cdot_{op} T) +_{op} U$
2		neg1cn	$⊢ - 1 \in ℂ$
3		homulcl	$⊢ (- 1 \in ℂ \land T : ℋ ⟶ ℋ) \to (-1 \cdot_{op} T) : ℋ ⟶ ℋ$
4	2 3	mpan	$⊢ T : ℋ ⟶ ℋ \to (-1 \cdot_{op} T) : ℋ ⟶ ℋ$
5		hoaddcom	$⊢ ((-1 \cdot_{op} T) : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} T) +_{op} U = U +_{op} (-1 \cdot_{op} T)$
6	4 5	sylan	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} T) +_{op} U = U +_{op} (-1 \cdot_{op} T)$
7		honegsub	$⊢ (U : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to U +_{op} (-1 \cdot_{op} T) = U -_{op} T$
8	7	ancoms	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to U +_{op} (-1 \cdot_{op} T) = U -_{op} T$
9	1 6 8	3eqtrd	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T -_{op} U) = U -_{op} T$

Metamath Proof Explorer