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 36814
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 36812 . 2 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp))
6 isdivrng2.5 . . . . . . 7 π‘ˆ = (GIdβ€˜π»)
71, 2, 4, 3, 6dvrunz 36810 . . . . . 6 (𝑅 ∈ DivRingOps β†’ π‘ˆ β‰  𝑍)
85, 7sylbir 234 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ β‰  𝑍)
9 grporndm 29750 . . . . . . . . . . . 12 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
109adantl 482 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
11 difss 4130 . . . . . . . . . . . . . . . . 17 (𝑋 βˆ– {𝑍}) βŠ† 𝑋
12 xpss12 5690 . . . . . . . . . . . . . . . . 17 (((𝑋 βˆ– {𝑍}) βŠ† 𝑋 ∧ (𝑋 βˆ– {𝑍}) βŠ† 𝑋) β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋))
1311, 11, 12mp2an 690 . . . . . . . . . . . . . . . 16 ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋)
141, 2, 4rngosm 36756 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps β†’ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹)
1514fdmd 6725 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps β†’ dom 𝐻 = (𝑋 Γ— 𝑋))
1613, 15sseqtrrid 4034 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻)
1716adantr 481 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻)
18 ssdmres 6002 . . . . . . . . . . . . . 14 (((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† dom 𝐻 ↔ dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
1917, 18sylib 217 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
2019dmeqd 5903 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = dom ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
21 dmxpid 5927 . . . . . . . . . . . 12 dom ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) = (𝑋 βˆ– {𝑍})
2220, 21eqtrdi 2788 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ dom dom (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
2310, 22eqtrd 2772 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
2423eleq2d 2819 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ↔ π‘₯ ∈ (𝑋 βˆ– {𝑍})))
2524biimpar 478 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
26 eqid 2732 . . . . . . . . . . 11 ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
27 eqid 2732 . . . . . . . . . . 11 (invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = (invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
2826, 27grpoinvcl 29764 . . . . . . . . . 10 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
2928adantll 712 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
30 eqid 2732 . . . . . . . . . . . 12 (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))
3126, 30, 27grpolinv 29766 . . . . . . . . . . 11 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))))
3231adantll 712 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))))
332rngomndo 36791 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ 𝐻 ∈ MndOp)
34 mndomgmid 36727 . . . . . . . . . . . . . 14 (𝐻 ∈ MndOp β†’ 𝐻 ∈ (Magma ∩ ExId ))
3533, 34syl 17 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps β†’ 𝐻 ∈ (Magma ∩ ExId ))
3635adantr 481 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ 𝐻 ∈ (Magma ∩ ExId ))
3711, 4sseqtri 4017 . . . . . . . . . . . . . 14 (𝑋 βˆ– {𝑍}) βŠ† ran 𝐺
382, 1rngorn1eq 36790 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ ran 𝐺 = ran 𝐻)
3937, 38sseqtrid 4033 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps β†’ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻)
4039adantr 481 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻)
411rneqi 5934 . . . . . . . . . . . . . . . 16 ran 𝐺 = ran (1st β€˜π‘…)
424, 41eqtri 2760 . . . . . . . . . . . . . . 15 𝑋 = ran (1st β€˜π‘…)
4342, 2, 6rngo1cl 36795 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps β†’ π‘ˆ ∈ 𝑋)
4443adantr 481 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ ∈ 𝑋)
45 eldifsn 4789 . . . . . . . . . . . . 13 (π‘ˆ ∈ (𝑋 βˆ– {𝑍}) ↔ (π‘ˆ ∈ 𝑋 ∧ π‘ˆ β‰  𝑍))
4644, 8, 45sylanbrc 583 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
47 grpomndo 36731 . . . . . . . . . . . . . 14 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ MndOp)
48 mndoismgmOLD 36726 . . . . . . . . . . . . . 14 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ MndOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
4947, 48syl 17 . . . . . . . . . . . . 13 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
5049adantl 482 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma)
51 eqid 2732 . . . . . . . . . . . . 13 ran 𝐻 = ran 𝐻
52 eqid 2732 . . . . . . . . . . . . 13 (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
5351, 6, 52exidresid 36735 . . . . . . . . . . . 12 (((𝐻 ∈ (Magma ∩ ExId ) ∧ (𝑋 βˆ– {𝑍}) βŠ† ran 𝐻 ∧ π‘ˆ ∈ (𝑋 βˆ– {𝑍})) ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ Magma) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5436, 40, 46, 50, 53syl31anc 1373 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5554adantr 481 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (GIdβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) = π‘ˆ)
5632, 55eqtrd 2772 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
57 oveq1 7412 . . . . . . . . . . 11 (𝑦 = ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯))
5857eqeq1d 2734 . . . . . . . . . 10 (𝑦 = ((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) β†’ ((𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ))
5958rspcev 3612 . . . . . . . . 9 ((((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯) ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∧ (((invβ€˜(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))))β€˜π‘₯)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6029, 56, 59syl2anc 584 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6125, 60syldan 591 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ)
6223adantr 481 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) = (𝑋 βˆ– {𝑍}))
6362rexeqdv 3326 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ))
64 ovres 7569 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋 βˆ– {𝑍}) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (𝑦𝐻π‘₯))
6564ancoms 459 . . . . . . . . . . 11 ((π‘₯ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑦 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = (𝑦𝐻π‘₯))
6665eqeq1d 2734 . . . . . . . . . 10 ((π‘₯ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑦 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ (𝑦𝐻π‘₯) = π‘ˆ))
6766rexbidva 3176 . . . . . . . . 9 (π‘₯ ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
6867adantl 482 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
6963, 68bitrd 278 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ ran (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑦(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
7061, 69mpbid 231 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ∧ π‘₯ ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)
7170ralrimiva 3146 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)
728, 71jca 512 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) β†’ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ))
731fvexi 6902 . . . . . . . 8 𝐺 ∈ V
7473rnex 7899 . . . . . . 7 ran 𝐺 ∈ V
754, 74eqeltri 2829 . . . . . 6 𝑋 ∈ V
76 difexg 5326 . . . . . 6 (𝑋 ∈ V β†’ (𝑋 βˆ– {𝑍}) ∈ V)
7775, 76mp1i 13 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝑋 βˆ– {𝑍}) ∈ V)
7814ffnd 6715 . . . . . . . 8 (𝑅 ∈ RingOps β†’ 𝐻 Fn (𝑋 Γ— 𝑋))
7978adantr 481 . . . . . . 7 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ 𝐻 Fn (𝑋 Γ— 𝑋))
80 fnssres 6670 . . . . . . 7 ((𝐻 Fn (𝑋 Γ— 𝑋) ∧ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
8179, 13, 80sylancl 586 . . . . . 6 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))
82 ovres 7569 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
8382adantl 482 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
84 eldifi 4125 . . . . . . . . . . . 12 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑒 ∈ 𝑋)
85 eldifi 4125 . . . . . . . . . . . 12 (𝑣 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑣 ∈ 𝑋)
8684, 85anim12i 613 . . . . . . . . . . 11 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋))
871, 2, 4rngocl 36757 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
88873expb 1120 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
8986, 88sylan2 593 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
9089adantlr 713 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ 𝑋)
91 oveq2 7413 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑒 β†’ (𝑦𝐻π‘₯) = (𝑦𝐻𝑒))
9291eqeq1d 2734 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑒 β†’ ((𝑦𝐻π‘₯) = π‘ˆ ↔ (𝑦𝐻𝑒) = π‘ˆ))
9392rexbidv 3178 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ↔ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ))
9493rspcv 3608 . . . . . . . . . . . . 13 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ))
9594imdistanri 570 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})))
96 eldifsn 4789 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝑋 βˆ– {𝑍}) ↔ (𝑣 ∈ 𝑋 ∧ 𝑣 β‰  𝑍))
97 ssrexv 4050 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 βˆ– {𝑍}) βŠ† 𝑋 β†’ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ β†’ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ))
9811, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ β†’ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ)
991, 2, 3, 4, 6zerdivemp1x 36803 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ βˆƒπ‘¦ ∈ 𝑋 (𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
10098, 99syl3an3 1165 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋 ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
10184, 100syl3an2 1164 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
1021013expb 1120 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) β†’ (𝑣 ∈ 𝑋 β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍)))
103102imp 407 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ 𝑋) β†’ ((𝑒𝐻𝑣) = 𝑍 β†’ 𝑣 = 𝑍))
104103necon3d 2961 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ 𝑋) β†’ (𝑣 β‰  𝑍 β†’ (𝑒𝐻𝑣) β‰  𝑍))
105104impr 455 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ (𝑣 ∈ 𝑋 ∧ 𝑣 β‰  𝑍)) β†’ (𝑒𝐻𝑣) β‰  𝑍)
10696, 105sylan2b 594 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒𝐻𝑣) β‰  𝑍)
107106an32s 650 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)) β†’ (𝑒𝐻𝑣) β‰  𝑍)
108107ancom2s 648 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
10995, 108sylan2 593 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍})) ∧ (βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
110109an42s 659 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
111110adantlrl 718 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) β‰  𝑍)
112 eldifsn 4789 . . . . . . . . 9 ((𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}) ↔ ((𝑒𝐻𝑣) ∈ 𝑋 ∧ (𝑒𝐻𝑣) β‰  𝑍))
11390, 111, 112sylanbrc 583 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}))
11483, 113eqeltrd 2833 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍}))
115114ralrimivva 3200 . . . . . 6 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ βˆ€π‘’ ∈ (𝑋 βˆ– {𝑍})βˆ€π‘£ ∈ (𝑋 βˆ– {𝑍})(𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍}))
116 ffnov 7531 . . . . . 6 ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ↔ ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) Fn ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})) ∧ βˆ€π‘’ ∈ (𝑋 βˆ– {𝑍})βˆ€π‘£ ∈ (𝑋 βˆ– {𝑍})(𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) ∈ (𝑋 βˆ– {𝑍})))
11781, 115, 116sylanbrc 583 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}))
1181133adantr3 1171 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻𝑣) ∈ (𝑋 βˆ– {𝑍}))
119 simpr3 1196 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ 𝑀 ∈ (𝑋 βˆ– {𝑍}))
120118, 119ovresd 7570 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = ((𝑒𝐻𝑣)𝐻𝑀))
121823adant3 1132 . . . . . . . 8 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
122121adantl 482 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣) = (𝑒𝐻𝑣))
123122oveq1d 7420 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = ((𝑒𝐻𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀))
124 ovres 7569 . . . . . . . . . 10 ((𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
1251243adant1 1130 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
126125adantl 482 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑣𝐻𝑀))
127126oveq2d 7421 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒𝐻(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = (𝑒𝐻(𝑣𝐻𝑀)))
128 simpr1 1194 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ 𝑒 ∈ (𝑋 βˆ– {𝑍}))
129 fovcdm 7573 . . . . . . . . . 10 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
1301293adant3r1 1182 . . . . . . . . 9 (((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))):((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))⟢(𝑋 βˆ– {𝑍}) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
131117, 130sylan 580 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) ∈ (𝑋 βˆ– {𝑍}))
132128, 131ovresd 7570 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = (𝑒𝐻(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)))
133 eldifi 4125 . . . . . . . . . 10 (𝑀 ∈ (𝑋 βˆ– {𝑍}) β†’ 𝑀 ∈ 𝑋)
13484, 85, 1333anim123i 1151 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋))
1351, 2, 4rngoass 36762 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋)) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
136134, 135sylan2 593 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
137136adantlr 713 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒𝐻𝑣)𝐻𝑀) = (𝑒𝐻(𝑣𝐻𝑀)))
138127, 132, 1373eqtr4d 2782 . . . . . 6 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)) = ((𝑒𝐻𝑣)𝐻𝑀))
139120, 123, 1383eqtr4d 2782 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ (𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑣 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑀 ∈ (𝑋 βˆ– {𝑍}))) β†’ ((𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑣)(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀) = (𝑒(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))(𝑣(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑀)))
14043anim1i 615 . . . . . . 7 ((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) β†’ (π‘ˆ ∈ 𝑋 ∧ π‘ˆ β‰  𝑍))
141140, 45sylibr 233 . . . . . 6 ((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
142141adantrr 715 . . . . 5 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ π‘ˆ ∈ (𝑋 βˆ– {𝑍}))
143 ovres 7569 . . . . . . . 8 ((π‘ˆ ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (π‘ˆπ»π‘’))
144141, 143sylan 580 . . . . . . 7 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (π‘ˆπ»π‘’))
1452, 42, 6rngolidm 36793 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ 𝑋) β†’ (π‘ˆπ»π‘’) = 𝑒)
14684, 145sylan2 593 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆπ»π‘’) = 𝑒)
147146adantlr 713 . . . . . . 7 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆπ»π‘’) = 𝑒)
148144, 147eqtrd 2772 . . . . . 6 (((𝑅 ∈ RingOps ∧ π‘ˆ β‰  𝑍) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = 𝑒)
149148adantlrr 719 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (π‘ˆ(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = 𝑒)
15093rspcva 3610 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) β†’ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ)
151 oveq1 7412 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (𝑦𝐻𝑒) = (𝑧𝐻𝑒))
152151eqeq1d 2734 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((𝑦𝐻𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
153152cbvrexvw 3235 . . . . . . . . . 10 (βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ)
154 ovres 7569 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ (𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = (𝑧𝐻𝑒))
155154eqeq1d 2734 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
156155ancoms 459 . . . . . . . . . . . 12 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ 𝑧 ∈ (𝑋 βˆ– {𝑍})) β†’ ((𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ (𝑧𝐻𝑒) = π‘ˆ))
157156rexbidva 3176 . . . . . . . . . . 11 (𝑒 ∈ (𝑋 βˆ– {𝑍}) β†’ (βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ ↔ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ))
158157biimpar 478 . . . . . . . . . 10 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧𝐻𝑒) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
159153, 158sylan2b 594 . . . . . . . . 9 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻𝑒) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
160150, 159syldan 591 . . . . . . . 8 ((𝑒 ∈ (𝑋 βˆ– {𝑍}) ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
161160ancoms 459 . . . . . . 7 ((βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
162161adantll 712 . . . . . 6 (((𝑅 ∈ RingOps ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
163162adantlrl 718 . . . . 5 (((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) ∧ 𝑒 ∈ (𝑋 βˆ– {𝑍})) β†’ βˆƒπ‘§ ∈ (𝑋 βˆ– {𝑍})(𝑧(𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍})))𝑒) = π‘ˆ)
16477, 117, 139, 142, 149, 163isgrpda 36811 . . . 4 ((𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)) β†’ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp)
16572, 164impbida 799 . . 3 (𝑅 ∈ RingOps β†’ ((𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp ↔ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
166165pm5.32i 575 . 2 ((𝑅 ∈ RingOps ∧ (𝐻 β†Ύ ((𝑋 βˆ– {𝑍}) Γ— (𝑋 βˆ– {𝑍}))) ∈ GrpOp) ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
1675, 166bitri 274 1 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (π‘ˆ β‰  𝑍 ∧ βˆ€π‘₯ ∈ (𝑋 βˆ– {𝑍})βˆƒπ‘¦ ∈ (𝑋 βˆ– {𝑍})(𝑦𝐻π‘₯) = π‘ˆ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  {csn 4627   Γ— cxp 5673  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970  GrpOpcgr 29729  GIdcgi 29730  invcgn 29731   ExId cexid 36700  Magmacmagm 36704  MndOpcmndo 36722  RingOpscrngo 36750  DivRingOpscdrng 36804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-1st 7971  df-2nd 7972  df-1o 8462  df-en 8936  df-grpo 29733  df-gid 29734  df-ginv 29735  df-ablo 29785  df-ass 36699  df-exid 36701  df-mgmOLD 36705  df-sgrOLD 36717  df-mndo 36723  df-rngo 36751  df-drngo 36805
This theorem is referenced by:  isdrngo3  36815  divrngidl  36884
  Copyright terms: Public domain W3C validator