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 ∧ ( 𝑈𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )