hosubneg

Description: Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hosubneg	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T -_{op} (-1 \cdot_{op} U) = 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		honegsub	$⊢ (T : ℋ ⟶ ℋ \land (-1 \cdot_{op} U) : ℋ ⟶ ℋ) \to T +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U)) = T -_{op} (-1 \cdot_{op} U)$
5	3 4	sylan2	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U)) = T -_{op} (-1 \cdot_{op} U)$
6		honegneg	$⊢ U : ℋ ⟶ ℋ \to -1 \cdot_{op} (-1 \cdot_{op} U) = U$
7	6	oveq2d	$⊢ U : ℋ ⟶ ℋ \to T +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U)) = T +_{op} U$
8	7	adantl	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (-1 \cdot_{op} (-1 \cdot_{op} U)) = T +_{op} U$
9	5 8	eqtr3d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T -_{op} (-1 \cdot_{op} U) = T +_{op} U$

Metamath Proof Explorer