# Metamath Proof Explorer

## Theorem rngoueqz

Description: Obsolete as of 23-Jan-2020. Use 0ring01eqbi instead. In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses uznzr.1 ${⊢}{G}={1}^{st}\left({R}\right)$
uznzr.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
uznzr.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
uznzr.4 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
uznzr.5 ${⊢}{X}=\mathrm{ran}{G}$
Assertion rngoueqz ${⊢}{R}\in \mathrm{RingOps}\to \left({X}\approx {1}_{𝑜}↔{U}={Z}\right)$

### Proof

Step Hyp Ref Expression
1 uznzr.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 uznzr.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 uznzr.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
4 uznzr.4 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
5 uznzr.5 ${⊢}{X}=\mathrm{ran}{G}$
6 1 5 3 rngo0cl ${⊢}{R}\in \mathrm{RingOps}\to {Z}\in {X}$
7 en1eqsn ${⊢}\left({Z}\in {X}\wedge {X}\approx {1}_{𝑜}\right)\to {X}=\left\{{Z}\right\}$
8 1 rneqi ${⊢}\mathrm{ran}{G}=\mathrm{ran}{1}^{st}\left({R}\right)$
9 8 2 4 rngo1cl ${⊢}{R}\in \mathrm{RingOps}\to {U}\in \mathrm{ran}{G}$
10 eleq2 ${⊢}{X}=\left\{{Z}\right\}\to \left({U}\in {X}↔{U}\in \left\{{Z}\right\}\right)$
11 10 biimpd ${⊢}{X}=\left\{{Z}\right\}\to \left({U}\in {X}\to {U}\in \left\{{Z}\right\}\right)$
12 elsni ${⊢}{U}\in \left\{{Z}\right\}\to {U}={Z}$
13 11 12 syl6com ${⊢}{U}\in {X}\to \left({X}=\left\{{Z}\right\}\to {U}={Z}\right)$
14 5 eqcomi ${⊢}\mathrm{ran}{G}={X}$
15 13 14 eleq2s ${⊢}{U}\in \mathrm{ran}{G}\to \left({X}=\left\{{Z}\right\}\to {U}={Z}\right)$
16 9 15 syl ${⊢}{R}\in \mathrm{RingOps}\to \left({X}=\left\{{Z}\right\}\to {U}={Z}\right)$
17 7 16 syl5com ${⊢}\left({Z}\in {X}\wedge {X}\approx {1}_{𝑜}\right)\to \left({R}\in \mathrm{RingOps}\to {U}={Z}\right)$
18 17 ex ${⊢}{Z}\in {X}\to \left({X}\approx {1}_{𝑜}\to \left({R}\in \mathrm{RingOps}\to {U}={Z}\right)\right)$
19 18 com23 ${⊢}{Z}\in {X}\to \left({R}\in \mathrm{RingOps}\to \left({X}\approx {1}_{𝑜}\to {U}={Z}\right)\right)$
20 6 19 mpcom ${⊢}{R}\in \mathrm{RingOps}\to \left({X}\approx {1}_{𝑜}\to {U}={Z}\right)$
21 1 5 rngone0 ${⊢}{R}\in \mathrm{RingOps}\to {X}\ne \varnothing$
22 oveq2 ${⊢}{U}={Z}\to {x}{H}{U}={x}{H}{Z}$
23 22 ralrimivw ${⊢}{U}={Z}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}$
24 3 5 1 2 rngorz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\to {x}{H}{Z}={Z}$
25 24 ralrimiva ${⊢}{R}\in \mathrm{RingOps}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}$
26 5 8 eqtri ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
27 2 26 4 rngoridm ${⊢}\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\to {x}{H}{U}={x}$
28 27 ralrimiva ${⊢}{R}\in \mathrm{RingOps}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}$
29 r19.26 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)↔\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}\right)$
30 r19.26 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\wedge {x}{H}{Z}={Z}\right)↔\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\right)$
31 eqtr ${⊢}\left({x}={x}{H}{U}\wedge {x}{H}{U}={x}{H}{Z}\right)\to {x}={x}{H}{Z}$
32 eqtr ${⊢}\left({x}={x}{H}{Z}\wedge {x}{H}{Z}={Z}\right)\to {x}={Z}$
33 32 ex ${⊢}{x}={x}{H}{Z}\to \left({x}{H}{Z}={Z}\to {x}={Z}\right)$
34 31 33 syl ${⊢}\left({x}={x}{H}{U}\wedge {x}{H}{U}={x}{H}{Z}\right)\to \left({x}{H}{Z}={Z}\to {x}={Z}\right)$
35 34 ex ${⊢}{x}={x}{H}{U}\to \left({x}{H}{U}={x}{H}{Z}\to \left({x}{H}{Z}={Z}\to {x}={Z}\right)\right)$
36 35 eqcoms ${⊢}{x}{H}{U}={x}\to \left({x}{H}{U}={x}{H}{Z}\to \left({x}{H}{Z}={Z}\to {x}={Z}\right)\right)$
37 36 imp31 ${⊢}\left(\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\wedge {x}{H}{Z}={Z}\right)\to {x}={Z}$
38 37 ralimi ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\wedge {x}{H}{Z}={Z}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}$
39 eqsn ${⊢}{X}\ne \varnothing \to \left({X}=\left\{{Z}\right\}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\right)$
40 ensn1g ${⊢}{Z}\in {X}\to \left\{{Z}\right\}\approx {1}_{𝑜}$
41 6 40 syl ${⊢}{R}\in \mathrm{RingOps}\to \left\{{Z}\right\}\approx {1}_{𝑜}$
42 breq1 ${⊢}{X}=\left\{{Z}\right\}\to \left({X}\approx {1}_{𝑜}↔\left\{{Z}\right\}\approx {1}_{𝑜}\right)$
43 41 42 syl5ibr ${⊢}{X}=\left\{{Z}\right\}\to \left({R}\in \mathrm{RingOps}\to {X}\approx {1}_{𝑜}\right)$
44 39 43 syl6bir ${⊢}{X}\ne \varnothing \to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\to \left({R}\in \mathrm{RingOps}\to {X}\approx {1}_{𝑜}\right)\right)$
45 44 com3l ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)$
46 38 45 syl ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\wedge {x}{H}{Z}={Z}\right)\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)$
47 30 46 sylbir ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\right)\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)$
48 47 ex ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{U}={x}\wedge {x}{H}{U}={x}{H}{Z}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)\right)$
49 29 48 sylbir ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)\right)$
50 49 ex ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)\right)\right)$
51 50 com24 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}\to \left({R}\in \mathrm{RingOps}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)\right)\right)$
52 28 51 mpcom ${⊢}{R}\in \mathrm{RingOps}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{Z}={Z}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)\right)$
53 25 52 mpd ${⊢}{R}\in \mathrm{RingOps}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{U}={x}{H}{Z}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)$
54 23 53 syl5com ${⊢}{U}={Z}\to \left({R}\in \mathrm{RingOps}\to \left({X}\ne \varnothing \to {X}\approx {1}_{𝑜}\right)\right)$
55 54 com13 ${⊢}{X}\ne \varnothing \to \left({R}\in \mathrm{RingOps}\to \left({U}={Z}\to {X}\approx {1}_{𝑜}\right)\right)$
56 21 55 mpcom ${⊢}{R}\in \mathrm{RingOps}\to \left({U}={Z}\to {X}\approx {1}_{𝑜}\right)$
57 20 56 impbid ${⊢}{R}\in \mathrm{RingOps}\to \left({X}\approx {1}_{𝑜}↔{U}={Z}\right)$