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

Theorem isdrngo2 30329
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 30327 . 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 25300 . . . . . 6  |-  ( R  e.  DivRingOps  ->  U  =/=  Z
)
85, 7sylbir 213 . . . . 5  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  U  =/= 
Z )
9 grporndm 25077 . . . . . . . . . . . 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 466 . . . . . . . . . . 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 3613 . . . . . . . . . . . . . . . . 17  |-  ( X 
\  { Z }
)  C_  X
12 xpss12 5094 . . . . . . . . . . . . . . . . 17  |-  ( ( ( X  \  { Z } )  C_  X  /\  ( X  \  { Z } )  C_  X
)  ->  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) )  C_  ( X  X.  X ) )
1311, 11, 12mp2an 672 . . . . . . . . . . . . . . . 16  |-  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) )  C_  ( X  X.  X )
141, 2, 4rngosm 25248 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RingOps  ->  H : ( X  X.  X ) --> X )
15 fdm 5721 . . . . . . . . . . . . . . . . 17  |-  ( H : ( X  X.  X ) --> X  ->  dom  H  =  ( X  X.  X ) )
1614, 15syl 16 . . . . . . . . . . . . . . . 16  |-  ( R  e.  RingOps  ->  dom  H  =  ( X  X.  X
) )
1713, 16syl5sseqr 3535 . . . . . . . . . . . . . . 15  |-  ( R  e.  RingOps  ->  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) )  C_  dom  H )
1817adantr 465 . . . . . . . . . . . . . 14  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) )  C_  dom  H )
19 ssdmres 5281 . . . . . . . . . . . . . 14  |-  ( ( ( X  \  { Z } )  X.  ( X  \  { Z }
) )  C_  dom  H  <->  dom  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
2018, 19sylib 196 . . . . . . . . . . . . 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 5191 . . . . . . . . . . . 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 5208 . . . . . . . . . . . 12  |-  dom  (
( X  \  { Z } )  X.  ( X  \  { Z }
) )  =  ( X  \  { Z } )
2321, 22syl6eq 2498 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  dom  dom  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( X  \  { Z } ) )
2410, 23eqtrd 2482 . . . . . . . . . 10  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ( X  \  { Z } ) )
2524eleq2d 2511 . . . . . . . . 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 485 . . . . . . . 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 2441 . . . . . . . . . . 11  |-  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
28 eqid 2441 . . . . . . . . . . 11  |-  ( inv `  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  ( inv `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
2927, 28grpoinvcl 25093 . . . . . . . . . 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 713 . . . . . . . . 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 2441 . . . . . . . . . . . 12  |-  (GId `  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  (GId `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
3227, 31, 28grpolinv 25095 . . . . . . . . . . 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 713 . . . . . . . . . 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 25288 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  H  e. MndOp )
35 mndomgmid 25209 . . . . . . . . . . . . . 14  |-  ( H  e. MndOp  ->  H  e.  (
Magma  i^i  ExId  ) )
3634, 35syl 16 . . . . . . . . . . . . 13  |-  ( R  e.  RingOps  ->  H  e.  (
Magma  i^i  ExId  ) )
3736adantr 465 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  H  e.  ( Magma  i^i  ExId  )
)
3811, 4sseqtri 3518 . . . . . . . . . . . . . 14  |-  ( X 
\  { Z }
)  C_  ran  G
392, 1rngorn1eq 25287 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  ran  G  =  ran  H )
4038, 39syl5sseq 3534 . . . . . . . . . . . . 13  |-  ( R  e.  RingOps  ->  ( X  \  { Z } )  C_  ran  H )
4140adantr 465 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( X 
\  { Z }
)  C_  ran  H )
421rneqi 5215 . . . . . . . . . . . . . . . 16  |-  ran  G  =  ran  ( 1st `  R
)
434, 42eqtri 2470 . . . . . . . . . . . . . . 15  |-  X  =  ran  ( 1st `  R
)
4443, 2, 6rngo1cl 25296 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  U  e.  X
)
4544adantr 465 . . . . . . . . . . . . 13  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  U  e.  X )
46 eldifsn 4136 . . . . . . . . . . . . 13  |-  ( U  e.  ( X  \  { Z } )  <->  ( U  e.  X  /\  U  =/= 
Z ) )
4745, 8, 46sylanbrc 664 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  U  e.  ( X  \  { Z } ) )
48 grpomndo 25213 . . . . . . . . . . . . . 14  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e. MndOp )
49 mndoismgmOLD 25208 . . . . . . . . . . . . . 14  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. MndOp  ->  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  e. 
Magma )
5048, 49syl 16 . . . . . . . . . . . . 13  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e.  Magma )
5150adantl 466 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e.  Magma )
52 eqid 2441 . . . . . . . . . . . . 13  |-  ran  H  =  ran  H
53 eqid 2441 . . . . . . . . . . . . 13  |-  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  =  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
5452, 6, 53exidresid 30309 . . . . . . . . . . . 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 1230 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  (GId `  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  U )
5655adantr 465 . . . . . . . . . 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 2482 . . . . . . . . 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 6284 . . . . . . . . . . 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 2443 . . . . . . . . . 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 3194 . . . . . . . . 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 661 . . . . . . . 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 470 . . . . . . 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 465 . . . . . . . . 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 3045 . . . . . . . 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 6423 . . . . . . . . . . . 12  |-  ( ( y  e.  ( X 
\  { Z }
)  /\  x  e.  ( X  \  { Z } ) )  -> 
( y ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) x )  =  ( y H x ) )
6665ancoms 453 . . . . . . . . . . 11  |-  ( ( x  e.  ( X 
\  { Z }
)  /\  y  e.  ( X  \  { Z } ) )  -> 
( y ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) x )  =  ( y H x ) )
6766eqeq1d 2443 . . . . . . . . . 10  |-  ( ( x  e.  ( X 
\  { Z }
)  /\  y  e.  ( X  \  { Z } ) )  -> 
( ( y ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) x )  =  U  <->  ( y H x )  =  U ) )
6867rexbidva 2949 . . . . . . . . 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 466 . . . . . . . 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 253 . . . . . . 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 210 . . . . . 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 2855 . . . . 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 532 . . . 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 5862 . . . . . . . . 9  |-  ( 1st `  R )  e.  _V
751, 74eqeltri 2525 . . . . . . . 8  |-  G  e. 
_V
7675rnex 6715 . . . . . . 7  |-  ran  G  e.  _V
774, 76eqeltri 2525 . . . . . 6  |-  X  e. 
_V
78 difexg 4581 . . . . . 6  |-  ( X  e.  _V  ->  ( X  \  { Z }
)  e.  _V )
7977, 78mp1i 12 . . . . 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 5717 . . . . . . . . 9  |-  ( H : ( X  X.  X ) --> X  ->  H  Fn  ( X  X.  X ) )
8114, 80syl 16 . . . . . . . 8  |-  ( R  e.  RingOps  ->  H  Fn  ( X  X.  X ) )
8281adantr 465 . . . . . . 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 5680 . . . . . . 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 662 . . . . . 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 6423 . . . . . . . . 9  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } ) )  -> 
( u ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) v )  =  ( u H v ) )
8685adantl 466 . . . . . . . 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 3608 . . . . . . . . . . . 12  |-  ( u  e.  ( X  \  { Z } )  ->  u  e.  X )
88 eldifi 3608 . . . . . . . . . . . 12  |-  ( v  e.  ( X  \  { Z } )  -> 
v  e.  X )
8987, 88anim12i 566 . . . . . . . . . . 11  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } ) )  -> 
( u  e.  X  /\  v  e.  X
) )
901, 2, 4rngocl 25249 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  u  e.  X  /\  v  e.  X )  ->  (
u H v )  e.  X )
91903expb 1196 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  (
u  e.  X  /\  v  e.  X )
)  ->  ( u H v )  e.  X )
9289, 91sylan2 474 . . . . . . . . . 10  |-  ( ( R  e.  RingOps  /\  (
u  e.  ( X 
\  { Z }
)  /\  v  e.  ( X  \  { Z } ) ) )  ->  ( u H v )  e.  X
)
9392adantlr 714 . . . . . . . . 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 6285 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
y H x )  =  ( y H u ) )
9594eqeq1d 2443 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
( y H x )  =  U  <->  ( y H u )  =  U ) )
9695rexbidv 2952 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  ( E. y  e.  ( X  \  { Z }
) ( y H x )  =  U  <->  E. y  e.  ( X  \  { Z }
) ( y H u )  =  U ) )
9796rspcv 3190 . . . . . . . . . . . . 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 691 . . . . . . . . . . . 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 4136 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( X  \  { Z } )  <->  ( v  e.  X  /\  v  =/=  Z ) )
100 ssrexv 3547 . . . . . . . . . . . . . . . . . . . . . 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 30326 . . . . . . . . . . . . . . . . . . . . 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 1262 . . . . . . . . . . . . . . . . . . . 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 1261 . . . . . . . . . . . . . . . . . . 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 1196 . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . 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 2665 . . . . . . . . . . . . . . . 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 619 . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . 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 800 . . . . . . . . . . . 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 474 . . . . . . . . . . 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 825 . . . . . . . . . 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 719 . . . . . . . . 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 4136 . . . . . . . . 9  |-  ( ( u H v )  e.  ( X  \  { Z } )  <->  ( (
u H v )  e.  X  /\  (
u H v )  =/=  Z ) )
11693, 114, 115sylanbrc 664 . . . . . . . 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 2529 . . . . . . 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 2862 . . . . . 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 6387 . . . . . 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 664 . . . . 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 1156 . . . . . . 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 1003 . . . . . . 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 6424 . . . . . 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 1015 . . . . . . . 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 466 . . . . . . 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 6292 . . . . . 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 6423 . . . . . . . . . 10  |-  ( ( v  e.  ( X 
\  { Z }
)  /\  w  e.  ( X  \  { Z } ) )  -> 
( v ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) w )  =  ( v H w ) )
1281273adant1 1013 . . . . . . . . 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 466 . . . . . . . 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 6293 . . . . . . 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 1001 . . . . . . . 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 6426 . . . . . . . . . 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 1204 . . . . . . . . 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 471 . . . . . . . 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 6424 . . . . . . 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 3608 . . . . . . . . . 10  |-  ( w  e.  ( X  \  { Z } )  ->  w  e.  X )
13787, 88, 1363anim123i 1180 . . . . . . . . 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 25254 . . . . . . . . 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 474 . . . . . . . 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 714 . . . . . . 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 2492 . . . . . 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 2492 . . . . 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 568 . . . . . . 7  |-  ( ( R  e.  RingOps  /\  U  =/=  Z )  ->  ( U  e.  X  /\  U  =/=  Z ) )
144143, 46sylibr 212 . . . . . 6  |-  ( ( R  e.  RingOps  /\  U  =/=  Z )  ->  U  e.  ( X  \  { Z } ) )
145144adantrr 716 . . . . 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 6423 . . . . . . . 8  |-  ( ( U  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( U ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) u )  =  ( U H u ) )
147144, 146sylan 471 . . . . . . 7  |-  ( ( ( R  e.  RingOps  /\  U  =/=  Z )  /\  u  e.  ( X  \  { Z } ) )  ->  ( U
( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) u )  =  ( U H u ) )
1482, 43, 6rngolidm 25291 . . . . . . . . 9  |-  ( ( R  e.  RingOps  /\  u  e.  X )  ->  ( U H u )  =  u )
14987, 148sylan2 474 . . . . . . . 8  |-  ( ( R  e.  RingOps  /\  u  e.  ( X  \  { Z } ) )  -> 
( U H u )  =  u )
150149adantlr 714 . . . . . . 7  |-  ( ( ( R  e.  RingOps  /\  U  =/=  Z )  /\  u  e.  ( X  \  { Z } ) )  ->  ( U H u )  =  u )
151147, 150eqtrd 2482 . . . . . 6  |-  ( ( ( R  e.  RingOps  /\  U  =/=  Z )  /\  u  e.  ( X  \  { Z } ) )  ->  ( U
( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) u )  =  u )
152151adantlrr 720 . . . . 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 3192 . . . . . . . . 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 6284 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y H u )  =  ( z H u ) )
155154eqeq1d 2443 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( y H u )  =  U  <->  ( z H u )  =  U ) )
156155cbvrexv 3069 . . . . . . . . . 10  |-  ( E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U  <->  E. z  e.  ( X  \  { Z }
) ( z H u )  =  U )
157 ovres 6423 . . . . . . . . . . . . . 14  |-  ( ( z  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( z ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) u )  =  ( z H u ) )
158157eqeq1d 2443 . . . . . . . . . . . . 13  |-  ( ( z  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( ( z ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) u )  =  U  <->  ( z H u )  =  U ) )
159158ancoms 453 . . . . . . . . . . . 12  |-  ( ( u  e.  ( X 
\  { Z }
)  /\  z  e.  ( X  \  { Z } ) )  -> 
( ( z ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) u )  =  U  <->  ( z H u )  =  U ) )
160159rexbidva 2949 . . . . . . . . . . 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 485 . . . . . . . . . 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 475 . . . . . . . . 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 470 . . . . . . . 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 453 . . . . . . 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 713 . . . . . 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 719 . . . . 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 25164 . . . 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 830 . . 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 637 . 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 249 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 184    /\ wa 369    /\ w3a 972    = wceq 1381    e. wcel 1802    =/= wne 2636   A.wral 2791   E.wrex 2792   _Vcvv 3093    \ cdif 3455    i^i cin 3457    C_ wss 3458   {csn 4010    X. cxp 4983   dom cdm 4985   ran crn 4986    |` cres 4987    Fn wfn 5569   -->wf 5570   ` cfv 5574  (class class class)co 6277   1stc1st 6779   2ndc2nd 6780   GrpOpcgr 25053  GIdcgi 25054   invcgn 25055    ExId cexid 25181   Magmacmagm 25185  MndOpcmndo 25204   RingOpscrngo 25242   DivRingOpscdrng 25272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-om 6682  df-1st 6781  df-2nd 6782  df-1o 7128  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-grpo 25058  df-gid 25059  df-ginv 25060  df-ablo 25149  df-ass 25180  df-exid 25182  df-mgmOLD 25186  df-sgrOLD 25198  df-mndo 25205  df-rngo 25243  df-drngo 25273
This theorem is referenced by:  isdrngo3  30330  divrngidl  30393
  Copyright terms: Public domain W3C validator