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

Theorem isdrngo2 30288
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 30286 . 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 25258 . . . . . 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 25035 . . . . . . . . . . . 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 3636 . . . . . . . . . . . . . . . . 17  |-  ( X 
\  { Z }
)  C_  X
12 xpss12 5114 . . . . . . . . . . . . . . . . 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 25206 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RingOps  ->  H : ( X  X.  X ) --> X )
15 fdm 5741 . . . . . . . . . . . . . . . . 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 3558 . . . . . . . . . . . . . . 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 5301 . . . . . . . . . . . . . 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 5211 . . . . . . . . . . . 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 5228 . . . . . . . . . . . 12  |-  dom  (
( X  \  { Z } )  X.  ( X  \  { Z }
) )  =  ( X  \  { Z } )
2321, 22syl6eq 2524 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  dom  dom  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( X  \  { Z } ) )
2410, 23eqtrd 2508 . . . . . . . . . 10  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ( X  \  { Z } ) )
2524eleq2d 2537 . . . . . . . . 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 2467 . . . . . . . . . . 11  |-  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
28 eqid 2467 . . . . . . . . . . 11  |-  ( inv `  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  ( inv `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
2927, 28grpoinvcl 25051 . . . . . . . . . 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 2467 . . . . . . . . . . . 12  |-  (GId `  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  (GId `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
3227, 31, 28grpolinv 25053 . . . . . . . . . . 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 25246 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  H  e. MndOp )
35 mndomgmid 25167 . . . . . . . . . . . . . 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 3541 . . . . . . . . . . . . . 14  |-  ( X 
\  { Z }
)  C_  ran  G
392, 1rngorn1eq 25245 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  ran  G  =  ran  H )
4038, 39syl5sseq 3557 . . . . . . . . . . . . 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 5235 . . . . . . . . . . . . . . . 16  |-  ran  G  =  ran  ( 1st `  R
)
434, 42eqtri 2496 . . . . . . . . . . . . . . 15  |-  X  =  ran  ( 1st `  R
)
4443, 2, 6rngo1cl 25254 . . . . . . . . . . . . . 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 4158 . . . . . . . . . . . . 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 25171 . . . . . . . . . . . . . 14  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e. MndOp )
49 mndoismgmOLD 25166 . . . . . . . . . . . . . 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 2467 . . . . . . . . . . . . 13  |-  ran  H  =  ran  H
53 eqid 2467 . . . . . . . . . . . . 13  |-  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  =  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
5452, 6, 53exidresid 30268 . . . . . . . . . . . 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 1231 . . . . . . . . . . 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 2508 . . . . . . . . 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 6302 . . . . . . . . . . 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 2469 . . . . . . . . . 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 3219 . . . . . . . . 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 3070 . . . . . . . 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 6437 . . . . . . . . . . . 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 2469 . . . . . . . . . 10  |-  ( ( x  e.  ( X 
\  { Z }
)  /\  y  e.  ( X  \  { Z } ) )  -> 
( ( y ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) x )  =  U  <->  ( y H x )  =  U ) )
6867rexbidva 2975 . . . . . . . . 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 2881 . . . . 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 5882 . . . . . . . . 9  |-  ( 1st `  R )  e.  _V
751, 74eqeltri 2551 . . . . . . . 8  |-  G  e. 
_V
7675rnex 6729 . . . . . . 7  |-  ran  G  e.  _V
774, 76eqeltri 2551 . . . . . 6  |-  X  e. 
_V
78 difexg 4601 . . . . . 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 5737 . . . . . . . . 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 5700 . . . . . . 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 6437 . . . . . . . . 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 3631 . . . . . . . . . . . 12  |-  ( u  e.  ( X  \  { Z } )  ->  u  e.  X )
88 eldifi 3631 . . . . . . . . . . . 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 25207 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  u  e.  X  /\  v  e.  X )  ->  (
u H v )  e.  X )
91903expb 1197 . . . . . . . . . . 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 6303 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
y H x )  =  ( y H u ) )
9594eqeq1d 2469 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
( y H x )  =  U  <->  ( y H u )  =  U ) )
9695rexbidv 2978 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  ( E. y  e.  ( X  \  { Z }
) ( y H x )  =  U  <->  E. y  e.  ( X  \  { Z }
) ( y H u )  =  U ) )
9796rspcv 3215 . . . . . . . . . . . . 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 4158 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( X  \  { Z } )  <->  ( v  e.  X  /\  v  =/=  Z ) )
100 ssrexv 3570 . . . . . . . . . . . . . . . . . . . . . 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 30285 . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . 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 1262 . . . . . . . . . . . . . . . . . . 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 1197 . . . . . . . . . . . . . . . . . 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 2691 . . . . . . . . . . . . . . . 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 4158 . . . . . . . . 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 2555 . . . . . . 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 2888 . . . . . 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 6401 . . . . . 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 1157 . . . . . . 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 1004 . . . . . . 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 6438 . . . . . 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 1016 . . . . . . . 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 6310 . . . . . 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 6437 . . . . . . . . . 10  |-  ( ( v  e.  ( X 
\  { Z }
)  /\  w  e.  ( X  \  { Z } ) )  -> 
( v ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) w )  =  ( v H w ) )
1281273adant1 1014 . . . . . . . . 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 6311 . . . . . . 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 1002 . . . . . . . 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 6440 . . . . . . . . . 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 1205 . . . . . . . . 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 6438 . . . . . . 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 3631 . . . . . . . . . 10  |-  ( w  e.  ( X  \  { Z } )  ->  w  e.  X )
13787, 88, 1363anim123i 1181 . . . . . . . . 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 25212 . . . . . . . . 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 2518 . . . . . 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 2518 . . . . 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 6437 . . . . . . . 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 25249 . . . . . . . . 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 2508 . . . . . 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 3217 . . . . . . . . 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 6302 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y H u )  =  ( z H u ) )
155154eqeq1d 2469 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( y H u )  =  U  <->  ( z H u )  =  U ) )
156155cbvrexv 3094 . . . . . . . . . 10  |-  ( E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U  <->  E. z  e.  ( X  \  { Z }
) ( z H u )  =  U )
157 ovres 6437 . . . . . . . . . . . . . 14  |-  ( ( z  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( z ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) u )  =  ( z H u ) )
158157eqeq1d 2469 . . . . . . . . . . . . 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 2975 . . . . . . . . . . 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 25122 . . . 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 973    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2817   E.wrex 2818   _Vcvv 3118    \ cdif 3478    i^i cin 3480    C_ wss 3481   {csn 4033    X. cxp 5003   dom cdm 5005   ran crn 5006    |` cres 5007    Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6295   1stc1st 6793   2ndc2nd 6794   GrpOpcgr 25011  GIdcgi 25012   invcgn 25013    ExId cexid 25139   Magmacmagm 25143  MndOpcmndo 25162   RingOpscrngo 25200   DivRingOpscdrng 25230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-om 6696  df-1st 6795  df-2nd 6796  df-1o 7142  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-grpo 25016  df-gid 25017  df-ginv 25018  df-ablo 25107  df-ass 25138  df-exid 25140  df-mgmOLD 25144  df-sgrOLD 25156  df-mndo 25163  df-rngo 25201  df-drngo 25231
This theorem is referenced by:  isdrngo3  30289  divrngidl  30352
  Copyright terms: Public domain W3C validator