Metamath Proof Explorer


Theorem idl0cl

Description: An ideal contains 0 . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idl0cl.1 G = 1 st R
idl0cl.2 Z = GId G
Assertion idl0cl R RingOps I Idl R Z I

Proof

Step Hyp Ref Expression
1 idl0cl.1 G = 1 st R
2 idl0cl.2 Z = GId G
3 eqid 2 nd R = 2 nd R
4 eqid ran G = ran G
5 1 3 4 2 isidl R RingOps I Idl R I ran G Z I x I y I x G y I z ran G z 2 nd R x I x 2 nd R z I
6 5 biimpa R RingOps I Idl R I ran G Z I x I y I x G y I z ran G z 2 nd R x I x 2 nd R z I
7 6 simp2d R RingOps I Idl R Z I