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=1stR
0idl.2 Z=GIdG
Assertion 0idl RRingOpsZIdlR

Proof

Step Hyp Ref Expression
1 0idl.1 G=1stR
2 0idl.2 Z=GIdG
3 eqid ranG=ranG
4 1 3 2 rngo0cl RRingOpsZranG
5 4 snssd RRingOpsZranG
6 2 fvexi ZV
7 6 snid ZZ
8 7 a1i RRingOpsZZ
9 velsn xZx=Z
10 velsn yZy=Z
11 1 3 2 rngo0rid RRingOpsZranGZGZ=Z
12 4 11 mpdan RRingOpsZGZ=Z
13 ovex ZGZV
14 13 elsn ZGZZZGZ=Z
15 12 14 sylibr RRingOpsZGZZ
16 oveq2 y=ZZGy=ZGZ
17 16 eleq1d y=ZZGyZZGZZ
18 15 17 syl5ibrcom RRingOpsy=ZZGyZ
19 10 18 syl5bi RRingOpsyZZGyZ
20 19 ralrimiv RRingOpsyZZGyZ
21 eqid 2ndR=2ndR
22 2 3 1 21 rngorz RRingOpszranGz2ndRZ=Z
23 ovex z2ndRZV
24 23 elsn z2ndRZZz2ndRZ=Z
25 22 24 sylibr RRingOpszranGz2ndRZZ
26 2 3 1 21 rngolz RRingOpszranGZ2ndRz=Z
27 ovex Z2ndRzV
28 27 elsn Z2ndRzZZ2ndRz=Z
29 26 28 sylibr RRingOpszranGZ2ndRzZ
30 25 29 jca RRingOpszranGz2ndRZZZ2ndRzZ
31 30 ralrimiva RRingOpszranGz2ndRZZZ2ndRzZ
32 20 31 jca RRingOpsyZZGyZzranGz2ndRZZZ2ndRzZ
33 oveq1 x=ZxGy=ZGy
34 33 eleq1d x=ZxGyZZGyZ
35 34 ralbidv x=ZyZxGyZyZZGyZ
36 oveq2 x=Zz2ndRx=z2ndRZ
37 36 eleq1d x=Zz2ndRxZz2ndRZZ
38 oveq1 x=Zx2ndRz=Z2ndRz
39 38 eleq1d x=Zx2ndRzZZ2ndRzZ
40 37 39 anbi12d x=Zz2ndRxZx2ndRzZz2ndRZZZ2ndRzZ
41 40 ralbidv x=ZzranGz2ndRxZx2ndRzZzranGz2ndRZZZ2ndRzZ
42 35 41 anbi12d x=ZyZxGyZzranGz2ndRxZx2ndRzZyZZGyZzranGz2ndRZZZ2ndRzZ
43 32 42 syl5ibrcom RRingOpsx=ZyZxGyZzranGz2ndRxZx2ndRzZ
44 9 43 syl5bi RRingOpsxZyZxGyZzranGz2ndRxZx2ndRzZ
45 44 ralrimiv RRingOpsxZyZxGyZzranGz2ndRxZx2ndRzZ
46 1 21 3 2 isidl RRingOpsZIdlRZranGZZxZyZxGyZzranGz2ndRxZx2ndRzZ
47 5 8 45 46 mpbir3and RRingOpsZIdlR