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 
|- 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 )