# 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}={1}^{st}\left({R}\right)$
0idl.2 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
Assertion 0idl ${⊢}{R}\in \mathrm{RingOps}\to \left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 0idl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 0idl.2 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
3 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
4 1 3 2 rngo0cl ${⊢}{R}\in \mathrm{RingOps}\to {Z}\in \mathrm{ran}{G}$
5 4 snssd ${⊢}{R}\in \mathrm{RingOps}\to \left\{{Z}\right\}\subseteq \mathrm{ran}{G}$
6 2 fvexi ${⊢}{Z}\in \mathrm{V}$
7 6 snid ${⊢}{Z}\in \left\{{Z}\right\}$
8 7 a1i ${⊢}{R}\in \mathrm{RingOps}\to {Z}\in \left\{{Z}\right\}$
9 velsn ${⊢}{x}\in \left\{{Z}\right\}↔{x}={Z}$
10 velsn ${⊢}{y}\in \left\{{Z}\right\}↔{y}={Z}$
11 1 3 2 rngo0rid ${⊢}\left({R}\in \mathrm{RingOps}\wedge {Z}\in \mathrm{ran}{G}\right)\to {Z}{G}{Z}={Z}$
12 4 11 mpdan ${⊢}{R}\in \mathrm{RingOps}\to {Z}{G}{Z}={Z}$
13 ovex ${⊢}{Z}{G}{Z}\in \mathrm{V}$
14 13 elsn ${⊢}{Z}{G}{Z}\in \left\{{Z}\right\}↔{Z}{G}{Z}={Z}$
15 12 14 sylibr ${⊢}{R}\in \mathrm{RingOps}\to {Z}{G}{Z}\in \left\{{Z}\right\}$
16 oveq2 ${⊢}{y}={Z}\to {Z}{G}{y}={Z}{G}{Z}$
17 16 eleq1d ${⊢}{y}={Z}\to \left({Z}{G}{y}\in \left\{{Z}\right\}↔{Z}{G}{Z}\in \left\{{Z}\right\}\right)$
18 15 17 syl5ibrcom ${⊢}{R}\in \mathrm{RingOps}\to \left({y}={Z}\to {Z}{G}{y}\in \left\{{Z}\right\}\right)$
19 10 18 syl5bi ${⊢}{R}\in \mathrm{RingOps}\to \left({y}\in \left\{{Z}\right\}\to {Z}{G}{y}\in \left\{{Z}\right\}\right)$
20 19 ralrimiv ${⊢}{R}\in \mathrm{RingOps}\to \forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{Z}{G}{y}\in \left\{{Z}\right\}$
21 eqid ${⊢}{2}^{nd}\left({R}\right)={2}^{nd}\left({R}\right)$
22 2 3 1 21 rngorz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {z}\in \mathrm{ran}{G}\right)\to {z}{2}^{nd}\left({R}\right){Z}={Z}$
23 ovex ${⊢}{z}{2}^{nd}\left({R}\right){Z}\in \mathrm{V}$
24 23 elsn ${⊢}{z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}↔{z}{2}^{nd}\left({R}\right){Z}={Z}$
25 22 24 sylibr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {z}\in \mathrm{ran}{G}\right)\to {z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}$
26 2 3 1 21 rngolz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {z}\in \mathrm{ran}{G}\right)\to {Z}{2}^{nd}\left({R}\right){z}={Z}$
27 ovex ${⊢}{Z}{2}^{nd}\left({R}\right){z}\in \mathrm{V}$
28 27 elsn ${⊢}{Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}↔{Z}{2}^{nd}\left({R}\right){z}={Z}$
29 26 28 sylibr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {z}\in \mathrm{ran}{G}\right)\to {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}$
30 25 29 jca ${⊢}\left({R}\in \mathrm{RingOps}\wedge {z}\in \mathrm{ran}{G}\right)\to \left({z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\wedge {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)$
31 30 ralrimiva ${⊢}{R}\in \mathrm{RingOps}\to \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\wedge {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)$
32 20 31 jca ${⊢}{R}\in \mathrm{RingOps}\to \left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{Z}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\wedge {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)$
33 oveq1 ${⊢}{x}={Z}\to {x}{G}{y}={Z}{G}{y}$
34 33 eleq1d ${⊢}{x}={Z}\to \left({x}{G}{y}\in \left\{{Z}\right\}↔{Z}{G}{y}\in \left\{{Z}\right\}\right)$
35 34 ralbidv ${⊢}{x}={Z}\to \left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\in \left\{{Z}\right\}↔\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{Z}{G}{y}\in \left\{{Z}\right\}\right)$
36 oveq2 ${⊢}{x}={Z}\to {z}{2}^{nd}\left({R}\right){x}={z}{2}^{nd}\left({R}\right){Z}$
37 36 eleq1d ${⊢}{x}={Z}\to \left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}↔{z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\right)$
38 oveq1 ${⊢}{x}={Z}\to {x}{2}^{nd}\left({R}\right){z}={Z}{2}^{nd}\left({R}\right){z}$
39 38 eleq1d ${⊢}{x}={Z}\to \left({x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}↔{Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)$
40 37 39 anbi12d ${⊢}{x}={Z}\to \left(\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)↔\left({z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\wedge {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)$
41 40 ralbidv ${⊢}{x}={Z}\to \left(\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)↔\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\wedge {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)$
42 35 41 anbi12d ${⊢}{x}={Z}\to \left(\left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)↔\left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{Z}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){Z}\in \left\{{Z}\right\}\wedge {Z}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)\right)$
43 32 42 syl5ibrcom ${⊢}{R}\in \mathrm{RingOps}\to \left({x}={Z}\to \left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)\right)$
44 9 43 syl5bi ${⊢}{R}\in \mathrm{RingOps}\to \left({x}\in \left\{{Z}\right\}\to \left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)\right)$
45 44 ralrimiv ${⊢}{R}\in \mathrm{RingOps}\to \forall {x}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)$
46 1 21 3 2 isidl ${⊢}{R}\in \mathrm{RingOps}\to \left(\left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)↔\left(\left\{{Z}\right\}\subseteq \mathrm{ran}{G}\wedge {Z}\in \left\{{Z}\right\}\wedge \forall {x}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left\{{Z}\right\}\phantom{\rule{.4em}{0ex}}{x}{G}{y}\in \left\{{Z}\right\}\wedge \forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({z}{2}^{nd}\left({R}\right){x}\in \left\{{Z}\right\}\wedge {x}{2}^{nd}\left({R}\right){z}\in \left\{{Z}\right\}\right)\right)\right)\right)$
47 5 8 45 46 mpbir3and ${⊢}{R}\in \mathrm{RingOps}\to \left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)$