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 = ( 1st ` R )
isdivrng1.2 
|- H = ( 2nd ` R )
isdivrng1.3 
|- Z = ( GId ` G )
isdivrng1.4 
|- X = ran G
isdivrng2.5 
|- U = ( GId ` H )
Assertion isdrngo2 
|- ( R e. DivRingOps <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = U ) ) )

Proof

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