Metamath Proof Explorer

Theorem 0idl

Description: The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses 0idl.1 
|- G = ( 1st ` R )
0idl.2 
|- Z = ( GId ` G )
Assertion 0idl 
|- ( R e. RingOps -> { Z } e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 0idl.1 
 |-  G = ( 1st ` R )
2 0idl.2 
 |-  Z = ( GId ` G )
3 eqid 
 |-  ran G = ran G
4 1 3 2 rngo0cl 
 |-  ( R e. RingOps -> Z e. ran G )
5 4 snssd 
 |-  ( R e. RingOps -> { Z } C_ ran G )
6 2 fvexi 
 |-  Z e. _V
7 6 snid 
 |-  Z e. { Z }
8 7 a1i 
 |-  ( R e. RingOps -> Z e. { Z } )
9 velsn 
 |-  ( x e. { Z } <-> x = Z )
10 velsn 
 |-  ( y e. { Z } <-> y = Z )
11 1 3 2 rngo0rid 
 |-  ( ( R e. RingOps /\ Z e. ran G ) -> ( Z G Z ) = Z )
12 4 11 mpdan 
 |-  ( R e. RingOps -> ( Z G Z ) = Z )
13 ovex 
 |-  ( Z G Z ) e. _V
14 13 elsn 
 |-  ( ( Z G Z ) e. { Z } <-> ( Z G Z ) = Z )
15 12 14 sylibr 
 |-  ( R e. RingOps -> ( Z G Z ) e. { Z } )
16 oveq2 
 |-  ( y = Z -> ( Z G y ) = ( Z G Z ) )
17 16 eleq1d 
 |-  ( y = Z -> ( ( Z G y ) e. { Z } <-> ( Z G Z ) e. { Z } ) )
18 15 17 syl5ibrcom 
 |-  ( R e. RingOps -> ( y = Z -> ( Z G y ) e. { Z } ) )
19 10 18 biimtrid 
 |-  ( R e. RingOps -> ( y e. { Z } -> ( Z G y ) e. { Z } ) )
20 19 ralrimiv 
 |-  ( R e. RingOps -> A. y e. { Z } ( Z G y ) e. { Z } )
21 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
22 2 3 1 21 rngorz 
 |-  ( ( R e. RingOps /\ z e. ran G ) -> ( z ( 2nd ` R ) Z ) = Z )
23 ovex 
 |-  ( z ( 2nd ` R ) Z ) e. _V
24 23 elsn 
 |-  ( ( z ( 2nd ` R ) Z ) e. { Z } <-> ( z ( 2nd ` R ) Z ) = Z )
25 22 24 sylibr 
 |-  ( ( R e. RingOps /\ z e. ran G ) -> ( z ( 2nd ` R ) Z ) e. { Z } )
26 2 3 1 21 rngolz 
 |-  ( ( R e. RingOps /\ z e. ran G ) -> ( Z ( 2nd ` R ) z ) = Z )
27 ovex 
 |-  ( Z ( 2nd ` R ) z ) e. _V
28 27 elsn 
 |-  ( ( Z ( 2nd ` R ) z ) e. { Z } <-> ( Z ( 2nd ` R ) z ) = Z )
29 26 28 sylibr 
 |-  ( ( R e. RingOps /\ z e. ran G ) -> ( Z ( 2nd ` R ) z ) e. { Z } )
30 25 29 jca 
 |-  ( ( R e. RingOps /\ z e. ran G ) -> ( ( z ( 2nd ` R ) Z ) e. { Z } /\ ( Z ( 2nd ` R ) z ) e. { Z } ) )
31 30 ralrimiva 
 |-  ( R e. RingOps -> A. z e. ran G ( ( z ( 2nd ` R ) Z ) e. { Z } /\ ( Z ( 2nd ` R ) z ) e. { Z } ) )
32 20 31 jca 
 |-  ( R e. RingOps -> ( A. y e. { Z } ( Z G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) Z ) e. { Z } /\ ( Z ( 2nd ` R ) z ) e. { Z } ) ) )
33 oveq1 
 |-  ( x = Z -> ( x G y ) = ( Z G y ) )
34 33 eleq1d 
 |-  ( x = Z -> ( ( x G y ) e. { Z } <-> ( Z G y ) e. { Z } ) )
35 34 ralbidv 
 |-  ( x = Z -> ( A. y e. { Z } ( x G y ) e. { Z } <-> A. y e. { Z } ( Z G y ) e. { Z } ) )
36 oveq2 
 |-  ( x = Z -> ( z ( 2nd ` R ) x ) = ( z ( 2nd ` R ) Z ) )
37 36 eleq1d 
 |-  ( x = Z -> ( ( z ( 2nd ` R ) x ) e. { Z } <-> ( z ( 2nd ` R ) Z ) e. { Z } ) )
38 oveq1 
 |-  ( x = Z -> ( x ( 2nd ` R ) z ) = ( Z ( 2nd ` R ) z ) )
39 38 eleq1d 
 |-  ( x = Z -> ( ( x ( 2nd ` R ) z ) e. { Z } <-> ( Z ( 2nd ` R ) z ) e. { Z } ) )
40 37 39 anbi12d 
 |-  ( x = Z -> ( ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) <-> ( ( z ( 2nd ` R ) Z ) e. { Z } /\ ( Z ( 2nd ` R ) z ) e. { Z } ) ) )
41 40 ralbidv 
 |-  ( x = Z -> ( A. z e. ran G ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) <-> A. z e. ran G ( ( z ( 2nd ` R ) Z ) e. { Z } /\ ( Z ( 2nd ` R ) z ) e. { Z } ) ) )
42 35 41 anbi12d 
 |-  ( x = Z -> ( ( A. y e. { Z } ( x G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) ) <-> ( A. y e. { Z } ( Z G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) Z ) e. { Z } /\ ( Z ( 2nd ` R ) z ) e. { Z } ) ) ) )
43 32 42 syl5ibrcom 
 |-  ( R e. RingOps -> ( x = Z -> ( A. y e. { Z } ( x G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) ) ) )
44 9 43 biimtrid 
 |-  ( R e. RingOps -> ( x e. { Z } -> ( A. y e. { Z } ( x G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) ) ) )
45 44 ralrimiv 
 |-  ( R e. RingOps -> A. x e. { Z } ( A. y e. { Z } ( x G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) ) )
46 1 21 3 2 isidl 
 |-  ( R e. RingOps -> ( { Z } e. ( Idl ` R ) <-> ( { Z } C_ ran G /\ Z e. { Z } /\ A. x e. { Z } ( A. y e. { Z } ( x G y ) e. { Z } /\ A. z e. ran G ( ( z ( 2nd ` R ) x ) e. { Z } /\ ( x ( 2nd ` R ) z ) e. { Z } ) ) ) ) )
47 5 8 45 46 mpbir3and 
 |-  ( R e. RingOps -> { Z } e. ( Idl ` R ) )