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

Metamath Proof Explorer

Theorem nv0rid

Description: The zero vector is a right 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	⊢ 𝑍 = ( 0_vec ‘ 𝑈 )
	Assertion	nv0rid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 )

Proof

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