ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  issrg Unicode version

Theorem issrg 13148
Description: The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.)
Hypotheses
Ref Expression
issrg.b  |-  B  =  ( Base `  R
)
issrg.g  |-  G  =  (mulGrp `  R )
issrg.p  |-  .+  =  ( +g  `  R )
issrg.t  |-  .x.  =  ( .r `  R )
issrg.0  |-  .0.  =  ( 0g `  R )
Assertion
Ref Expression
issrg  |-  ( R  e. SRing 
<->  ( R  e. CMnd  /\  G  e.  Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
Distinct variable groups:    x, y, z, 
.+    x,  .0. , y, z   
x,  .x. , y, z    x, B, y, z    x, R, y, z
Allowed substitution hints:    G( x, y, z)

Proof of Theorem issrg
Dummy variables  n  b  p  r  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2749 . 2  |-  ( R  e. SRing  ->  R  e.  _V )
2 simp1 997 . . 3  |-  ( ( R  e. CMnd  /\  G  e.  Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) )  ->  R  e. CMnd )
32elexd 2751 . 2  |-  ( ( R  e. CMnd  /\  G  e.  Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) )  ->  R  e.  _V )
4 issrg.g . . . . . . . 8  |-  G  =  (mulGrp `  R )
54eleq1i 2243 . . . . . . 7  |-  ( G  e.  Mnd  <->  (mulGrp `  R
)  e.  Mnd )
65bicomi 132 . . . . . 6  |-  ( (mulGrp `  R )  e.  Mnd  <->  G  e.  Mnd )
76a1i 9 . . . . 5  |-  ( R  e.  _V  ->  (
(mulGrp `  R )  e.  Mnd  <->  G  e.  Mnd ) )
8 issrg.b . . . . . . 7  |-  B  =  ( Base `  R
)
9 basfn 12520 . . . . . . . 8  |-  Base  Fn  _V
10 funfvex 5533 . . . . . . . . 9  |-  ( ( Fun  Base  /\  R  e. 
dom  Base )  ->  ( Base `  R )  e. 
_V )
1110funfni 5317 . . . . . . . 8  |-  ( (
Base  Fn  _V  /\  R  e.  _V )  ->  ( Base `  R )  e. 
_V )
129, 11mpan 424 . . . . . . 7  |-  ( R  e.  _V  ->  ( Base `  R )  e. 
_V )
138, 12eqeltrid 2264 . . . . . 6  |-  ( R  e.  _V  ->  B  e.  _V )
14 issrg.p . . . . . . . . 9  |-  .+  =  ( +g  `  R )
15 plusgslid 12571 . . . . . . . . . 10  |-  ( +g  = Slot  ( +g  `  ndx )  /\  ( +g  `  ndx )  e.  NN )
1615slotex 12489 . . . . . . . . 9  |-  ( R  e.  _V  ->  ( +g  `  R )  e. 
_V )
1714, 16eqeltrid 2264 . . . . . . . 8  |-  ( R  e.  _V  ->  .+  e.  _V )
1817adantr 276 . . . . . . 7  |-  ( ( R  e.  _V  /\  b  =  B )  ->  .+  e.  _V )
19 issrg.t . . . . . . . . . 10  |-  .x.  =  ( .r `  R )
20 mulrslid 12590 . . . . . . . . . . 11  |-  ( .r  = Slot  ( .r `  ndx )  /\  ( .r `  ndx )  e.  NN )
2120slotex 12489 . . . . . . . . . 10  |-  ( R  e.  _V  ->  ( .r `  R )  e. 
_V )
2219, 21eqeltrid 2264 . . . . . . . . 9  |-  ( R  e.  _V  ->  .x.  e.  _V )
2322ad2antrr 488 . . . . . . . 8  |-  ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  ->  .x.  e.  _V )
24 issrg.0 . . . . . . . . . . 11  |-  .0.  =  ( 0g `  R )
25 fn0g 12794 . . . . . . . . . . . 12  |-  0g  Fn  _V
26 funfvex 5533 . . . . . . . . . . . . 13  |-  ( ( Fun  0g  /\  R  e.  dom  0g )  -> 
( 0g `  R
)  e.  _V )
2726funfni 5317 . . . . . . . . . . . 12  |-  ( ( 0g  Fn  _V  /\  R  e.  _V )  ->  ( 0g `  R
)  e.  _V )
2825, 27mpan 424 . . . . . . . . . . 11  |-  ( R  e.  _V  ->  ( 0g `  R )  e. 
_V )
2924, 28eqeltrid 2264 . . . . . . . . . 10  |-  ( R  e.  _V  ->  .0.  e.  _V )
3029ad3antrrr 492 . . . . . . . . 9  |-  ( ( ( ( R  e. 
_V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  ->  .0.  e.  _V )
31 simp-4r 542 . . . . . . . . . 10  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  b  =  B )
32 simplr 528 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  t  =  .x.  )
33 eqidd 2178 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  x  =  x )
34 simpllr 534 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  p  =  .+  )
3534oveqd 5892 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
y p z )  =  ( y  .+  z ) )
3632, 33, 35oveq123d 5896 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
x t ( y p z ) )  =  ( x  .x.  ( y  .+  z
) ) )
3732oveqd 5892 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
x t y )  =  ( x  .x.  y ) )
3832oveqd 5892 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
x t z )  =  ( x  .x.  z ) )
3934, 37, 38oveq123d 5896 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( x t y ) p ( x t z ) )  =  ( ( x 
.x.  y )  .+  ( x  .x.  z ) ) )
4036, 39eqeq12d 2192 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  <->  ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) ) ) )
4134oveqd 5892 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
x p y )  =  ( x  .+  y ) )
42 eqidd 2178 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  z  =  z )
4332, 41, 42oveq123d 5896 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( x p y ) t z )  =  ( ( x 
.+  y )  .x.  z ) )
4432oveqd 5892 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
y t z )  =  ( y  .x.  z ) )
4534, 38, 44oveq123d 5896 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( x t z ) p ( y t z ) )  =  ( ( x 
.x.  z )  .+  ( y  .x.  z
) ) )
4643, 45eqeq12d 2192 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) )  <->  ( (
x  .+  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) ) )
4740, 46anbi12d 473 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  <->  ( ( x 
.x.  ( y  .+  z ) )  =  ( ( x  .x.  y )  .+  (
x  .x.  z )
)  /\  ( (
x  .+  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) ) ) )
4831, 47raleqbidv 2685 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  ( A. z  e.  b 
( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  <->  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) ) ) )
4931, 48raleqbidv 2685 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  ( A. y  e.  b  A. z  e.  b 
( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  <->  A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) ) ) )
50 simpr 110 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  n  =  .0.  )
5132, 50, 33oveq123d 5896 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
n t x )  =  (  .0.  .x.  x ) )
5251, 50eqeq12d 2192 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( n t x )  =  n  <->  (  .0.  .x.  x )  =  .0.  ) )
5332, 33, 50oveq123d 5896 . . . . . . . . . . . . 13  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
x t n )  =  ( x  .x.  .0.  ) )
5453, 50eqeq12d 2192 . . . . . . . . . . . 12  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( x t n )  =  n  <->  ( x  .x.  .0.  )  =  .0.  ) )
5552, 54anbi12d 473 . . . . . . . . . . 11  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( ( n t x )  =  n  /\  ( x t n )  =  n )  <->  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) )
5649, 55anbi12d 473 . . . . . . . . . 10  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  (
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  ( A. y  e.  B  A. z  e.  B  ( (
x  .x.  ( y  .+  z ) )  =  ( ( x  .x.  y )  .+  (
x  .x.  z )
)  /\  ( (
x  .+  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
5731, 56raleqbidv 2685 . . . . . . . . 9  |-  ( ( ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  /\  n  =  .0.  )  ->  ( A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
5830, 57sbcied 3000 . . . . . . . 8  |-  ( ( ( ( R  e. 
_V  /\  b  =  B )  /\  p  =  .+  )  /\  t  =  .x.  )  ->  ( [.  .0.  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
5923, 58sbcied 3000 . . . . . . 7  |-  ( ( ( R  e.  _V  /\  b  =  B )  /\  p  =  .+  )  ->  ( [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
6018, 59sbcied 3000 . . . . . 6  |-  ( ( R  e.  _V  /\  b  =  B )  ->  ( [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
6113, 60sbcied 3000 . . . . 5  |-  ( R  e.  _V  ->  ( [. B  /  b ]. [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
627, 61anbi12d 473 . . . 4  |-  ( R  e.  _V  ->  (
( (mulGrp `  R
)  e.  Mnd  /\  [. B  /  b ]. [. 
.+  /  p ]. [. 
.x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) )  <->  ( G  e.  Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) ) )
6362anbi2d 464 . . 3  |-  ( R  e.  _V  ->  (
( R  e. CMnd  /\  ( (mulGrp `  R )  e.  Mnd  /\  [. B  /  b ]. [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) )  <->  ( R  e. CMnd  /\  ( G  e. 
Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) ) ) )
64 fveq2 5516 . . . . . 6  |-  ( r  =  R  ->  (mulGrp `  r )  =  (mulGrp `  R ) )
6564eleq1d 2246 . . . . 5  |-  ( r  =  R  ->  (
(mulGrp `  r )  e.  Mnd  <->  (mulGrp `  R )  e.  Mnd ) )
66 fveq2 5516 . . . . . . 7  |-  ( r  =  R  ->  ( Base `  r )  =  ( Base `  R
) )
6766, 8eqtr4di 2228 . . . . . 6  |-  ( r  =  R  ->  ( Base `  r )  =  B )
68 fveq2 5516 . . . . . . . 8  |-  ( r  =  R  ->  ( +g  `  r )  =  ( +g  `  R
) )
6968, 14eqtr4di 2228 . . . . . . 7  |-  ( r  =  R  ->  ( +g  `  r )  = 
.+  )
70 fveq2 5516 . . . . . . . . 9  |-  ( r  =  R  ->  ( .r `  r )  =  ( .r `  R
) )
7170, 19eqtr4di 2228 . . . . . . . 8  |-  ( r  =  R  ->  ( .r `  r )  = 
.x.  )
72 fveq2 5516 . . . . . . . . . 10  |-  ( r  =  R  ->  ( 0g `  r )  =  ( 0g `  R
) )
7372, 24eqtr4di 2228 . . . . . . . . 9  |-  ( r  =  R  ->  ( 0g `  r )  =  .0.  )
7473sbceq1d 2968 . . . . . . . 8  |-  ( r  =  R  ->  ( [. ( 0g `  r
)  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) )
7571, 74sbceqbid 2970 . . . . . . 7  |-  ( r  =  R  ->  ( [. ( .r `  r
)  /  t ]. [. ( 0g `  r
)  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) )
7669, 75sbceqbid 2970 . . . . . 6  |-  ( r  =  R  ->  ( [. ( +g  `  r
)  /  p ]. [. ( .r `  r
)  /  t ]. [. ( 0g `  r
)  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) )
7767, 76sbceqbid 2970 . . . . 5  |-  ( r  =  R  ->  ( [. ( Base `  r
)  /  b ]. [. ( +g  `  r
)  /  p ]. [. ( .r `  r
)  /  t ]. [. ( 0g `  r
)  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) )  <->  [. B  /  b ]. [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) )
7865, 77anbi12d 473 . . . 4  |-  ( r  =  R  ->  (
( (mulGrp `  r
)  e.  Mnd  /\  [. ( Base `  r
)  /  b ]. [. ( +g  `  r
)  /  p ]. [. ( .r `  r
)  /  t ]. [. ( 0g `  r
)  /  n ]. A. x  e.  b 
( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) )  <->  ( (mulGrp `  R )  e.  Mnd  /\ 
[. B  /  b ]. [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) ) )
79 df-srg 13147 . . . 4  |- SRing  =  {
r  e. CMnd  |  (
(mulGrp `  r )  e.  Mnd  /\  [. ( Base `  r )  / 
b ]. [. ( +g  `  r )  /  p ]. [. ( .r `  r )  /  t ]. [. ( 0g `  r )  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) }
8078, 79elrab2 2897 . . 3  |-  ( R  e. SRing 
<->  ( R  e. CMnd  /\  ( (mulGrp `  R )  e.  Mnd  /\  [. B  /  b ]. [.  .+  /  p ]. [.  .x.  /  t ]. [.  .0.  /  n ]. A. x  e.  b  ( A. y  e.  b  A. z  e.  b  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) ) )
81 3anass 982 . . 3  |-  ( ( R  e. CMnd  /\  G  e.  Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) )  <->  ( R  e. CMnd  /\  ( G  e. 
Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) ) )
8263, 80, 813bitr4g 223 . 2  |-  ( R  e.  _V  ->  ( R  e. SRing  <->  ( R  e. CMnd  /\  G  e.  Mnd  /\ 
A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) ) )
831, 3, 82pm5.21nii 704 1  |-  ( R  e. SRing 
<->  ( R  e. CMnd  /\  G  e.  Mnd  /\  A. x  e.  B  ( A. y  e.  B  A. z  e.  B  ( ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  /\  ( ( x  .+  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )  /\  ( (  .0. 
.x.  x )  =  .0.  /\  ( x 
.x.  .0.  )  =  .0.  ) ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105    /\ w3a 978    = wceq 1353    e. wcel 2148   A.wral 2455   _Vcvv 2738   [.wsbc 2963    Fn wfn 5212   ` cfv 5217  (class class class)co 5875   Basecbs 12462   +g cplusg 12536   .rcmulr 12537   0gc0g 12705   Mndcmnd 12817  CMndccmn 13088  mulGrpcmgp 13130  SRingcsrg 13146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-sbc 2964  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-iota 5179  df-fun 5219  df-fn 5220  df-fv 5225  df-riota 5831  df-ov 5878  df-inn 8920  df-2 8978  df-3 8979  df-ndx 12465  df-slot 12466  df-base 12468  df-plusg 12549  df-mulr 12550  df-0g 12707  df-srg 13147
This theorem is referenced by:  srgcmn  13149  srgmgp  13151  srgdilem  13152  srgrz  13167  srglz  13168  ringsrg  13224
  Copyright terms: Public domain W3C validator