Theorem idl0cl

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

	Ref	Expression
Hypotheses	idl0cl.1	|- G = ( 1st ` R )
	idl0cl.2	|- Z = ( GId ` G )
Assertion	idl0cl	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> Z e. I )

Proof

Step	Hyp	Ref	Expression
1		idl0cl.1	|- G = ( 1st ` R )
2		idl0cl.2	|- Z = ( GId ` G )
3		eqid	|- ( 2nd ` R ) = ( 2nd ` R )
4		eqid	|- ran G = ran G
5	1 3 4 2	isidl	|- ( R e. RingOps -> ( I e. ( Idl ` R ) <-> ( I C_ ran G /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) ) ) )
6	5	biimpa	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( I C_ ran G /\ Z e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. I /\ ( x ( 2nd ` R ) z ) e. I ) ) ) )
7	6	simp2d	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> Z e. I )