Theorem nvgf

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

	Ref	Expression
Hypotheses	nvgf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvgf.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
Assertion	nvgf	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		nvgf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvgf.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3	2	nvgrp	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )
4	1 2	bafval	⊢ 𝑋 = ran 𝐺
5	4	grpofo	⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )
6		fof	⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
7	3 5 6	3syl	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )