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	|- X = ( BaseSet ` U )
	nv0id.2	|- G = ( +v ` U )
	nv0id.6	|- Z = ( 0vec ` U )
Assertion	nv0rid	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G Z ) = A )

Proof

Step	Hyp	Ref	Expression
1		nv0id.1	|- X = ( BaseSet ` U )
2		nv0id.2	|- G = ( +v ` U )
3		nv0id.6	|- Z = ( 0vec ` U )
4	2 3	0vfval	|- ( U e. NrmCVec -> Z = ( GId ` G ) )
5	4	oveq2d	|- ( U e. NrmCVec -> ( A G Z ) = ( A G ( GId ` G ) ) )
6	5	adantr	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G Z ) = ( A G ( GId ` G ) ) )
7	2	nvgrp	|- ( U e. NrmCVec -> G e. GrpOp )
8	1 2	bafval	|- X = ran G
9		eqid	|- ( GId ` G ) = ( GId ` G )
10	8 9	grporid	|- ( ( G e. GrpOp /\ A e. X ) -> ( A G ( GId ` G ) ) = A )
11	7 10	sylan	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( GId ` G ) ) = A )
12	6 11	eqtrd	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G Z ) = A )