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 ⊢ G = 1 st ⁡ R
isdivrng1.2 ⊢ H = 2 nd ⁡ R
isdivrng1.3 ⊢ Z = GId ⁡ G
isdivrng1.4 ⊢ X = ran ⁡ G
isdivrng2.5 ⊢ U = GId ⁡ H
Assertion isdrngo2 ⊢ R ∈ DivRingOps ↔ R ∈ RingOps ∧ U ≠ Z ∧ ∀ x ∈ X ∖ Z ∃ y ∈ X ∖ Z y H x = U

Proof

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