honegsubdi

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

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

Step	Hyp	Ref	Expression
1		neg1cn	$⊢ - 1 \in ℂ$
2		homulcl	$⊢ (- 1 \in ℂ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
3	1 2	mpan	$⊢ U : ℋ ⟶ ℋ \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
4		honegdi	$⊢ (T : ℋ ⟶ ℋ \land (-1 \cdot_{op} U) : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = (-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U))$
5	3 4	sylan2	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = (-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U))$
6		honegsub	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (-1 \cdot_{op} U) = T -_{op} U$
7	6	oveq2d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = -1 \cdot_{op} (T -_{op} U)$
8		honegneg	$⊢ U : ℋ ⟶ ℋ \to -1 \cdot_{op} (-1 \cdot_{op} U) = U$
9	8	adantl	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (-1 \cdot_{op} U) = U$
10	9	oveq2d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U)) = (-1 \cdot_{op} T) +_{op} U$
11	5 7 10	3eqtr3d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T -_{op} U) = (-1 \cdot_{op} T) +_{op} U$

Metamath Proof Explorer