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	|- X = ( BaseSet ` U )
	nv0id.2	|- G = ( +v ` U )
	nv0id.6	|- Z = ( 0vec ` U )
Assertion	nv0lid	|- ( ( U e. NrmCVec /\ A e. X ) -> ( Z G A ) = 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	oveq1d	|- ( U e. NrmCVec -> ( Z G A ) = ( ( GId ` G ) G A ) )
6	5	adantr	|- ( ( U e. NrmCVec /\ A e. X ) -> ( Z G A ) = ( ( GId ` G ) G A ) )
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	grpolid	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( GId ` G ) G A ) = A )
11	7 10	sylan	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( GId ` G ) G A ) = A )
12	6 11	eqtrd	|- ( ( U e. NrmCVec /\ A e. X ) -> ( Z G A ) = A )