hvsubf

Description: Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	hvsubf	$⊢ -_{ℎ} : ℋ \times ℋ ⟶ ℋ$

Step	Hyp	Ref	Expression
1		neg1cn	$⊢ - 1 \in ℂ$
2		hvmulcl	$⊢ (- 1 \in ℂ \land y \in ℋ) \to -1 \cdot_{ℎ} y \in ℋ$
3	1 2	mpan	$⊢ y \in ℋ \to -1 \cdot_{ℎ} y \in ℋ$
4		hvaddcl	$⊢ (x \in ℋ \land -1 \cdot_{ℎ} y \in ℋ) \to x +_{ℎ} (-1 \cdot_{ℎ} y) \in ℋ$
5	3 4	sylan2	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} (-1 \cdot_{ℎ} y) \in ℋ$
6	5	rgen2	$⊢ \forall x \in ℋ \forall y \in ℋ x +_{ℎ} (-1 \cdot_{ℎ} y) \in ℋ$
7		df-hvsub	$⊢ -_{ℎ} = (x \in ℋ, y \in ℋ ⟼ x +_{ℎ} (-1 \cdot_{ℎ} y))$
8	7	fmpo	$⊢ \forall x \in ℋ \forall y \in ℋ x +_{ℎ} (-1 \cdot_{ℎ} y) \in ℋ \leftrightarrow -_{ℎ} : ℋ \times ℋ ⟶ ℋ$
9	6 8	mpbi	$⊢ -_{ℎ} : ℋ \times ℋ ⟶ ℋ$

Metamath Proof Explorer