This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ −ℎ : ( ℋ × ℋ ) ⟶ ℋ