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 )