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 35105
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 35103 . 2 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
6 isdivrng2.5 . . . . . . 7 𝑈 = (GId‘𝐻)
71, 2, 4, 3, 6dvrunz 35101 . . . . . 6 (𝑅 ∈ DivRingOps → 𝑈𝑍)
85, 7sylbir 236 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈𝑍)
9 grporndm 28202 . . . . . . . . . . . 12 ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
109adantl 482 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
11 difss 4111 . . . . . . . . . . . . . . . . 17 (𝑋 ∖ {𝑍}) ⊆ 𝑋
12 xpss12 5568 . . . . . . . . . . . . . . . . 17 (((𝑋 ∖ {𝑍}) ⊆ 𝑋 ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋))
1311, 11, 12mp2an 688 . . . . . . . . . . . . . . . 16 ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)
141, 2, 4rngosm 35047 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋)
1514fdmd 6519 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → dom 𝐻 = (𝑋 × 𝑋))
1613, 15sseqtrrid 4023 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
1716adantr 481 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
18 ssdmres 5874 . . . . . . . . . . . . . 14 (((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻 ↔ dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
1917, 18sylib 219 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
2019dmeqd 5772 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
21 dmxpid 5798 . . . . . . . . . . . 12 dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) = (𝑋 ∖ {𝑍})
2220, 21syl6eq 2876 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
2310, 22eqtrd 2860 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
2423eleq2d 2902 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ↔ 𝑥 ∈ (𝑋 ∖ {𝑍})))
2524biimpar 478 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
26 eqid 2824 . . . . . . . . . . 11 ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
27 eqid 2824 . . . . . . . . . . 11 (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
2826, 27grpoinvcl 28216 . . . . . . . . . 10 (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
2928adantll 710 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
30 eqid 2824 . . . . . . . . . . . 12 (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
3126, 30, 27grpolinv 28218 . . . . . . . . . . 11 (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
3231adantll 710 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
332rngomndo 35082 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
34 mndomgmid 35018 . . . . . . . . . . . . . 14 (𝐻 ∈ MndOp → 𝐻 ∈ (Magma ∩ ExId ))
3533, 34syl 17 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps → 𝐻 ∈ (Magma ∩ ExId ))
3635adantr 481 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝐻 ∈ (Magma ∩ ExId ))
3711, 4sseqtri 4006 . . . . . . . . . . . . . 14 (𝑋 ∖ {𝑍}) ⊆ ran 𝐺
382, 1rngorn1eq 35081 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻)
3937, 38sseqtrid 4022 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
4039adantr 481 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
411rneqi 5805 . . . . . . . . . . . . . . . 16 ran 𝐺 = ran (1st𝑅)
424, 41eqtri 2848 . . . . . . . . . . . . . . 15 𝑋 = ran (1st𝑅)
4342, 2, 6rngo1cl 35086 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps → 𝑈𝑋)
4443adantr 481 . . . . . . . . . . . . 13 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈𝑋)
45 eldifsn 4717 . . . . . . . . . . . . 13 (𝑈 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑈𝑋𝑈𝑍))
4644, 8, 45sylanbrc 583 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
47 grpomndo 35022 . . . . . . . . . . . . . 14 ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp)
48 mndoismgmOLD 35017 . . . . . . . . . . . . . 14 ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
4947, 48syl 17 . . . . . . . . . . . . 13 ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
5049adantl 482 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
51 eqid 2824 . . . . . . . . . . . . 13 ran 𝐻 = ran 𝐻
52 eqid 2824 . . . . . . . . . . . . 13 (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
5351, 6, 52exidresid 35026 . . . . . . . . . . . 12 (((𝐻 ∈ (Magma ∩ ExId ) ∧ (𝑋 ∖ {𝑍}) ⊆ ran 𝐻𝑈 ∈ (𝑋 ∖ {𝑍})) ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
5436, 40, 46, 50, 53syl31anc 1367 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
5554adantr 481 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
5632, 55eqtrd 2860 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
57 oveq1 7158 . . . . . . . . . . 11 (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥))
5857eqeq1d 2826 . . . . . . . . . 10 (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
5958rspcev 3626 . . . . . . . . 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 3421 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
64 ovres 7307 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
6564ancoms 459 . . . . . . . . . . 11 ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
6665eqeq1d 2826 . . . . . . . . . 10 ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (𝑦𝐻𝑥) = 𝑈))
6766rexbidva 3300 . . . . . . . . 9 (𝑥 ∈ (𝑋 ∖ {𝑍}) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
6867adantl 482 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
6963, 68bitrd 280 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
7061, 69mpbid 233 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)
7170ralrimiva 3186 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)
728, 71jca 512 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
731fvexi 6680 . . . . . . . 8 𝐺 ∈ V
7473rnex 7608 . . . . . . 7 ran 𝐺 ∈ V
754, 74eqeltri 2913 . . . . . 6 𝑋 ∈ V
76 difexg 5227 . . . . . 6 (𝑋 ∈ V → (𝑋 ∖ {𝑍}) ∈ V)
7775, 76mp1i 13 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝑋 ∖ {𝑍}) ∈ V)
7814ffnd 6511 . . . . . . . 8 (𝑅 ∈ RingOps → 𝐻 Fn (𝑋 × 𝑋))
7978adantr 481 . . . . . . 7 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝐻 Fn (𝑋 × 𝑋))
80 fnssres 6466 . . . . . . 7 ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
8179, 13, 80sylancl 586 . . . . . 6 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
82 ovres 7307 . . . . . . . . 9 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
8382adantl 482 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
84 eldifi 4106 . . . . . . . . . . . 12 (𝑢 ∈ (𝑋 ∖ {𝑍}) → 𝑢𝑋)
85 eldifi 4106 . . . . . . . . . . . 12 (𝑣 ∈ (𝑋 ∖ {𝑍}) → 𝑣𝑋)
8684, 85anim12i 612 . . . . . . . . . . 11 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢𝑋𝑣𝑋))
871, 2, 4rngocl 35048 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝑢𝑋𝑣𝑋) → (𝑢𝐻𝑣) ∈ 𝑋)
88873expb 1114 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ (𝑢𝑋𝑣𝑋)) → (𝑢𝐻𝑣) ∈ 𝑋)
8986, 88sylan2 592 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
9089adantlr 711 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
91 oveq2 7159 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → (𝑦𝐻𝑥) = (𝑦𝐻𝑢))
9291eqeq1d 2826 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → ((𝑦𝐻𝑥) = 𝑈 ↔ (𝑦𝐻𝑢) = 𝑈))
9392rexbidv 3301 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
9493rspcv 3621 . . . . . . . . . . . . 13 (𝑢 ∈ (𝑋 ∖ {𝑍}) → (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
9594imdistanri 570 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈𝑢 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈𝑢 ∈ (𝑋 ∖ {𝑍})))
96 eldifsn 4717 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑣𝑋𝑣𝑍))
97 ssrexv 4037 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∖ {𝑍}) ⊆ 𝑋 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦𝑋 (𝑦𝐻𝑢) = 𝑈))
9811, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦𝑋 (𝑦𝐻𝑢) = 𝑈)
991, 2, 3, 4, 6zerdivemp1x 35094 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ 𝑢𝑋 ∧ ∃𝑦𝑋 (𝑦𝐻𝑢) = 𝑈) → (𝑣𝑋 → ((𝑢𝐻𝑣) = 𝑍𝑣 = 𝑍)))
10098, 99syl3an3 1159 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ 𝑢𝑋 ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → (𝑣𝑋 → ((𝑢𝐻𝑣) = 𝑍𝑣 = 𝑍)))
10184, 100syl3an2 1158 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → (𝑣𝑋 → ((𝑢𝐻𝑣) = 𝑍𝑣 = 𝑍)))
1021013expb 1114 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) → (𝑣𝑋 → ((𝑢𝐻𝑣) = 𝑍𝑣 = 𝑍)))
103102imp 407 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣𝑋) → ((𝑢𝐻𝑣) = 𝑍𝑣 = 𝑍))
104103necon3d 3041 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣𝑋) → (𝑣𝑍 → (𝑢𝐻𝑣) ≠ 𝑍))
105104impr 455 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ (𝑣𝑋𝑣𝑍)) → (𝑢𝐻𝑣) ≠ 𝑍)
10696, 105sylan2b 593 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢𝐻𝑣) ≠ 𝑍)
107106an32s 648 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) → (𝑢𝐻𝑣) ≠ 𝑍)
108107ancom2s 646 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) ∧ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈𝑢 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
10995, 108sylan2 592 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) ∧ (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈𝑢 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
110109an42s 657 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
111110adantlrl 716 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
112 eldifsn 4717 . . . . . . . . 9 ((𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}) ↔ ((𝑢𝐻𝑣) ∈ 𝑋 ∧ (𝑢𝐻𝑣) ≠ 𝑍))
11390, 111, 112sylanbrc 583 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
11483, 113eqeltrd 2917 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
115114ralrimivva 3195 . . . . . 6 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
116 ffnov 7271 . . . . . 6 ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ↔ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ∧ ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍})))
11781, 115, 116sylanbrc 583 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}))
1181133adantr3 1165 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
119 simpr3 1190 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑤 ∈ (𝑋 ∖ {𝑍}))
120118, 119ovresd 7308 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)𝐻𝑤))
121823adant3 1126 . . . . . . . 8 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
122121adantl 482 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
123122oveq1d 7166 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤))
124 ovres 7307 . . . . . . . . . 10 ((𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
1251243adant1 1124 . . . . . . . . 9 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
126125adantl 482 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
127126oveq2d 7167 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣𝐻𝑤)))
128 simpr1 1188 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑢 ∈ (𝑋 ∖ {𝑍}))
129 fovrn 7311 . . . . . . . . . 10 (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
1301293adant3r1 1176 . . . . . . . . 9 (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
131117, 130sylan 580 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
132128, 131ovresd 7308 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
133 eldifi 4106 . . . . . . . . . 10 (𝑤 ∈ (𝑋 ∖ {𝑍}) → 𝑤𝑋)
13484, 85, 1333anim123i 1145 . . . . . . . . 9 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢𝑋𝑣𝑋𝑤𝑋))
1351, 2, 4rngoass 35053 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ (𝑢𝑋𝑣𝑋𝑤𝑋)) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
136134, 135sylan2 592 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
137136adantlr 711 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
138127, 132, 1373eqtr4d 2870 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = ((𝑢𝐻𝑣)𝐻𝑤))
139120, 123, 1383eqtr4d 2870 . . . . 5 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
14043anim1i 614 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → (𝑈𝑋𝑈𝑍))
141140, 45sylibr 235 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
142141adantrr 713 . . . . 5 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
143 ovres 7307 . . . . . . . 8 ((𝑈 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
144141, 143sylan 580 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑈𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
1452, 42, 6rngolidm 35084 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑢𝑋) → (𝑈𝐻𝑢) = 𝑢)
14684, 145sylan2 592 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
147146adantlr 711 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑈𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
148144, 147eqtrd 2860 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑈𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
149148adantlrr 717 . . . . 5 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
15093rspcva 3624 . . . . . . . . 9 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)
151 oveq1 7158 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝐻𝑢) = (𝑧𝐻𝑢))
152151eqeq1d 2826 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑦𝐻𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
153152cbvrexv 3458 . . . . . . . . . 10 (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ↔ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈)
154 ovres 7307 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑧𝐻𝑢))
155154eqeq1d 2826 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
156155ancoms 459 . . . . . . . . . . . 12 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑧 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
157156rexbidva 3300 . . . . . . . . . . 11 (𝑢 ∈ (𝑋 ∖ {𝑍}) → (∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈))
158157biimpar 478 . . . . . . . . . 10 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
159153, 158sylan2b 593 . . . . . . . . 9 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
160150, 159syldan 591 . . . . . . . 8 ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
161160ancoms 459 . . . . . . 7 ((∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈𝑢 ∈ (𝑋 ∖ {𝑍})) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
162161adantll 710 . . . . . 6 (((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
163162adantlrl 716 . . . . 5 (((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
16477, 117, 139, 142, 149, 163isgrpda 35102 . . . 4 ((𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)
16572, 164impbida 797 . . 3 (𝑅 ∈ RingOps → ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
166165pm5.32i 575 . 2 ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
1675, 166bitri 276 1 (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2106  wne 3020  wral 3142  wrex 3143  Vcvv 3499  cdif 3936  cin 3938  wss 3939  {csn 4563   × cxp 5551  dom cdm 5553  ran crn 5554  cres 5555   Fn wfn 6346  wf 6347  cfv 6351  (class class class)co 7151  1st c1st 7681  2nd c2nd 7682  GrpOpcgr 28181  GIdcgi 28182  invcgn 28183   ExId cexid 34991  Magmacmagm 34995  MndOpcmndo 35013  RingOpscrngo 35041  DivRingOpscdrng 35095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-13 2385  ax-ext 2796  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-om 7572  df-1st 7683  df-2nd 7684  df-1o 8096  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-grpo 28185  df-gid 28186  df-ginv 28187  df-ablo 28237  df-ass 34990  df-exid 34992  df-mgmOLD 34996  df-sgrOLD 35008  df-mndo 35014  df-rngo 35042  df-drngo 35096
This theorem is referenced by:  isdrngo3  35106  divrngidl  35175
  Copyright terms: Public domain W3C validator