# Metamath Proof Explorer

## Theorem isdrngo3

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses isdivrng1.1 ${⊢}{G}={1}^{st}\left({R}\right)$
isdivrng1.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
isdivrng1.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
isdivrng1.4 ${⊢}{X}=\mathrm{ran}{G}$
isdivrng2.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
Assertion isdrngo3 ${⊢}{R}\in \mathrm{DivRingOps}↔\left({R}\in \mathrm{RingOps}\wedge \left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)\right)$

### Proof

Step Hyp Ref Expression
1 isdivrng1.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 isdivrng1.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 isdivrng1.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
4 isdivrng1.4 ${⊢}{X}=\mathrm{ran}{G}$
5 isdivrng2.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
6 1 2 3 4 5 isdrngo2 ${⊢}{R}\in \mathrm{DivRingOps}↔\left({R}\in \mathrm{RingOps}\wedge \left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)\right)$
7 eldifi ${⊢}{x}\in \left({X}\setminus \left\{{Z}\right\}\right)\to {x}\in {X}$
8 difss ${⊢}{X}\setminus \left\{{Z}\right\}\subseteq {X}$
9 ssrexv ${⊢}{X}\setminus \left\{{Z}\right\}\subseteq {X}\to \left(\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)$
10 8 9 ax-mp ${⊢}\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}$
11 neeq1 ${⊢}{y}{H}{x}={U}\to \left({y}{H}{x}\ne {Z}↔{U}\ne {Z}\right)$
12 11 biimparc ${⊢}\left({U}\ne {Z}\wedge {y}{H}{x}={U}\right)\to {y}{H}{x}\ne {Z}$
13 3 4 1 2 rngolz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\to {Z}{H}{x}={Z}$
14 oveq1 ${⊢}{y}={Z}\to {y}{H}{x}={Z}{H}{x}$
15 14 eqeq1d ${⊢}{y}={Z}\to \left({y}{H}{x}={Z}↔{Z}{H}{x}={Z}\right)$
16 13 15 syl5ibrcom ${⊢}\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\to \left({y}={Z}\to {y}{H}{x}={Z}\right)$
17 16 necon3d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\to \left({y}{H}{x}\ne {Z}\to {y}\ne {Z}\right)$
18 17 imp ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\wedge {y}{H}{x}\ne {Z}\right)\to {y}\ne {Z}$
19 12 18 sylan2 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {x}\in {X}\right)\wedge \left({U}\ne {Z}\wedge {y}{H}{x}={U}\right)\right)\to {y}\ne {Z}$
20 19 an4s ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge \left({x}\in {X}\wedge {y}{H}{x}={U}\right)\right)\to {y}\ne {Z}$
21 20 anassrs ${⊢}\left(\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\wedge {y}{H}{x}={U}\right)\to {y}\ne {Z}$
22 pm3.2 ${⊢}{y}\in {X}\to \left({y}\ne {Z}\to \left({y}\in {X}\wedge {y}\ne {Z}\right)\right)$
23 21 22 syl5com ${⊢}\left(\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\wedge {y}{H}{x}={U}\right)\to \left({y}\in {X}\to \left({y}\in {X}\wedge {y}\ne {Z}\right)\right)$
24 eldifsn ${⊢}{y}\in \left({X}\setminus \left\{{Z}\right\}\right)↔\left({y}\in {X}\wedge {y}\ne {Z}\right)$
25 23 24 syl6ibr ${⊢}\left(\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\wedge {y}{H}{x}={U}\right)\to \left({y}\in {X}\to {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)$
26 25 imdistanda ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\to \left(\left({y}{H}{x}={U}\wedge {y}\in {X}\right)\to \left({y}{H}{x}={U}\wedge {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\right)$
27 ancom ${⊢}\left({y}\in {X}\wedge {y}{H}{x}={U}\right)↔\left({y}{H}{x}={U}\wedge {y}\in {X}\right)$
28 ancom ${⊢}\left({y}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {y}{H}{x}={U}\right)↔\left({y}{H}{x}={U}\wedge {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)$
29 26 27 28 3imtr4g ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\to \left(\left({y}\in {X}\wedge {y}{H}{x}={U}\right)\to \left({y}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {y}{H}{x}={U}\right)\right)$
30 29 reximdv2 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\to \exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)$
31 10 30 impbid2 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in {X}\right)\to \left(\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)$
32 7 31 sylan2 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\wedge {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\to \left(\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)$
33 32 ralbidva ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}↔\forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)$
34 33 pm5.32da ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)↔\left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)\right)$
35 34 pm5.32i ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)\right)↔\left({R}\in \mathrm{RingOps}\wedge \left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)\right)$
36 6 35 bitri ${⊢}{R}\in \mathrm{DivRingOps}↔\left({R}\in \mathrm{RingOps}\wedge \left({U}\ne {Z}\wedge \forall {x}\in \left({X}\setminus \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{H}{x}={U}\right)\right)$