Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isdrngo2 Structured version   Visualization version   GIF version
Theorem isdrngo2 37293
Description: A division ring is a ring in which 1 β‰  0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.)
Hypotheses
Ref Expression
isdivrng1.1 𝐺 = (1st β€˜π‘…)
isdivrng1.2 𝐻 = (2nd β€˜π‘…)
isdivrng1.3 𝑍 = (GIdβ€˜πΊ)
isdivrng1.4 𝑋 = ran 𝐺
isdivrng2.5 π‘ˆ = (GIdβ€˜π»)
Assertion
Ref Expression
isdrngo2 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
Distinct variable groups:   π‘₯,𝐻,𝑦   π‘₯,𝑋,𝑦   π‘₯,𝑍,𝑦   π‘₯,𝑅,𝑦   π‘₯,π‘ˆ,𝑦
Allowed substitution hints:   𝐺(π‘₯,𝑦)
Proof of Theorem isdrngo2
Dummy variables 𝑒 𝑣 𝑀 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isdivrng1.1 . . 3 𝐺 = (1st β€˜π‘…)
2 isdivrng1.2 . . 3 𝐻 = (2nd β€˜π‘…)
3 isdivrng1.3 . . 3 𝑍 = (GIdβ€˜πΊ)
4 isdivrng1.4 . . 3 𝑋 = ran 𝐺
51, 2, 3, 4isdrngo1 37291 . 2 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp))
6 isdivrng2.5 . . . . . . 7 π‘ˆ = (GIdβ€˜π»)
71, 2, 4, 3, 6dvrunz 37289 . . . . . 6 (𝑅 ∈ DivRingOps β†’ π‘ˆ β‰  𝑍)
85, 7sylbir 234 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ β‰  𝑍)
9 grporndm 30198 . . . . . . . . . . . 12 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
109adantl 481 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
11 difss 4131 . . . . . . . . . . . . . . . . 17 (𝑋 βˆ– {𝑍}) βŠ† 𝑋
12 xpss12 5691 . . . . . . . . . . . . . . . . 17 (((𝑋 βˆ– {𝑍}) βŠ† 𝑋 ∧ (𝑋 βˆ– {𝑍}) βŠ† 𝑋) β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋))
1311, 11, 12mp2an 689 . . . . . . . . . . . . . . . 16 ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋)
141, 2, 4rngosm 37235 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps β†’ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹)
1514fdmd 6728 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps β†’ dom 𝐻 = (𝑋 Γ— 𝑋))
1613, 15sseqtrrid 4035 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻)
1716adantr 480 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻)
18 ssdmres 6004 . . . . . . . . . . . . . 14 (((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻 ↔ dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
1917, 18sylib 217 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
2019dmeqd 5905 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
21 dmxpid 5929 . . . . . . . . . . . 12 dom ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) = (𝑋 βˆ– {𝑍})
2220, 21eqtrdi 2787 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
2310, 22eqtrd 2771 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
2423eleq2d 2818 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ↔ π‘₯ ∈ (𝑋 βˆ– {𝑍})))
2524biimpar 477 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
26 eqid 2731 . . . . . . . . . . 11 ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
27 eqid 2731 . . . . . . . . . . 11 (invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = (invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
2826, 27grpoinvcl 30212 . . . . . . . . . 10 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
2928adantll 711 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
30 eqid 2731 . . . . . . . . . . . 12 (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
3126, 30, 27grpolinv 30214 . . . . . . . . . . 11 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))))
3231adantll 711 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))))
332rngomndo 37270 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ 𝐻 ∈ MndOp)
34 mndomgmid 37206 . . . . . . . . . . . . . 14 (𝐻 ∈ MndOp β†’ 𝐻 ∈ (Magma ∩ ExId ))
3533, 34syl 17 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps β†’ 𝐻 ∈ (Magma ∩ ExId ))
3635adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ 𝐻 ∈ (Magma ∩ ExId ))
3711, 4sseqtri 4018 . . . . . . . . . . . . . 14 (𝑋 βˆ– {𝑍}) βŠ† ran 𝐺
382, 1rngorn1eq 37269 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ ran 𝐺 = ran 𝐻)
3937, 38sseqtrid 4034 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps β†’ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻)
4039adantr 480 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻)
411rneqi 5936 . . . . . . . . . . . . . . . 16 ran 𝐺 = ran (1st β€˜π‘…)
424, 41eqtri 2759 . . . . . . . . . . . . . . 15 𝑋 = ran (1st β€˜π‘…)
4342, 2, 6rngo1cl 37274 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ π‘ˆ ∈ 𝑋)
4443adantr 480 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ ∈ 𝑋)
45 eldifsn 4790 . . . . . . . . . . . . 13 (π‘ˆ ∈ (𝑋 βˆ– {𝑍}) ↔ (π‘ˆ ∈ 𝑋 ∧ π‘ˆ β‰  𝑍))
4644, 8, 45sylanbrc 582 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
47 grpomndo 37210 . . . . . . . . . . . . . 14 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ MndOp)
48 mndoismgmOLD 37205 . . . . . . . . . . . . . 14 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ MndOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
4947, 48syl 17 . . . . . . . . . . . . 13 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
5049adantl 481 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
51 eqid 2731 . . . . . . . . . . . . 13 ran 𝐻 = ran 𝐻
52 eqid 2731 . . . . . . . . . . . . 13 (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
5351, 6, 52exidresid 37214 . . . . . . . . . . . 12 (((𝐻 ∈ (Magma ∩ ExId ) ∧ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻 ∧ π‘ˆ ∈ (𝑋 βˆ– {𝑍})) ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5436, 40, 46, 50, 53syl31anc 1372 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5554adantr 480 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5632, 55eqtrd 2771 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
57 oveq1 7419 . . . . . . . . . . 11 (𝑦 = ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯))
5857eqeq1d 2733 . . . . . . . . . 10 (𝑦 = ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) β†’ ((𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ))
5958rspcev 3612 . . . . . . . . 9 ((((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∧ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6029, 56, 59syl2anc 583 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6125, 60syldan 590 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6223adantr 480 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
6362rexeqdv 3325 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ))
64 ovres 7577 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋 βˆ– {𝑍}) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (𝑦𝐻π‘₯))
6564ancoms 458 . . . . . . . . . . 11 ((π‘₯ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑦 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (𝑦𝐻π‘₯))
6665eqeq1d 2733 . . . . . . . . . 10 ((π‘₯ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑦 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ (𝑦𝐻π‘₯) = π‘ˆ))
6766rexbidva 3175 . . . . . . . . 9 (π‘₯ ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
6867adantl 481 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
6963, 68bitrd 279 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
7061, 69mpbid 231 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)
7170ralrimiva 3145 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)
728, 71jca 511 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
731fvexi 6905 . . . . . . . 8 𝐺 ∈ V
7473rnex 7907 . . . . . . 7 ran 𝐺 ∈ V
754, 74eqeltri 2828 . . . . . 6 𝑋 ∈ V
76 difexg 5327 . . . . . 6 (𝑋 ∈ V β†’ (𝑋 βˆ– {𝑍}) ∈ V)
7775, 76mp1i 13 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝑋 βˆ– {𝑍}) ∈ V)
7814ffnd 6718 . . . . . . . 8 (𝑅 ∈ RingOps β†’ 𝐻 Fn (𝑋 Γ— 𝑋))
7978adantr 480 . . . . . . 7 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ 𝐻 Fn (𝑋 Γ— 𝑋))
80 fnssres 6673 . . . . . . 7 ((𝐻 Fn (𝑋 Γ— 𝑋) ∧ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
8179, 13, 80sylancl 585 . . . . . 6 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
82 ovres 7577 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
8382adantl 481 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
84 eldifi 4126 . . . . . . . . . . . 12 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑒 ∈ 𝑋)
85 eldifi 4126 . . . . . . . . . . . 12 (𝑣 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑣 ∈ 𝑋)
8684, 85anim12i 612 . . . . . . . . . . 11 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋))
871, 2, 4rngocl 37236 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
88873expb 1119 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
8986, 88sylan2 592 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
9089adantlr 712 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
91 oveq2 7420 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑒 β†’ (𝑦𝐻π‘₯) = (𝑦𝐻𝑒))
9291eqeq1d 2733 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑒 β†’ ((𝑦𝐻π‘₯) = π‘ˆ ↔ (𝑦𝐻𝑒) = π‘ˆ))
9392rexbidv 3177 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ))
9493rspcv 3608 . . . . . . . . . . . . 13 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ))
9594imdistanri 569 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})))
96 eldifsn 4790 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝑋 βˆ– {𝑍}) ↔ (𝑣 ∈ 𝑋 ∧ 𝑣 β‰  𝑍))
97 ssrexv 4051 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 βˆ– {𝑍}) βŠ† 𝑋 β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ β†’ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ))
9811, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ β†’ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ)
991, 2, 3, 4, 6zerdivemp1x 37282 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
10098, 99syl3an3 1164 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
10184, 100syl3an2 1163 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
1021013expb 1119 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
103102imp 406 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ 𝑋) β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍))
104103necon3d 2960 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ 𝑋) β†’ (𝑣 β‰  𝑍 β†’ (𝑒𝐻𝑣) β‰  𝑍))
105104impr 454 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ (𝑣 ∈ 𝑋 ∧ 𝑣 β‰  𝑍)) β†’ (𝑒𝐻𝑣) β‰  𝑍)
10696, 105sylan2b 593 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒𝐻𝑣) β‰  𝑍)
107106an32s 649 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) β†’ (𝑒𝐻𝑣) β‰  𝑍)
108107ancom2s 647 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
10995, 108sylan2 592 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
110109an42s 658 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
111110adantlrl 717 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
112 eldifsn 4790 . . . . . . . . 9 ((𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}) ↔ ((𝑒𝐻𝑣) ∈ 𝑋 ∧ (𝑒𝐻𝑣) β‰  𝑍))
11390, 111, 112sylanbrc 582 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}))
11483, 113eqeltrd 2832 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍}))
115114ralrimivva 3199 . . . . . 6 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ βˆ€π‘’ ∈ (𝑋 βˆ– {𝑍})βˆ€π‘£ ∈ (𝑋 βˆ– {𝑍})(𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍}))
116 ffnov 7538 . . . . . 6 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ↔ ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) ∧ βˆ€π‘’ ∈ (𝑋 βˆ– {𝑍})βˆ€π‘£ ∈ (𝑋 βˆ– {𝑍})(𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍})))
11781, 115, 116sylanbrc 582 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}))
1181133adantr3 1170 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}))
119 simpr3 1195 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ 𝑀 ∈ (𝑋 βˆ– {𝑍}))
120118, 119ovresd 7578 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = ((𝑒𝐻𝑣)𝐻𝑀))
121823adant3 1131 . . . . . . . 8 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
122121adantl 481 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
123122oveq1d 7427 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = ((𝑒𝐻𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀))
124 ovres 7577 . . . . . . . . . 10 ((𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
1251243adant1 1129 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
126125adantl 481 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
127126oveq2d 7428 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = (𝑒𝐻(𝑣𝐻𝑀)))
128 simpr1 1193 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ 𝑒 ∈ (𝑋 βˆ– {𝑍}))
129 fovcdm 7581 . . . . . . . . . 10 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
1301293adant3r1 1181 . . . . . . . . 9 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
131117, 130sylan 579 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
132128, 131ovresd 7578 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = (𝑒𝐻(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)))
133 eldifi 4126 . . . . . . . . . 10 (𝑀 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑀 ∈ 𝑋)
13484, 85, 1333anim123i 1150 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋))
1351, 2, 4rngoass 37241 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋)) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
136134, 135sylan2 592 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
137136adantlr 712 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
138127, 132, 1373eqtr4d 2781 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = ((𝑒𝐻𝑣)𝐻𝑀))
139120, 123, 1383eqtr4d 2781 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)))
14043anim1i 614 . . . . . . 7 ((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) β†’ (π‘ˆ ∈ 𝑋 ∧ π‘ˆ β‰  𝑍))
141140, 45sylibr 233 . . . . . 6 ((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
142141adantrr 714 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
143 ovres 7577 . . . . . . . 8 ((π‘ˆ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (π‘ˆπ»π‘’))
144141, 143sylan 579 . . . . . . 7 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (π‘ˆπ»π‘’))
1452, 42, 6rngolidm 37272 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋) β†’ (π‘ˆπ»π‘’) = 𝑒)
14684, 145sylan2 592 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆπ»π‘’) = 𝑒)
147146adantlr 712 . . . . . . 7 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆπ»π‘’) = 𝑒)
148144, 147eqtrd 2771 . . . . . 6 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = 𝑒)
149148adantlrr 718 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = 𝑒)
15093rspcva 3610 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)
151 oveq1 7419 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦𝐻𝑒) = (𝑧𝐻𝑒))
152151eqeq1d 2733 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((𝑦𝐻𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
153152cbvrexvw 3234 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ)
154 ovres 7577 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (𝑧𝐻𝑒))
155154eqeq1d 2733 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
156155ancoms 458 . . . . . . . . . . . 12 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑧 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
157156rexbidva 3175 . . . . . . . . . . 11 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ))
158157biimpar 477 . . . . . . . . . 10 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
159153, 158sylan2b 593 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
160150, 159syldan 590 . . . . . . . 8 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
161160ancoms 458 . . . . . . 7 ((βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
162161adantll 711 . . . . . 6 (((𝑅 ∈ RingOps ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
163162adantlrl 717 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
16477, 117, 139, 142, 149, 163isgrpda 37290 . . . 4 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp)
16572, 164impbida 798 . . 3 (𝑅 ∈ RingOps β†’ ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ↔ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
166165pm5.32i 574 . 2 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
1675, 166bitri 275 1 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   βˆ– cdif 3945   ∩ cin 3947   βŠ† wss 3948  {csn 4628   Γ— cxp 5674  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7412  1st c1st 7977  2nd c2nd 7978  GrpOpcgr 30177  GIdcgi 30178  invcgn 30179   ExId cexid 37179  Magmacmagm 37183  MndOpcmndo 37201  RingOpscrngo 37229  DivRingOpscdrng 37283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-1st 7979  df-2nd 7980  df-1o 8472  df-en 8946  df-grpo 30181  df-gid 30182  df-ginv 30183  df-ablo 30233  df-ass 37178  df-exid 37180  df-mgmOLD 37184  df-sgrOLD 37196  df-mndo 37202  df-rngo 37230  df-drngo 37284
This theorem is referenced by:  isdrngo3  37294  divrngidl  37363
  Copyright terms: Public domain W3C validator