Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isdrngo2 Structured version   Visualization version   Unicode version

Theorem isdrngo2 32261
Description: A division ring is a ring in which  1  =/=  0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.)
Hypotheses
Ref Expression
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
Ref Expression
isdrngo2  |-  ( R  e.  DivRingOps 
<->  ( R  e.  RingOps  /\  ( U  =/=  Z  /\  A. x  e.  ( X  \  { Z } ) E. y  e.  ( X  \  { Z } ) ( y H x )  =  U ) ) )
Distinct variable groups:    x, H, y    x, X, y    x, Z, y    x, R, y   
x, U, y
Allowed substitution hints:    G( x, y)

Proof of Theorem isdrngo2
Dummy variables  u  v  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isdivrng1.1 . . 3  |-  G  =  ( 1st `  R
)
2 isdivrng1.2 . . 3  |-  H  =  ( 2nd `  R
)
3 isdivrng1.3 . . 3  |-  Z  =  (GId `  G )
4 isdivrng1.4 . . 3  |-  X  =  ran  G
51, 2, 3, 4isdrngo1 32259 . 2  |-  ( R  e.  DivRingOps 
<->  ( R  e.  RingOps  /\  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  e. 
GrpOp ) )
6 isdivrng2.5 . . . . . . 7  |-  U  =  (GId `  H )
71, 2, 4, 3, 6dvrunz 26242 . . . . . 6  |-  ( R  e.  DivRingOps  ->  U  =/=  Z
)
85, 7sylbir 218 . . . . 5  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  U  =/= 
Z )
9 grporndm 26019 . . . . . . . . . . . 12  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  =  dom  dom  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
109adantl 473 . . . . . . . . . . 11  |-  ( ( 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 3549 . . . . . . . . . . . . . . . . 17  |-  ( X 
\  { Z }
)  C_  X
12 xpss12 4945 . . . . . . . . . . . . . . . . 17  |-  ( ( ( X  \  { Z } )  C_  X  /\  ( X  \  { Z } )  C_  X
)  ->  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) )  C_  ( X  X.  X ) )
1311, 11, 12mp2an 686 . . . . . . . . . . . . . . . 16  |-  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) )  C_  ( X  X.  X )
141, 2, 4rngosm 26190 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RingOps  ->  H : ( X  X.  X ) --> X )
15 fdm 5745 . . . . . . . . . . . . . . . . 17  |-  ( H : ( X  X.  X ) --> X  ->  dom  H  =  ( X  X.  X ) )
1614, 15syl 17 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RingOps  ->  dom  H  =  ( X  X.  X
) )
1713, 16syl5sseqr 3467 . . . . . . . . . . . . . . 15  |-  ( R  e.  RingOps  ->  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) )  C_  dom  H )
1817adantr 472 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) )  C_  dom  H )
19 ssdmres 5132 . . . . . . . . . . . . . 14  |-  ( ( ( X  \  { Z } )  X.  ( X  \  { Z }
) )  C_  dom  H  <->  dom  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
2018, 19sylib 201 . . . . . . . . . . . . 13  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  dom  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
2120dmeqd 5042 . . . . . . . . . . . 12  |-  ( ( 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 }
) ) )
22 dmxpid 5060 . . . . . . . . . . . 12  |-  dom  (
( X  \  { Z } )  X.  ( X  \  { Z }
) )  =  ( X  \  { Z } )
2321, 22syl6eq 2521 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  dom  dom  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( X  \  { Z } ) )
2410, 23eqtrd 2505 . . . . . . . . . 10  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ( X  \  { Z } ) )
2524eleq2d 2534 . . . . . . . . 9  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( x  e.  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  <-> 
x  e.  ( X 
\  { Z }
) ) )
2625biimpar 493 . . . . . . . 8  |-  ( ( ( R  e.  RingOps  /\  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  e. 
GrpOp )  /\  x  e.  ( X  \  { Z } ) )  ->  x  e.  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) )
27 eqid 2471 . . . . . . . . . . 11  |-  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
28 eqid 2471 . . . . . . . . . . 11  |-  ( inv `  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  ( inv `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
2927, 28grpoinvcl 26035 . . . . . . . . . 10  |-  ( ( ( 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 } ) ) ) )
3029adantll 728 . . . . . . . . 9  |-  ( ( ( 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 } ) ) ) )
31 eqid 2471 . . . . . . . . . . . 12  |-  (GId `  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  (GId `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
3227, 31, 28grpolinv 26037 . . . . . . . . . . 11  |-  ( ( ( 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 }
) ) ) ) )
3332adantll 728 . . . . . . . . . 10  |-  ( ( ( 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 }
) ) ) ) )
342rngomndo 26230 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  H  e. MndOp )
35 mndomgmid 26151 . . . . . . . . . . . . . 14  |-  ( H  e. MndOp  ->  H  e.  (
Magma  i^i  ExId  ) )
3634, 35syl 17 . . . . . . . . . . . . 13  |-  ( R  e.  RingOps  ->  H  e.  (
Magma  i^i  ExId  ) )
3736adantr 472 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  H  e.  ( Magma  i^i  ExId  )
)
3811, 4sseqtri 3450 . . . . . . . . . . . . . 14  |-  ( X 
\  { Z }
)  C_  ran  G
392, 1rngorn1eq 26229 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  ran  G  =  ran  H )
4038, 39syl5sseq 3466 . . . . . . . . . . . . 13  |-  ( R  e.  RingOps  ->  ( X  \  { Z } )  C_  ran  H )
4140adantr 472 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( X 
\  { Z }
)  C_  ran  H )
421rneqi 5067 . . . . . . . . . . . . . . . 16  |-  ran  G  =  ran  ( 1st `  R
)
434, 42eqtri 2493 . . . . . . . . . . . . . . 15  |-  X  =  ran  ( 1st `  R
)
4443, 2, 6rngo1cl 26238 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  U  e.  X
)
4544adantr 472 . . . . . . . . . . . . 13  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  U  e.  X )
46 eldifsn 4088 . . . . . . . . . . . . 13  |-  ( U  e.  ( X  \  { Z } )  <->  ( U  e.  X  /\  U  =/= 
Z ) )
4745, 8, 46sylanbrc 677 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  U  e.  ( X  \  { Z } ) )
48 grpomndo 26155 . . . . . . . . . . . . . 14  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e. MndOp )
49 mndoismgmOLD 26150 . . . . . . . . . . . . . 14  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. MndOp  ->  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  e. 
Magma )
5048, 49syl 17 . . . . . . . . . . . . 13  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e.  Magma )
5150adantl 473 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e.  Magma )
52 eqid 2471 . . . . . . . . . . . . 13  |-  ran  H  =  ran  H
53 eqid 2471 . . . . . . . . . . . . 13  |-  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  =  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
5452, 6, 53exidresid 32241 . . . . . . . . . . . 12  |-  ( ( ( 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 )
5537, 41, 47, 51, 54syl31anc 1295 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  (GId `  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  U )
5655adantr 472 . . . . . . . . . 10  |-  ( ( ( 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 )
5733, 56eqtrd 2505 . . . . . . . . 9  |-  ( ( ( 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 )
58 oveq1 6315 . . . . . . . . . . 11  |-  ( 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 ) )
5958eqeq1d 2473 . . . . . . . . . 10  |-  ( 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 ) )
6059rspcev 3136 . . . . . . . . 9  |-  ( ( ( ( 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 )
6130, 57, 60syl2anc 673 . . . . . . . 8  |-  ( ( ( 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 )
6226, 61syldan 478 . . . . . . 7  |-  ( ( ( 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 )
6324adantr 472 . . . . . . . . 9  |-  ( ( ( R  e.  RingOps  /\  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  e. 
GrpOp )  /\  x  e.  ( X  \  { Z } ) )  ->  ran  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( X  \  { Z } ) )
6463rexeqdv 2980 . . . . . . . 8  |-  ( ( ( 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 ) )
65 ovres 6455 . . . . . . . . . . . 12  |-  ( ( y  e.  ( X 
\  { Z }
)  /\  x  e.  ( X  \  { Z } ) )  -> 
( y ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) x )  =  ( y H x ) )
6665ancoms 460 . . . . . . . . . . 11  |-  ( ( x  e.  ( X 
\  { Z }
)  /\  y  e.  ( X  \  { Z } ) )  -> 
( y ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) x )  =  ( y H x ) )
6766eqeq1d 2473 . . . . . . . . . 10  |-  ( ( x  e.  ( X 
\  { Z }
)  /\  y  e.  ( X  \  { Z } ) )  -> 
( ( y ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) x )  =  U  <->  ( y H x )  =  U ) )
6867rexbidva 2889 . . . . . . . . 9  |-  ( 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 ) )
6968adantl 473 . . . . . . . 8  |-  ( ( ( 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 ) )
7064, 69bitrd 261 . . . . . . 7  |-  ( ( ( 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 ) )
7162, 70mpbid 215 . . . . . 6  |-  ( ( ( R  e.  RingOps  /\  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  e. 
GrpOp )  /\  x  e.  ( X  \  { Z } ) )  ->  E. y  e.  ( X  \  { Z }
) ( y H x )  =  U )
7271ralrimiva 2809 . . . . 5  |-  ( ( 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 )
738, 72jca 541 . . . 4  |-  ( ( 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 ) )
74 fvex 5889 . . . . . . . . 9  |-  ( 1st `  R )  e.  _V
751, 74eqeltri 2545 . . . . . . . 8  |-  G  e. 
_V
7675rnex 6746 . . . . . . 7  |-  ran  G  e.  _V
774, 76eqeltri 2545 . . . . . 6  |-  X  e. 
_V
78 difexg 4545 . . . . . 6  |-  ( X  e.  _V  ->  ( X  \  { Z }
)  e.  _V )
7977, 78mp1i 13 . . . . 5  |-  ( ( R  e.  RingOps  /\  ( U  =/=  Z  /\  A. x  e.  ( X  \  { Z } ) E. y  e.  ( X  \  { Z } ) ( y H x )  =  U ) )  -> 
( X  \  { Z } )  e.  _V )
80 ffn 5739 . . . . . . . . 9  |-  ( H : ( X  X.  X ) --> X  ->  H  Fn  ( X  X.  X ) )
8114, 80syl 17 . . . . . . . 8  |-  ( R  e.  RingOps  ->  H  Fn  ( X  X.  X ) )
8281adantr 472 . . . . . . 7  |-  ( ( R  e.  RingOps  /\  ( U  =/=  Z  /\  A. x  e.  ( X  \  { Z } ) E. y  e.  ( X  \  { Z } ) ( y H x )  =  U ) )  ->  H  Fn  ( X  X.  X ) )
83 fnssres 5699 . . . . . . 7  |-  ( ( 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 } ) ) )
8482, 13, 83sylancl 675 . . . . . 6  |-  ( ( 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 } ) ) )
85 ovres 6455 . . . . . . . . 9  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } ) )  -> 
( u ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) v )  =  ( u H v ) )
8685adantl 473 . . . . . . . 8  |-  ( ( ( 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 ) )
87 eldifi 3544 . . . . . . . . . . . 12  |-  ( u  e.  ( X  \  { Z } )  ->  u  e.  X )
88 eldifi 3544 . . . . . . . . . . . 12  |-  ( v  e.  ( X  \  { Z } )  -> 
v  e.  X )
8987, 88anim12i 576 . . . . . . . . . . 11  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } ) )  -> 
( u  e.  X  /\  v  e.  X
) )
901, 2, 4rngocl 26191 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  u  e.  X  /\  v  e.  X )  ->  (
u H v )  e.  X )
91903expb 1232 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  (
u  e.  X  /\  v  e.  X )
)  ->  ( u H v )  e.  X )
9289, 91sylan2 482 . . . . . . . . . 10  |-  ( ( R  e.  RingOps  /\  (
u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } ) ) )  ->  ( u H v )  e.  X
)
9392adantlr 729 . . . . . . . . 9  |-  ( ( ( 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
)
94 oveq2 6316 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
y H x )  =  ( y H u ) )
9594eqeq1d 2473 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
( y H x )  =  U  <->  ( y H u )  =  U ) )
9695rexbidv 2892 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  ( E. y  e.  ( X  \  { Z }
) ( y H x )  =  U  <->  E. y  e.  ( X  \  { Z }
) ( y H u )  =  U ) )
9796rspcv 3132 . . . . . . . . . . . . 13  |-  ( 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 ) )
9897imdistanri 705 . . . . . . . . . . . 12  |-  ( ( 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 } ) ) )
99 eldifsn 4088 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( X  \  { Z } )  <->  ( v  e.  X  /\  v  =/=  Z ) )
100 ssrexv 3480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  \  { Z } )  C_  X  ->  ( E. y  e.  ( X  \  { Z } ) ( y H u )  =  U  ->  E. y  e.  X  ( y H u )  =  U ) )
10111, 100ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U  ->  E. y  e.  X  ( y H u )  =  U )
1021, 2, 3, 4, 6zerdivemp1x 32258 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e.  RingOps  /\  u  e.  X  /\  E. y  e.  X  ( y H u )  =  U )  ->  (
v  e.  X  -> 
( ( u H v )  =  Z  ->  v  =  Z ) ) )
103101, 102syl3an3 1327 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  RingOps  /\  u  e.  X  /\  E. y  e.  ( X  \  { Z } ) ( y H u )  =  U )  ->  (
v  e.  X  -> 
( ( u H v )  =  Z  ->  v  =  Z ) ) )
10487, 103syl3an2 1326 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) )
1051043expb 1232 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
106105imp 436 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
107106necon3d 2664 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
108107impr 631 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
10999, 108sylan2b 483 . . . . . . . . . . . . . 14  |-  ( ( ( R  e.  RingOps  /\  ( u  e.  ( X  \  { Z }
)  /\  E. y  e.  ( X  \  { Z } ) ( y H u )  =  U ) )  /\  v  e.  ( X  \  { Z } ) )  ->  ( u H v )  =/= 
Z )
110109an32s 821 . . . . . . . . . . . . 13  |-  ( ( ( R  e.  RingOps  /\  v  e.  ( X  \  { Z } ) )  /\  ( u  e.  ( X  \  { Z } )  /\  E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U ) )  ->  (
u H v )  =/=  Z )
111110ancom2s 819 . . . . . . . . . . . 12  |-  ( ( ( R  e.  RingOps  /\  v  e.  ( X  \  { Z } ) )  /\  ( E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U  /\  u  e.  ( X  \  { Z } ) ) )  ->  ( u H v )  =/=  Z
)
11298, 111sylan2 482 . . . . . . . . . . 11  |-  ( ( ( 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
)
113112an42s 843 . . . . . . . . . 10  |-  ( ( ( 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
)
114113adantlrl 734 . . . . . . . . 9  |-  ( ( ( 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
)
115 eldifsn 4088 . . . . . . . . 9  |-  ( ( u H v )  e.  ( X  \  { Z } )  <->  ( (
u H v )  e.  X  /\  (
u H v )  =/=  Z ) )
11693, 114, 115sylanbrc 677 . . . . . . . 8  |-  ( ( ( 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 } ) )
11786, 116eqeltrd 2549 . . . . . . 7  |-  ( ( ( 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 }
) )
118117ralrimivva 2814 . . . . . 6  |-  ( ( 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 }
) )
119 ffnov 6419 . . . . . 6  |-  ( ( 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 }
) ) )
12084, 118, 119sylanbrc 677 . . . . 5  |-  ( ( 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 } ) )
1211163adantr3 1191 . . . . . . 7  |-  ( ( ( 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 } ) )
122 simpr3 1038 . . . . . . 7  |-  ( ( ( 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 } ) )
123121, 122ovresd 6456 . . . . . 6  |-  ( ( ( 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 ) )
124853adant3 1050 . . . . . . . 8  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } )  /\  w  e.  ( X  \  { Z } ) )  -> 
( u ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) v )  =  ( u H v ) )
125124adantl 473 . . . . . . 7  |-  ( ( ( 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 ) )
126125oveq1d 6323 . . . . . 6  |-  ( ( ( 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 ) )
127 ovres 6455 . . . . . . . . . 10  |-  ( ( v  e.  ( X 
\  { Z }
)  /\  w  e.  ( X  \  { Z } ) )  -> 
( v ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) w )  =  ( v H w ) )
1281273adant1 1048 . . . . . . . . 9  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } )  /\  w  e.  ( X  \  { Z } ) )  -> 
( v ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) w )  =  ( v H w ) )
129128adantl 473 . . . . . . . 8  |-  ( ( ( 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 ) )
130129oveq2d 6324 . . . . . . 7  |-  ( ( ( 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 ) ) )
131 simpr1 1036 . . . . . . . 8  |-  ( ( ( 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 } ) )
132 fovrn 6458 . . . . . . . . . 10  |-  ( ( ( 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 } ) )
1331323adant3r1 1240 . . . . . . . . 9  |-  ( ( ( 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 }
) )
134120, 133sylan 479 . . . . . . . 8  |-  ( ( ( 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 }
) )
135131, 134ovresd 6456 . . . . . . 7  |-  ( ( ( 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 ) ) )
136 eldifi 3544 . . . . . . . . . 10  |-  ( w  e.  ( X  \  { Z } )  ->  w  e.  X )
13787, 88, 1363anim123i 1215 . . . . . . . . 9  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } )  /\  w  e.  ( X  \  { Z } ) )  -> 
( u  e.  X  /\  v  e.  X  /\  w  e.  X
) )
1381, 2, 4rngoass 26196 . . . . . . . . 9  |-  ( ( R  e.  RingOps  /\  (
u  e.  X  /\  v  e.  X  /\  w  e.  X )
)  ->  ( (
u H v ) H w )  =  ( u H ( v H w ) ) )
139137, 138sylan2 482 . . . . . . . 8  |-  ( ( 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 ) ) )
140139adantlr 729 . . . . . . 7  |-  ( ( ( 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 ) ) )
141130, 135, 1403eqtr4d 2515 . . . . . 6  |-  ( ( ( 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 ) )
142123, 126, 1413eqtr4d 2515 . . . . 5  |-  ( ( ( 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 ) ) )
14344anim1i 578 . . . . . . 7  |-  ( ( R  e.  RingOps  /\  U  =/=  Z )  ->  ( U  e.  X  /\  U  =/=  Z ) )
144143, 46sylibr 217 . . . . . 6  |-  ( ( R  e.  RingOps  /\  U  =/=  Z )  ->  U  e.  ( X  \  { Z } ) )
145144adantrr 731 . . . . 5  |-  ( ( R  e.  RingOps  /\  ( U  =/=  Z  /\  A. x  e.  ( X  \  { Z } ) E. y  e.  ( X  \  { Z } ) ( y H x )  =  U ) )  ->  U  e.  ( X  \  { Z } ) )
146 ovres 6455 . . . . . . . 8  |-  ( ( U  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( U ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) u )  =  ( U H u ) )
147144, 146sylan 479 . . . . . . 7  |-  ( ( ( R  e.  RingOps  /\  U  =/=  Z )  /\  u  e.  ( X  \  { Z } ) )  ->  ( U
( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) u )  =  ( U H u ) )
1482, 43, 6rngolidm 26233 . . . . . . . . 9  |-  ( ( R  e.  RingOps  /\  u  e.  X )  ->  ( U H u )  =  u )
14987, 148sylan2 482 . . . . . . . 8  |-  ( ( R  e.  RingOps  /\  u  e.  ( X  \  { Z } ) )  -> 
( U H u )  =  u )
150149adantlr 729 . . . . . . 7  |-  ( ( ( R  e.  RingOps  /\  U  =/=  Z )  /\  u  e.  ( X  \  { Z } ) )  ->  ( U H u )  =  u )
151147, 150eqtrd 2505 . . . . . 6  |-  ( ( ( R  e.  RingOps  /\  U  =/=  Z )  /\  u  e.  ( X  \  { Z } ) )  ->  ( U
( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) u )  =  u )
152151adantlrr 735 . . . . 5  |-  ( ( ( 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 )
15396rspcva 3134 . . . . . . . . 9  |-  ( ( 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 )
154 oveq1 6315 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y H u )  =  ( z H u ) )
155154eqeq1d 2473 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( y H u )  =  U  <->  ( z H u )  =  U ) )
156155cbvrexv 3006 . . . . . . . . . 10  |-  ( E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U  <->  E. z  e.  ( X  \  { Z }
) ( z H u )  =  U )
157 ovres 6455 . . . . . . . . . . . . . 14  |-  ( ( z  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( z ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) u )  =  ( z H u ) )
158157eqeq1d 2473 . . . . . . . . . . . . 13  |-  ( ( z  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( ( z ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) u )  =  U  <->  ( z H u )  =  U ) )
159158ancoms 460 . . . . . . . . . . . 12  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  z  e.  ( X  \  { Z } ) )  -> 
( ( z ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) u )  =  U  <->  ( z H u )  =  U ) )
160159rexbidva 2889 . . . . . . . . . . 11  |-  ( 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 ) )
161160biimpar 493 . . . . . . . . . 10  |-  ( ( 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 )
162156, 161sylan2b 483 . . . . . . . . 9  |-  ( ( 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 )
163153, 162syldan 478 . . . . . . . 8  |-  ( ( 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 )
164163ancoms 460 . . . . . . 7  |-  ( ( 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 )
165164adantll 728 . . . . . 6  |-  ( ( ( 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 )
166165adantlrl 734 . . . . 5  |-  ( ( ( 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 )
16779, 120, 142, 145, 152, 166isgrpda 26106 . . . 4  |-  ( ( 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 )
16873, 167impbida 850 . . 3  |-  ( 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 ) ) )
169168pm5.32i 649 . 2  |-  ( ( 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 ) ) )
1705, 169bitri 257 1  |-  ( R  e.  DivRingOps 
<->  ( R  e.  RingOps  /\  ( U  =/=  Z  /\  A. x  e.  ( X  \  { Z } ) E. y  e.  ( X  \  { Z } ) ( y H x )  =  U ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031    \ cdif 3387    i^i cin 3389    C_ wss 3390   {csn 3959    X. cxp 4837   dom cdm 4839   ran crn 4840    |` cres 4841    Fn wfn 5584   -->wf 5585   ` cfv 5589  (class class class)co 6308   1stc1st 6810   2ndc2nd 6811   GrpOpcgr 25995  GIdcgi 25996   invcgn 25997    ExId cexid 26123   Magmacmagm 26127  MndOpcmndo 26146   RingOpscrngo 26184   DivRingOpscdrng 26214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-om 6712  df-1st 6812  df-2nd 6813  df-1o 7200  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-grpo 26000  df-gid 26001  df-ginv 26002  df-ablo 26091  df-ass 26122  df-exid 26124  df-mgmOLD 26128  df-sgrOLD 26140  df-mndo 26147  df-rngo 26185  df-drngo 26215
This theorem is referenced by:  isdrngo3  32262  divrngidl  32325
  Copyright terms: Public domain W3C validator