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

Theorem isdrngo2 28717
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 28715 . 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 23871 . . . . . 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 23648 . . . . . . . . . . . 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 3478 . . . . . . . . . . . . . . . . 17  |-  ( X 
\  { Z }
)  C_  X
12 xpss12 4940 . . . . . . . . . . . . . . . . 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 23819 . . . . . . . . . . . . . . . . 17  |-  ( R  e.  RingOps  ->  H : ( X  X.  X ) --> X )
15 fdm 5558 . . . . . . . . . . . . . . . . 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 3400 . . . . . . . . . . . . . . 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 5127 . . . . . . . . . . . . . 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 5037 . . . . . . . . . . . 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 5054 . . . . . . . . . . . 12  |-  dom  (
( X  \  { Z } )  X.  ( X  \  { Z }
) )  =  ( X  \  { Z } )
2321, 22syl6eq 2486 . . . . . . . . . . 11  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  dom  dom  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) )  =  ( X  \  { Z } ) )
2410, 23eqtrd 2470 . . . . . . . . . 10  |-  ( ( R  e.  RingOps  /\  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp )  ->  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ( X  \  { Z } ) )
2524eleq2d 2505 . . . . . . . . 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 2438 . . . . . . . . . . 11  |-  ran  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) )  =  ran  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
28 eqid 2438 . . . . . . . . . . 11  |-  ( inv `  ( H  |`  (
( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  ( inv `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
2927, 28grpoinvcl 23664 . . . . . . . . . 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 2438 . . . . . . . . . . . 12  |-  (GId `  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z }
) ) ) )  =  (GId `  ( H  |`  ( ( X 
\  { Z }
)  X.  ( X 
\  { Z }
) ) ) )
3227, 31, 28grpolinv 23666 . . . . . . . . . . 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 23859 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  H  e. MndOp )
35 mndomgmid 23780 . . . . . . . . . . . . . 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 3383 . . . . . . . . . . . . . 14  |-  ( X 
\  { Z }
)  C_  ran  G
392, 1rngorn1eq 23858 . . . . . . . . . . . . . 14  |-  ( R  e.  RingOps  ->  ran  G  =  ran  H )
4038, 39syl5sseq 3399 . . . . . . . . . . . . 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 5061 . . . . . . . . . . . . . . . 16  |-  ran  G  =  ran  ( 1st `  R
)
434, 42eqtri 2458 . . . . . . . . . . . . . . 15  |-  X  =  ran  ( 1st `  R
)
4443, 2, 6rngo1cl 23867 . . . . . . . . . . . . . 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 3995 . . . . . . . . . . . . 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 23784 . . . . . . . . . . . . . 14  |-  ( ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) )  e. 
GrpOp  ->  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  e. MndOp )
49 mndoismgm 23779 . . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . 13  |-  ran  H  =  ran  H
53 eqid 2438 . . . . . . . . . . . . 13  |-  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )  =  ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) )
5452, 6, 53exidresid 28697 . . . . . . . . . . . 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 1221 . . . . . . . . . . 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 2470 . . . . . . . . 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 6093 . . . . . . . . . . 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 2446 . . . . . . . . . 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 3068 . . . . . . . . 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 2919 . . . . . . . 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 6225 . . . . . . . . . . . 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 2446 . . . . . . . . . 10  |-  ( ( x  e.  ( X 
\  { Z }
)  /\  y  e.  ( X  \  { Z } ) )  -> 
( ( y ( H  |`  ( ( X  \  { Z }
)  X.  ( X 
\  { Z }
) ) ) x )  =  U  <->  ( y H x )  =  U ) )
6867rexbidva 2727 . . . . . . . . 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 2794 . . . . 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 5696 . . . . . . . . 9  |-  ( 1st `  R )  e.  _V
751, 74eqeltri 2508 . . . . . . . 8  |-  G  e. 
_V
7675rnex 6507 . . . . . . 7  |-  ran  G  e.  _V
774, 76eqeltri 2508 . . . . . 6  |-  X  e. 
_V
78 difexg 4435 . . . . . 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 5554 . . . . . . . . 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 5519 . . . . . . 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 6225 . . . . . . . . 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 3473 . . . . . . . . . . . 12  |-  ( u  e.  ( X  \  { Z } )  ->  u  e.  X )
88 eldifi 3473 . . . . . . . . . . . 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 23820 . . . . . . . . . . . 12  |-  ( ( R  e.  RingOps  /\  u  e.  X  /\  v  e.  X )  ->  (
u H v )  e.  X )
91903expb 1188 . . . . . . . . . . 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 6094 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
y H x )  =  ( y H u ) )
9594eqeq1d 2446 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  (
( y H x )  =  U  <->  ( y H u )  =  U ) )
9695rexbidv 2731 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  ( E. y  e.  ( X  \  { Z }
) ( y H x )  =  U  <->  E. y  e.  ( X  \  { Z }
) ( y H u )  =  U ) )
9796rspcv 3064 . . . . . . . . . . . . 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 3995 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( X  \  { Z } )  <->  ( v  e.  X  /\  v  =/=  Z ) )
100 ssrexv 3412 . . . . . . . . . . . . . . . . . . . . . 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 28714 . . . . . . . . . . . . . . . . . . . . 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 1253 . . . . . . . . . . . . . . . . . . . 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 1252 . . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . . 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 2641 . . . . . . . . . . . . . . . 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 823 . . . . . . . . . 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 3995 . . . . . . . . 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 2512 . . . . . . 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 2803 . . . . . 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 6189 . . . . . 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 1149 . . . . . . 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 996 . . . . . . 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 6226 . . . . . 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 1008 . . . . . . . 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 6101 . . . . . 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 6225 . . . . . . . . . 10  |-  ( ( v  e.  ( X 
\  { Z }
)  /\  w  e.  ( X  \  { Z } ) )  -> 
( v ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) w )  =  ( v H w ) )
1281273adant1 1006 . . . . . . . . 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 6102 . . . . . . 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 994 . . . . . . . 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 6228 . . . . . . . . . 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 1196 . . . . . . . . 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 6226 . . . . . . 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 3473 . . . . . . . . . 10  |-  ( w  e.  ( X  \  { Z } )  ->  w  e.  X )
13787, 88, 1363anim123i 1173 . . . . . . . . 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 23825 . . . . . . . . 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 2480 . . . . . 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 2480 . . . . 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 6225 . . . . . . . 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 23862 . . . . . . . . 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 2470 . . . . . 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 3066 . . . . . . . . 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 6093 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y H u )  =  ( z H u ) )
155154eqeq1d 2446 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( y H u )  =  U  <->  ( z H u )  =  U ) )
156155cbvrexv 2943 . . . . . . . . . 10  |-  ( E. y  e.  ( X 
\  { Z }
) ( y H u )  =  U  <->  E. z  e.  ( X  \  { Z }
) ( z H u )  =  U )
157 ovres 6225 . . . . . . . . . . . . . 14  |-  ( ( z  e.  ( X 
\  { Z }
)  /\  u  e.  ( X  \  { Z } ) )  -> 
( z ( H  |`  ( ( X  \  { Z } )  X.  ( X  \  { Z } ) ) ) u )  =  ( z H u ) )
158157eqeq1d 2446 . . . . . . . . . . . . 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 2727 . . . . . . . . . . 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 23735 . . . 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 828 . . 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 965    = wceq 1369    e. wcel 1756    =/= wne 2601   A.wral 2710   E.wrex 2711   _Vcvv 2967    \ cdif 3320    i^i cin 3322    C_ wss 3323   {csn 3872    X. cxp 4833   dom cdm 4835   ran crn 4836    |` cres 4837    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6086   1stc1st 6570   2ndc2nd 6571   GrpOpcgr 23624  GIdcgi 23625   invcgn 23626    ExId cexid 23752   Magmacmagm 23756  MndOpcmndo 23775   RingOpscrngo 23813   DivRingOpscdrng 23843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-om 6472  df-1st 6572  df-2nd 6573  df-1o 6912  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-grpo 23629  df-gid 23630  df-ginv 23631  df-ablo 23720  df-ass 23751  df-exid 23753  df-mgm 23757  df-sgr 23769  df-mndo 23776  df-rngo 23814  df-drngo 23844
This theorem is referenced by:  isdrngo3  28718  divrngidl  28781
  Copyright terms: Public domain W3C validator