Theorem nv0lid

Description: The zero vector is a left identity element. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nv0id.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nv0id.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	nv0id.6	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
Assertion	nv0lid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑍 𝐺 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nv0id.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nv0id.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		nv0id.6	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
4	2 3	0vfval	⊢ ( 𝑈 ∈ NrmCVec → 𝑍 = ( GId ‘ 𝐺 ) )
5	4	oveq1d	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑍 𝐺 𝐴 ) = ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) )
6	5	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑍 𝐺 𝐴 ) = ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) )
7	2	nvgrp	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )
8	1 2	bafval	⊢ 𝑋 = ran 𝐺
9		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
10	8 9	grpolid	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) = 𝐴 )
11	7 10	sylan	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) = 𝐴 )
12	6 11	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑍 𝐺 𝐴 ) = 𝐴 )