Metamath Proof Explorer


Theorem rngo0lid

Description: The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ring0cl.1
|- G = ( 1st ` R )
ring0cl.2
|- X = ran G
ring0cl.3
|- Z = ( GId ` G )
Assertion rngo0lid
|- ( ( R e. RingOps /\ A e. X ) -> ( Z G A ) = A )

Proof

Step Hyp Ref Expression
1 ring0cl.1
 |-  G = ( 1st ` R )
2 ring0cl.2
 |-  X = ran G
3 ring0cl.3
 |-  Z = ( GId ` G )
4 1 rngogrpo
 |-  ( R e. RingOps -> G e. GrpOp )
5 2 3 grpolid
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( Z G A ) = A )
6 4 5 sylan
 |-  ( ( R e. RingOps /\ A e. X ) -> ( Z G A ) = A )