Theorem hvsubf

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

	Ref	Expression
Assertion	hvsubf	⊢ −ℎ : ( ℋ × ℋ ) ⟶ ℋ

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( - 1 ·ℎ 𝑦 ) ∈ ℋ )
3	1 2	mpan	⊢ ( 𝑦 ∈ ℋ → ( - 1 ·ℎ 𝑦 ) ∈ ℋ )
4		hvaddcl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( - 1 ·ℎ 𝑦 ) ∈ ℋ ) → ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ∈ ℋ )
5	3 4	sylan2	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ∈ ℋ )
6	5	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ∈ ℋ
7		df-hvsub	⊢ −ℎ = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
8	7	fmpo	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ∈ ℋ ↔ −ℎ : ( ℋ × ℋ ) ⟶ ℋ )
9	6 8	mpbi	⊢ −ℎ : ( ℋ × ℋ ) ⟶ ℋ