Metamath Proof Explorer

Theorem rngoidl

Description: A ring R is an R ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses rngidl.1 
|- G = ( 1st ` R )
rngidl.2 
|- X = ran G
Assertion rngoidl 
|- ( R e. RingOps -> X e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 rngidl.1 
 |-  G = ( 1st ` R )
2 rngidl.2 
 |-  X = ran G
3 ssidd 
 |-  ( R e. RingOps -> X C_ X )
4 eqid 
 |-  ( GId ` G ) = ( GId ` G )
5 1 2 4 rngo0cl 
 |-  ( R e. RingOps -> ( GId ` G ) e. X )
6 1 2 rngogcl 
 |-  ( ( R e. RingOps /\ x e. X /\ y e. X ) -> ( x G y ) e. X )
7 6 3expa 
 |-  ( ( ( R e. RingOps /\ x e. X ) /\ y e. X ) -> ( x G y ) e. X )
8 7 ralrimiva 
 |-  ( ( R e. RingOps /\ x e. X ) -> A. y e. X ( x G y ) e. X )
9 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
10 1 9 2 rngocl 
 |-  ( ( R e. RingOps /\ z e. X /\ x e. X ) -> ( z ( 2nd ` R ) x ) e. X )
11 10 3com23 
 |-  ( ( R e. RingOps /\ x e. X /\ z e. X ) -> ( z ( 2nd ` R ) x ) e. X )
12 1 9 2 rngocl 
 |-  ( ( R e. RingOps /\ x e. X /\ z e. X ) -> ( x ( 2nd ` R ) z ) e. X )
13 11 12 jca 
 |-  ( ( R e. RingOps /\ x e. X /\ z e. X ) -> ( ( z ( 2nd ` R ) x ) e. X /\ ( x ( 2nd ` R ) z ) e. X ) )
14 13 3expa 
 |-  ( ( ( R e. RingOps /\ x e. X ) /\ z e. X ) -> ( ( z ( 2nd ` R ) x ) e. X /\ ( x ( 2nd ` R ) z ) e. X ) )
15 14 ralrimiva 
 |-  ( ( R e. RingOps /\ x e. X ) -> A. z e. X ( ( z ( 2nd ` R ) x ) e. X /\ ( x ( 2nd ` R ) z ) e. X ) )
16 8 15 jca 
 |-  ( ( R e. RingOps /\ x e. X ) -> ( A. y e. X ( x G y ) e. X /\ A. z e. X ( ( z ( 2nd ` R ) x ) e. X /\ ( x ( 2nd ` R ) z ) e. X ) ) )
17 16 ralrimiva 
 |-  ( R e. RingOps -> A. x e. X ( A. y e. X ( x G y ) e. X /\ A. z e. X ( ( z ( 2nd ` R ) x ) e. X /\ ( x ( 2nd ` R ) z ) e. X ) ) )
18 1 9 2 4 isidl 
 |-  ( R e. RingOps -> ( X e. ( Idl ` R ) <-> ( X C_ X /\ ( GId ` G ) e. X /\ A. x e. X ( A. y e. X ( x G y ) e. X /\ A. z e. X ( ( z ( 2nd ` R ) x ) e. X /\ ( x ( 2nd ` R ) z ) e. X ) ) ) ) )
19 3 5 17 18 mpbir3and 
 |-  ( R e. RingOps -> X e. ( Idl ` R ) )