# 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 } ) ) ) )
|-  ( ( 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 )
|-  ( ( 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 } ) ) ) )
|-  ( ( ( 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 } ) ) ) ) )
|-  ( ( ( 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 ) )
|-  ( ( 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 )
|-  ( ( 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 )
|-  ( ( 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 )
|-  ( ( 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 )
|-  ( ( ( 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 )
|-  ( ( ( 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 ) )
|-  ( ( ( 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 ) )
|-  ( ( 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 ) )
|-  ( ( ( 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 )
|-  ( ( ( 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 )
|-  ( ( ( 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 } ) )
|-  ( ( ( 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 ) )
|-  ( ( u e. ( X \ { Z } ) /\ v e. ( X \ { Z } ) /\ w e. ( X \ { Z } ) ) -> ( u ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) v ) = ( u H v ) )
|-  ( ( ( 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 ) )
|-  ( ( u e. ( X \ { Z } ) /\ v e. ( X \ { Z } ) /\ w e. ( X \ { Z } ) ) -> ( v ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) w ) = ( v H w ) )
|-  ( ( ( 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 } ) )
|-  ( ( ( 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 ) ) )
|-  ( ( ( 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 } ) )
|-  ( ( 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 )
|-  ( ( ( 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 )
|-  ( ( ( 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 )