Metamath Proof Explorer

Theorem isdrngo2

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

Ref Expression
Hypotheses isdivrng1.1 ⊢G=1st⁡R
isdivrng1.2 ⊢H=2nd⁡R
isdivrng1.3 ⊢Z=GId⁡G
isdivrng1.4 ⊢X=ran⁡G
isdivrng2.5 ⊢U=GId⁡H
Assertion isdrngo2 ⊢R∈DivRingOps↔R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U

Proof

Step Hyp Ref Expression
1 isdivrng1.1 ⊢G=1st⁡R
2 isdivrng1.2 ⊢H=2nd⁡R
3 isdivrng1.3 ⊢Z=GId⁡G
4 isdivrng1.4 ⊢X=ran⁡G
5 isdivrng2.5 ⊢U=GId⁡H
6 1 2 3 4 isdrngo1 ⊢R∈DivRingOps↔R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp
7 1 2 4 3 5 dvrunz ⊢R∈DivRingOps→U≠Z
8 6 7 sylbir ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→U≠Z
9 grporndm ⊢H↾X∖Z×X∖Z∈GrpOp→ran⁡H↾X∖Z×X∖Z=dom⁡dom⁡H↾X∖Z×X∖Z
10 9 adantl ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→ran⁡H↾X∖Z×X∖Z=dom⁡dom⁡H↾X∖Z×X∖Z
11 difss ⊢X∖Z⊆X
12 xpss12 ⊢X∖Z⊆X∧X∖Z⊆X→X∖Z×X∖Z⊆X×X
13 11 11 12 mp2an ⊢X∖Z×X∖Z⊆X×X
14 1 2 4 rngosm ⊢R∈RingOps→H:X×X⟶X
15 14 fdmd ⊢R∈RingOps→dom⁡H=X×X
16 13 15 sseqtrrid ⊢R∈RingOps→X∖Z×X∖Z⊆dom⁡H
17 16 adantr ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→X∖Z×X∖Z⊆dom⁡H
18 ssdmres ⊢X∖Z×X∖Z⊆dom⁡H↔dom⁡H↾X∖Z×X∖Z=X∖Z×X∖Z
19 17 18 sylib ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→dom⁡H↾X∖Z×X∖Z=X∖Z×X∖Z
20 19 dmeqd ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→dom⁡dom⁡H↾X∖Z×X∖Z=dom⁡X∖Z×X∖Z
21 dmxpid ⊢dom⁡X∖Z×X∖Z=X∖Z
22 20 21 eqtrdi ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→dom⁡dom⁡H↾X∖Z×X∖Z=X∖Z
23 10 22 eqtrd ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→ran⁡H↾X∖Z×X∖Z=X∖Z
24 23 eleq2d ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→x∈ran⁡H↾X∖Z×X∖Z↔x∈X∖Z
25 24 biimpar ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→x∈ran⁡H↾X∖Z×X∖Z
26 eqid ⊢ran⁡H↾X∖Z×X∖Z=ran⁡H↾X∖Z×X∖Z
27 eqid ⊢inv⁡H↾X∖Z×X∖Z=inv⁡H↾X∖Z×X∖Z
28 26 27 grpoinvcl ⊢H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→inv⁡H↾X∖Z×X∖Z⁡x∈ran⁡H↾X∖Z×X∖Z
29 28 adantll ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→inv⁡H↾X∖Z×X∖Z⁡x∈ran⁡H↾X∖Z×X∖Z
30 eqid ⊢GId⁡H↾X∖Z×X∖Z=GId⁡H↾X∖Z×X∖Z
31 26 30 27 grpolinv ⊢H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→inv⁡H↾X∖Z×X∖Z⁡xH↾X∖Z×X∖Zx=GId⁡H↾X∖Z×X∖Z
32 31 adantll ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→inv⁡H↾X∖Z×X∖Z⁡xH↾X∖Z×X∖Zx=GId⁡H↾X∖Z×X∖Z
33 2 rngomndo ⊢R∈RingOps→H∈MndOp
34 mndomgmid ⊢H∈MndOp→H∈Magma∩ExId
35 33 34 syl ⊢R∈RingOps→H∈Magma∩ExId
36 35 adantr ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→H∈Magma∩ExId
37 11 4 sseqtri ⊢X∖Z⊆ran⁡G
38 2 1 rngorn1eq ⊢R∈RingOps→ran⁡G=ran⁡H
39 37 38 sseqtrid ⊢R∈RingOps→X∖Z⊆ran⁡H
40 39 adantr ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→X∖Z⊆ran⁡H
41 1 rneqi ⊢ran⁡G=ran⁡1st⁡R
42 4 41 eqtri ⊢X=ran⁡1st⁡R
43 42 2 5 rngo1cl ⊢R∈RingOps→U∈X
44 43 adantr ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→U∈X
45 eldifsn ⊢U∈X∖Z↔U∈X∧U≠Z
46 44 8 45 sylanbrc ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→U∈X∖Z
47 grpomndo ⊢H↾X∖Z×X∖Z∈GrpOp→H↾X∖Z×X∖Z∈MndOp
48 mndoismgmOLD ⊢H↾X∖Z×X∖Z∈MndOp→H↾X∖Z×X∖Z∈Magma
49 47 48 syl ⊢H↾X∖Z×X∖Z∈GrpOp→H↾X∖Z×X∖Z∈Magma
50 49 adantl ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→H↾X∖Z×X∖Z∈Magma
51 eqid ⊢ran⁡H=ran⁡H
52 eqid ⊢H↾X∖Z×X∖Z=H↾X∖Z×X∖Z
53 51 5 52 exidresid ⊢H∈Magma∩ExId∧X∖Z⊆ran⁡H∧U∈X∖Z∧H↾X∖Z×X∖Z∈Magma→GId⁡H↾X∖Z×X∖Z=U
54 36 40 46 50 53 syl31anc ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→GId⁡H↾X∖Z×X∖Z=U
55 54 adantr ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→GId⁡H↾X∖Z×X∖Z=U
56 32 55 eqtrd ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→inv⁡H↾X∖Z×X∖Z⁡xH↾X∖Z×X∖Zx=U
57 oveq1 ⊢y=inv⁡H↾X∖Z×X∖Z⁡x→yH↾X∖Z×X∖Zx=inv⁡H↾X∖Z×X∖Z⁡xH↾X∖Z×X∖Zx
58 57 eqeq1d ⊢y=inv⁡H↾X∖Z×X∖Z⁡x→yH↾X∖Z×X∖Zx=U↔inv⁡H↾X∖Z×X∖Z⁡xH↾X∖Z×X∖Zx=U
59 58 rspcev ⊢inv⁡H↾X∖Z×X∖Z⁡x∈ran⁡H↾X∖Z×X∖Z∧inv⁡H↾X∖Z×X∖Z⁡xH↾X∖Z×X∖Zx=U→∃y∈ran⁡H↾X∖Z×X∖ZyH↾X∖Z×X∖Zx=U
60 29 56 59 syl2anc ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈ran⁡H↾X∖Z×X∖Z→∃y∈ran⁡H↾X∖Z×X∖ZyH↾X∖Z×X∖Zx=U
61 25 60 syldan ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→∃y∈ran⁡H↾X∖Z×X∖ZyH↾X∖Z×X∖Zx=U
62 23 adantr ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→ran⁡H↾X∖Z×X∖Z=X∖Z
63 62 rexeqdv ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→∃y∈ran⁡H↾X∖Z×X∖ZyH↾X∖Z×X∖Zx=U↔∃y∈X∖ZyH↾X∖Z×X∖Zx=U
64 ovres ⊢y∈X∖Z∧x∈X∖Z→yH↾X∖Z×X∖Zx=yHx
65 64 ancoms ⊢x∈X∖Z∧y∈X∖Z→yH↾X∖Z×X∖Zx=yHx
66 65 eqeq1d ⊢x∈X∖Z∧y∈X∖Z→yH↾X∖Z×X∖Zx=U↔yHx=U
67 66 rexbidva ⊢x∈X∖Z→∃y∈X∖ZyH↾X∖Z×X∖Zx=U↔∃y∈X∖ZyHx=U
68 67 adantl ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→∃y∈X∖ZyH↾X∖Z×X∖Zx=U↔∃y∈X∖ZyHx=U
69 63 68 bitrd ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→∃y∈ran⁡H↾X∖Z×X∖ZyH↾X∖Z×X∖Zx=U↔∃y∈X∖ZyHx=U
70 61 69 mpbid ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp∧x∈X∖Z→∃y∈X∖ZyHx=U
71 70 ralrimiva ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→∀x∈X∖Z∃y∈X∖ZyHx=U
72 8 71 jca ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp→U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U
73 1 fvexi ⊢G∈V
74 73 rnex ⊢ran⁡G∈V
75 4 74 eqeltri ⊢X∈V
76 difexg ⊢X∈V→X∖Z∈V
77 75 76 mp1i ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→X∖Z∈V
78 14 ffnd ⊢R∈RingOps→HFnX×X
79 78 adantr ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→HFnX×X
80 fnssres ⊢HFnX×X∧X∖Z×X∖Z⊆X×X→H↾X∖Z×X∖ZFnX∖Z×X∖Z
81 79 13 80 sylancl ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→H↾X∖Z×X∖ZFnX∖Z×X∖Z
82 ovres ⊢u∈X∖Z∧v∈X∖Z→uH↾X∖Z×X∖Zv=uHv
83 82 adantl ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z→uH↾X∖Z×X∖Zv=uHv
84 eldifi ⊢u∈X∖Z→u∈X
85 eldifi ⊢v∈X∖Z→v∈X
86 84 85 anim12i ⊢u∈X∖Z∧v∈X∖Z→u∈X∧v∈X
87 1 2 4 rngocl ⊢R∈RingOps∧u∈X∧v∈X→uHv∈X
88 87 3expb ⊢R∈RingOps∧u∈X∧v∈X→uHv∈X
89 86 88 sylan2 ⊢R∈RingOps∧u∈X∖Z∧v∈X∖Z→uHv∈X
90 89 adantlr ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z→uHv∈X
91 oveq2 ⊢x=u→yHx=yHu
92 91 eqeq1d ⊢x=u→yHx=U↔yHu=U
93 92 rexbidv ⊢x=u→∃y∈X∖ZyHx=U↔∃y∈X∖ZyHu=U
94 93 rspcv ⊢u∈X∖Z→∀x∈X∖Z∃y∈X∖ZyHx=U→∃y∈X∖ZyHu=U
95 94 imdistanri ⊢∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z→∃y∈X∖ZyHu=U∧u∈X∖Z
96 eldifsn ⊢v∈X∖Z↔v∈X∧v≠Z
97 ssrexv ⊢X∖Z⊆X→∃y∈X∖ZyHu=U→∃y∈XyHu=U
98 11 97 ax-mp ⊢∃y∈X∖ZyHu=U→∃y∈XyHu=U
99 1 2 3 4 5 zerdivemp1x ⊢R∈RingOps∧u∈X∧∃y∈XyHu=U→v∈X→uHv=Z→v=Z
100 98 99 syl3an3 ⊢R∈RingOps∧u∈X∧∃y∈X∖ZyHu=U→v∈X→uHv=Z→v=Z
101 84 100 syl3an2 ⊢R∈RingOps∧u∈X∖Z∧∃y∈X∖ZyHu=U→v∈X→uHv=Z→v=Z
102 101 3expb ⊢R∈RingOps∧u∈X∖Z∧∃y∈X∖ZyHu=U→v∈X→uHv=Z→v=Z
103 102 imp ⊢R∈RingOps∧u∈X∖Z∧∃y∈X∖ZyHu=U∧v∈X→uHv=Z→v=Z
104 103 necon3d ⊢R∈RingOps∧u∈X∖Z∧∃y∈X∖ZyHu=U∧v∈X→v≠Z→uHv≠Z
105 104 impr ⊢R∈RingOps∧u∈X∖Z∧∃y∈X∖ZyHu=U∧v∈X∧v≠Z→uHv≠Z
106 96 105 sylan2b ⊢R∈RingOps∧u∈X∖Z∧∃y∈X∖ZyHu=U∧v∈X∖Z→uHv≠Z
107 106 an32s ⊢R∈RingOps∧v∈X∖Z∧u∈X∖Z∧∃y∈X∖ZyHu=U→uHv≠Z
108 107 ancom2s ⊢R∈RingOps∧v∈X∖Z∧∃y∈X∖ZyHu=U∧u∈X∖Z→uHv≠Z
109 95 108 sylan2 ⊢R∈RingOps∧v∈X∖Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z→uHv≠Z
110 109 an42s ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z→uHv≠Z
111 110 adantlrl ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z→uHv≠Z
112 eldifsn ⊢uHv∈X∖Z↔uHv∈X∧uHv≠Z
113 90 111 112 sylanbrc ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z→uHv∈X∖Z
114 83 113 eqeltrd ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z→uH↾X∖Z×X∖Zv∈X∖Z
115 114 ralrimivva ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→∀u∈X∖Z∀v∈X∖ZuH↾X∖Z×X∖Zv∈X∖Z
116 ffnov ⊢H↾X∖Z×X∖Z:X∖Z×X∖Z⟶X∖Z↔H↾X∖Z×X∖ZFnX∖Z×X∖Z∧∀u∈X∖Z∀v∈X∖ZuH↾X∖Z×X∖Zv∈X∖Z
117 81 115 116 sylanbrc ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→H↾X∖Z×X∖Z:X∖Z×X∖Z⟶X∖Z
118 113 3adantr3 ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uHv∈X∖Z
119 simpr3 ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→w∈X∖Z
120 118 119 ovresd ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uHvH↾X∖Z×X∖Zw=uHvHw
121 82 3adant3 ⊢u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uH↾X∖Z×X∖Zv=uHv
122 121 adantl ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uH↾X∖Z×X∖Zv=uHv
123 122 oveq1d ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uH↾X∖Z×X∖ZvH↾X∖Z×X∖Zw=uHvH↾X∖Z×X∖Zw
124 ovres ⊢v∈X∖Z∧w∈X∖Z→vH↾X∖Z×X∖Zw=vHw
125 124 3adant1 ⊢u∈X∖Z∧v∈X∖Z∧w∈X∖Z→vH↾X∖Z×X∖Zw=vHw
126 125 adantl ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→vH↾X∖Z×X∖Zw=vHw
127 126 oveq2d ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uHvH↾X∖Z×X∖Zw=uHvHw
128 simpr1 ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→u∈X∖Z
129 fovcdm ⊢H↾X∖Z×X∖Z:X∖Z×X∖Z⟶X∖Z∧v∈X∖Z∧w∈X∖Z→vH↾X∖Z×X∖Zw∈X∖Z
130 129 3adant3r1 ⊢H↾X∖Z×X∖Z:X∖Z×X∖Z⟶X∖Z∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→vH↾X∖Z×X∖Zw∈X∖Z
131 117 130 sylan ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→vH↾X∖Z×X∖Zw∈X∖Z
132 128 131 ovresd ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uH↾X∖Z×X∖ZvH↾X∖Z×X∖Zw=uHvH↾X∖Z×X∖Zw
133 eldifi ⊢w∈X∖Z→w∈X
134 84 85 133 3anim123i ⊢u∈X∖Z∧v∈X∖Z∧w∈X∖Z→u∈X∧v∈X∧w∈X
135 1 2 4 rngoass ⊢R∈RingOps∧u∈X∧v∈X∧w∈X→uHvHw=uHvHw
136 134 135 sylan2 ⊢R∈RingOps∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uHvHw=uHvHw
137 136 adantlr ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uHvHw=uHvHw
138 127 132 137 3eqtr4d ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uH↾X∖Z×X∖ZvH↾X∖Z×X∖Zw=uHvHw
139 120 123 138 3eqtr4d ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z∧v∈X∖Z∧w∈X∖Z→uH↾X∖Z×X∖ZvH↾X∖Z×X∖Zw=uH↾X∖Z×X∖ZvH↾X∖Z×X∖Zw
140 43 anim1i ⊢R∈RingOps∧U≠Z→U∈X∧U≠Z
141 140 45 sylibr ⊢R∈RingOps∧U≠Z→U∈X∖Z
142 141 adantrr ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→U∈X∖Z
143 ovres ⊢U∈X∖Z∧u∈X∖Z→UH↾X∖Z×X∖Zu=UHu
144 141 143 sylan ⊢R∈RingOps∧U≠Z∧u∈X∖Z→UH↾X∖Z×X∖Zu=UHu
145 2 42 5 rngolidm ⊢R∈RingOps∧u∈X→UHu=u
146 84 145 sylan2 ⊢R∈RingOps∧u∈X∖Z→UHu=u
147 146 adantlr ⊢R∈RingOps∧U≠Z∧u∈X∖Z→UHu=u
148 144 147 eqtrd ⊢R∈RingOps∧U≠Z∧u∈X∖Z→UH↾X∖Z×X∖Zu=u
149 148 adantlrr ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z→UH↾X∖Z×X∖Zu=u
150 93 rspcva ⊢u∈X∖Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→∃y∈X∖ZyHu=U
151 oveq1 ⊢y=z→yHu=zHu
152 151 eqeq1d ⊢y=z→yHu=U↔zHu=U
153 152 cbvrexvw ⊢∃y∈X∖ZyHu=U↔∃z∈X∖ZzHu=U
154 ovres ⊢z∈X∖Z∧u∈X∖Z→zH↾X∖Z×X∖Zu=zHu
155 154 eqeq1d ⊢z∈X∖Z∧u∈X∖Z→zH↾X∖Z×X∖Zu=U↔zHu=U
156 155 ancoms ⊢u∈X∖Z∧z∈X∖Z→zH↾X∖Z×X∖Zu=U↔zHu=U
157 156 rexbidva ⊢u∈X∖Z→∃z∈X∖ZzH↾X∖Z×X∖Zu=U↔∃z∈X∖ZzHu=U
158 157 biimpar ⊢u∈X∖Z∧∃z∈X∖ZzHu=U→∃z∈X∖ZzH↾X∖Z×X∖Zu=U
159 153 158 sylan2b ⊢u∈X∖Z∧∃y∈X∖ZyHu=U→∃z∈X∖ZzH↾X∖Z×X∖Zu=U
160 150 159 syldan ⊢u∈X∖Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→∃z∈X∖ZzH↾X∖Z×X∖Zu=U
161 160 ancoms ⊢∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z→∃z∈X∖ZzH↾X∖Z×X∖Zu=U
162 161 adantll ⊢R∈RingOps∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z→∃z∈X∖ZzH↾X∖Z×X∖Zu=U
163 162 adantlrl ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U∧u∈X∖Z→∃z∈X∖ZzH↾X∖Z×X∖Zu=U
164 77 117 139 142 149 163 isgrpda ⊢R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U→H↾X∖Z×X∖Z∈GrpOp
165 72 164 impbida ⊢R∈RingOps→H↾X∖Z×X∖Z∈GrpOp↔U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U
166 165 pm5.32i ⊢R∈RingOps∧H↾X∖Z×X∖Z∈GrpOp↔R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U
167 6 166 bitri ⊢R∈DivRingOps↔R∈RingOps∧U≠Z∧∀x∈X∖Z∃y∈X∖ZyHx=U