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 36420
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 36418 . 2 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp))
6 isdivrng2.5 . . . . . . 7 π‘ˆ = (GIdβ€˜π»)
71, 2, 4, 3, 6dvrunz 36416 . . . . . 6 (𝑅 ∈ DivRingOps β†’ π‘ˆ β‰  𝑍)
85, 7sylbir 234 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ β‰  𝑍)
9 grporndm 29455 . . . . . . . . . . . 12 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
109adantl 483 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
11 difss 4092 . . . . . . . . . . . . . . . . 17 (𝑋 βˆ– {𝑍}) βŠ† 𝑋
12 xpss12 5649 . . . . . . . . . . . . . . . . 17 (((𝑋 βˆ– {𝑍}) βŠ† 𝑋 ∧ (𝑋 βˆ– {𝑍}) βŠ† 𝑋) β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋))
1311, 11, 12mp2an 691 . . . . . . . . . . . . . . . 16 ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋)
141, 2, 4rngosm 36362 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps β†’ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹)
1514fdmd 6680 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps β†’ dom 𝐻 = (𝑋 Γ— 𝑋))
1613, 15sseqtrrid 3998 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻)
1716adantr 482 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻)
18 ssdmres 5961 . . . . . . . . . . . . . 14 (((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻 ↔ dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
1917, 18sylib 217 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
2019dmeqd 5862 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
21 dmxpid 5886 . . . . . . . . . . . 12 dom ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) = (𝑋 βˆ– {𝑍})
2220, 21eqtrdi 2793 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
2310, 22eqtrd 2777 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
2423eleq2d 2824 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ↔ π‘₯ ∈ (𝑋 βˆ– {𝑍})))
2524biimpar 479 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
26 eqid 2737 . . . . . . . . . . 11 ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
27 eqid 2737 . . . . . . . . . . 11 (invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = (invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
2826, 27grpoinvcl 29469 . . . . . . . . . 10 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
2928adantll 713 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
30 eqid 2737 . . . . . . . . . . . 12 (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
3126, 30, 27grpolinv 29471 . . . . . . . . . . 11 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))))
3231adantll 713 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))))
332rngomndo 36397 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ 𝐻 ∈ MndOp)
34 mndomgmid 36333 . . . . . . . . . . . . . 14 (𝐻 ∈ MndOp β†’ 𝐻 ∈ (Magma ∩ ExId ))
3533, 34syl 17 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps β†’ 𝐻 ∈ (Magma ∩ ExId ))
3635adantr 482 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ 𝐻 ∈ (Magma ∩ ExId ))
3711, 4sseqtri 3981 . . . . . . . . . . . . . 14 (𝑋 βˆ– {𝑍}) βŠ† ran 𝐺
382, 1rngorn1eq 36396 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ ran 𝐺 = ran 𝐻)
3937, 38sseqtrid 3997 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps β†’ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻)
4039adantr 482 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻)
411rneqi 5893 . . . . . . . . . . . . . . . 16 ran 𝐺 = ran (1st β€˜π‘…)
424, 41eqtri 2765 . . . . . . . . . . . . . . 15 𝑋 = ran (1st β€˜π‘…)
4342, 2, 6rngo1cl 36401 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ π‘ˆ ∈ 𝑋)
4443adantr 482 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ ∈ 𝑋)
45 eldifsn 4748 . . . . . . . . . . . . 13 (π‘ˆ ∈ (𝑋 βˆ– {𝑍}) ↔ (π‘ˆ ∈ 𝑋 ∧ π‘ˆ β‰  𝑍))
4644, 8, 45sylanbrc 584 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
47 grpomndo 36337 . . . . . . . . . . . . . 14 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ MndOp)
48 mndoismgmOLD 36332 . . . . . . . . . . . . . 14 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ MndOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
4947, 48syl 17 . . . . . . . . . . . . 13 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
5049adantl 483 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
51 eqid 2737 . . . . . . . . . . . . 13 ran 𝐻 = ran 𝐻
52 eqid 2737 . . . . . . . . . . . . 13 (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
5351, 6, 52exidresid 36341 . . . . . . . . . . . 12 (((𝐻 ∈ (Magma ∩ ExId ) ∧ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻 ∧ π‘ˆ ∈ (𝑋 βˆ– {𝑍})) ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5436, 40, 46, 50, 53syl31anc 1374 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5554adantr 482 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5632, 55eqtrd 2777 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
57 oveq1 7365 . . . . . . . . . . 11 (𝑦 = ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯))
5857eqeq1d 2739 . . . . . . . . . 10 (𝑦 = ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) β†’ ((𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ))
5958rspcev 3582 . . . . . . . . 9 ((((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∧ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6029, 56, 59syl2anc 585 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6125, 60syldan 592 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6223adantr 482 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
6362rexeqdv 3315 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ))
64 ovres 7521 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋 βˆ– {𝑍}) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (𝑦𝐻π‘₯))
6564ancoms 460 . . . . . . . . . . 11 ((π‘₯ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑦 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (𝑦𝐻π‘₯))
6665eqeq1d 2739 . . . . . . . . . 10 ((π‘₯ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑦 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ (𝑦𝐻π‘₯) = π‘ˆ))
6766rexbidva 3174 . . . . . . . . 9 (π‘₯ ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
6867adantl 483 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
6963, 68bitrd 279 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
7061, 69mpbid 231 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)
7170ralrimiva 3144 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)
728, 71jca 513 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
731fvexi 6857 . . . . . . . 8 𝐺 ∈ V
7473rnex 7850 . . . . . . 7 ran 𝐺 ∈ V
754, 74eqeltri 2834 . . . . . 6 𝑋 ∈ V
76 difexg 5285 . . . . . 6 (𝑋 ∈ V β†’ (𝑋 βˆ– {𝑍}) ∈ V)
7775, 76mp1i 13 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝑋 βˆ– {𝑍}) ∈ V)
7814ffnd 6670 . . . . . . . 8 (𝑅 ∈ RingOps β†’ 𝐻 Fn (𝑋 Γ— 𝑋))
7978adantr 482 . . . . . . 7 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ 𝐻 Fn (𝑋 Γ— 𝑋))
80 fnssres 6625 . . . . . . 7 ((𝐻 Fn (𝑋 Γ— 𝑋) ∧ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
8179, 13, 80sylancl 587 . . . . . 6 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
82 ovres 7521 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
8382adantl 483 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
84 eldifi 4087 . . . . . . . . . . . 12 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑒 ∈ 𝑋)
85 eldifi 4087 . . . . . . . . . . . 12 (𝑣 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑣 ∈ 𝑋)
8684, 85anim12i 614 . . . . . . . . . . 11 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋))
871, 2, 4rngocl 36363 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
88873expb 1121 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
8986, 88sylan2 594 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
9089adantlr 714 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
91 oveq2 7366 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑒 β†’ (𝑦𝐻π‘₯) = (𝑦𝐻𝑒))
9291eqeq1d 2739 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑒 β†’ ((𝑦𝐻π‘₯) = π‘ˆ ↔ (𝑦𝐻𝑒) = π‘ˆ))
9392rexbidv 3176 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ))
9493rspcv 3578 . . . . . . . . . . . . 13 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ))
9594imdistanri 571 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})))
96 eldifsn 4748 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝑋 βˆ– {𝑍}) ↔ (𝑣 ∈ 𝑋 ∧ 𝑣 β‰  𝑍))
97 ssrexv 4012 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 βˆ– {𝑍}) βŠ† 𝑋 β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ β†’ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ))
9811, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ β†’ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ)
991, 2, 3, 4, 6zerdivemp1x 36409 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
10098, 99syl3an3 1166 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
10184, 100syl3an2 1165 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
1021013expb 1121 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
103102imp 408 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ 𝑋) β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍))
104103necon3d 2965 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ 𝑋) β†’ (𝑣 β‰  𝑍 β†’ (𝑒𝐻𝑣) β‰  𝑍))
105104impr 456 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ (𝑣 ∈ 𝑋 ∧ 𝑣 β‰  𝑍)) β†’ (𝑒𝐻𝑣) β‰  𝑍)
10696, 105sylan2b 595 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒𝐻𝑣) β‰  𝑍)
107106an32s 651 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) β†’ (𝑒𝐻𝑣) β‰  𝑍)
108107ancom2s 649 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
10995, 108sylan2 594 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
110109an42s 660 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
111110adantlrl 719 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
112 eldifsn 4748 . . . . . . . . 9 ((𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}) ↔ ((𝑒𝐻𝑣) ∈ 𝑋 ∧ (𝑒𝐻𝑣) β‰  𝑍))
11390, 111, 112sylanbrc 584 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}))
11483, 113eqeltrd 2838 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍}))
115114ralrimivva 3198 . . . . . 6 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ βˆ€π‘’ ∈ (𝑋 βˆ– {𝑍})βˆ€π‘£ ∈ (𝑋 βˆ– {𝑍})(𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍}))
116 ffnov 7484 . . . . . 6 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ↔ ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) ∧ βˆ€π‘’ ∈ (𝑋 βˆ– {𝑍})βˆ€π‘£ ∈ (𝑋 βˆ– {𝑍})(𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍})))
11781, 115, 116sylanbrc 584 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}))
1181133adantr3 1172 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}))
119 simpr3 1197 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ 𝑀 ∈ (𝑋 βˆ– {𝑍}))
120118, 119ovresd 7522 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = ((𝑒𝐻𝑣)𝐻𝑀))
121823adant3 1133 . . . . . . . 8 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
122121adantl 483 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
123122oveq1d 7373 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = ((𝑒𝐻𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀))
124 ovres 7521 . . . . . . . . . 10 ((𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
1251243adant1 1131 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
126125adantl 483 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
127126oveq2d 7374 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = (𝑒𝐻(𝑣𝐻𝑀)))
128 simpr1 1195 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ 𝑒 ∈ (𝑋 βˆ– {𝑍}))
129 fovcdm 7525 . . . . . . . . . 10 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
1301293adant3r1 1183 . . . . . . . . 9 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
131117, 130sylan 581 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
132128, 131ovresd 7522 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = (𝑒𝐻(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)))
133 eldifi 4087 . . . . . . . . . 10 (𝑀 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑀 ∈ 𝑋)
13484, 85, 1333anim123i 1152 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋))
1351, 2, 4rngoass 36368 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋)) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
136134, 135sylan2 594 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
137136adantlr 714 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
138127, 132, 1373eqtr4d 2787 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = ((𝑒𝐻𝑣)𝐻𝑀))
139120, 123, 1383eqtr4d 2787 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)))
14043anim1i 616 . . . . . . 7 ((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) β†’ (π‘ˆ ∈ 𝑋 ∧ π‘ˆ β‰  𝑍))
141140, 45sylibr 233 . . . . . 6 ((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
142141adantrr 716 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
143 ovres 7521 . . . . . . . 8 ((π‘ˆ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (π‘ˆπ»π‘’))
144141, 143sylan 581 . . . . . . 7 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (π‘ˆπ»π‘’))
1452, 42, 6rngolidm 36399 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋) β†’ (π‘ˆπ»π‘’) = 𝑒)
14684, 145sylan2 594 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆπ»π‘’) = 𝑒)
147146adantlr 714 . . . . . . 7 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆπ»π‘’) = 𝑒)
148144, 147eqtrd 2777 . . . . . 6 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = 𝑒)
149148adantlrr 720 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = 𝑒)
15093rspcva 3580 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)
151 oveq1 7365 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦𝐻𝑒) = (𝑧𝐻𝑒))
152151eqeq1d 2739 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((𝑦𝐻𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
153152cbvrexvw 3227 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ)
154 ovres 7521 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (𝑧𝐻𝑒))
155154eqeq1d 2739 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
156155ancoms 460 . . . . . . . . . . . 12 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑧 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
157156rexbidva 3174 . . . . . . . . . . 11 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ))
158157biimpar 479 . . . . . . . . . 10 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
159153, 158sylan2b 595 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
160150, 159syldan 592 . . . . . . . 8 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
161160ancoms 460 . . . . . . 7 ((βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
162161adantll 713 . . . . . 6 (((𝑅 ∈ RingOps ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
163162adantlrl 719 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
16477, 117, 139, 142, 149, 163isgrpda 36417 . . . 4 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp)
16572, 164impbida 800 . . 3 (𝑅 ∈ RingOps β†’ ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ↔ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
166165pm5.32i 576 . 2 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
1675, 166bitri 275 1 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3446   βˆ– cdif 3908   ∩ cin 3910   βŠ† wss 3911  {csn 4587   Γ— cxp 5632  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  1st c1st 7920  2nd c2nd 7921  GrpOpcgr 29434  GIdcgi 29435  invcgn 29436   ExId cexid 36306  Magmacmagm 36310  MndOpcmndo 36328  RingOpscrngo 36356  DivRingOpscdrng 36410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-1st 7922  df-2nd 7923  df-1o 8413  df-en 8885  df-grpo 29438  df-gid 29439  df-ginv 29440  df-ablo 29490  df-ass 36305  df-exid 36307  df-mgmOLD 36311  df-sgrOLD 36323  df-mndo 36329  df-rngo 36357  df-drngo 36411
This theorem is referenced by:  isdrngo3  36421  divrngidl  36490
  Copyright terms: Public domain W3C validator