Metamath Proof Explorer


Theorem rngo0cl

Description: A ring has an additive 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 rngo0cl
|- ( R e. RingOps -> Z e. X )

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 grpoidcl
 |-  ( G e. GrpOp -> Z e. X )
6 4 5 syl
 |-  ( R e. RingOps -> Z e. X )