Metamath Proof Explorer

Theorem isdrngo2

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

Ref Expression
Hypotheses isdivrng1.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
isdivrng1.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
isdivrng1.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
isdivrng1.4 ⊢ 𝑋 = ran 𝐺
isdivrng2.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion isdrngo2 ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )

Proof

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