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

Metamath Proof Explorer

Theorem nvgf

Description: Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvgf.1 ⊢ X = BaseSet ⁡ U
nvgf.2 ⊢ G = + v ⁡ U
Assertion nvgf ⊢ U ∈ NrmCVec → G : X × X ⟶ X

Proof

Step Hyp Ref Expression
1 nvgf.1 ⊢ X = BaseSet ⁡ U
2 nvgf.2 ⊢ G = + v ⁡ U
3 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
4 1 2 bafval ⊢ X = ran ⁡ G
5 4 grpofo ⊢ G ∈ GrpOp → G : X × X ⟶ onto X
6 fof ⊢ G : X × X ⟶ onto X → G : X × X ⟶ X
7 3 5 6 3syl ⊢ U ∈ NrmCVec → G : X × X ⟶ X