Metamath Proof Explorer

Theorem issrg

Description: The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018)

Ref Expression
Hypotheses 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 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. ) ) ) )

Proof

Step Hyp Ref Expression
1 issrg.b 
 |-  B = ( Base ` R )
2 issrg.g 
 |-  G = ( mulGrp ` R )
3 issrg.p 
 |-  .+ = ( +g ` R )
4 issrg.t 
 |-  .x. = ( .r ` R )
5 issrg.0 
 |-  .0. = ( 0g ` R )
6 2 eleq1i 
 |-  ( G e. Mnd <-> ( mulGrp ` R ) e. Mnd )
7 6 bicomi 
 |-  ( ( mulGrp ` R ) e. Mnd <-> G e. Mnd )
8 1 fvexi 
 |-  B e. _V
9 3 fvexi 
 |-  .+ e. _V
10 4 fvexi 
 |-  .x. e. _V
11 10 a1i 
 |-  ( ( b = B /\ p = .+ ) -> .x. e. _V )
12 5 fvexi 
 |-  .0. e. _V
13 12 a1i 
 |-  ( ( ( b = B /\ p = .+ ) /\ t = .x. ) -> .0. e. _V )
14 simplll 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> b = B )
15 simplr 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> t = .x. )
16 eqidd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> x = x )
17 simpllr 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> p = .+ )
18 17 oveqd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( y p z ) = ( y .+ z ) )
19 15 16 18 oveq123d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( x t ( y p z ) ) = ( x .x. ( y .+ z ) ) )
20 15 oveqd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( x t y ) = ( x .x. y ) )
21 15 oveqd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( x t z ) = ( x .x. z ) )
22 17 20 21 oveq123d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( ( x t y ) p ( x t z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
23 19 22 eqeq12d 
 |-  ( ( ( ( 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 ) ) ) )
24 17 oveqd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( x p y ) = ( x .+ y ) )
25 eqidd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> z = z )
26 15 24 25 oveq123d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( ( x p y ) t z ) = ( ( x .+ y ) .x. z ) )
27 15 oveqd 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( y t z ) = ( y .x. z ) )
28 17 21 27 oveq123d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( ( x t z ) p ( y t z ) ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
29 26 28 eqeq12d 
 |-  ( ( ( ( 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 ) ) ) )
30 23 29 anbi12d 
 |-  ( ( ( ( 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 ) ) ) ) )
31 14 30 raleqbidv 
 |-  ( ( ( ( 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 ) ) ) ) )
32 14 31 raleqbidv 
 |-  ( ( ( ( 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 ) ) ) ) )
33 simpr 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> n = .0. )
34 15 33 16 oveq123d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( n t x ) = ( .0. .x. x ) )
35 34 33 eqeq12d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( ( n t x ) = n <-> ( .0. .x. x ) = .0. ) )
36 15 16 33 oveq123d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( x t n ) = ( x .x. .0. ) )
37 36 33 eqeq12d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( ( x t n ) = n <-> ( x .x. .0. ) = .0. ) )
38 35 37 anbi12d 
 |-  ( ( ( ( b = B /\ p = .+ ) /\ t = .x. ) /\ n = .0. ) -> ( ( ( n t x ) = n /\ ( x t n ) = n ) <-> ( ( .0. .x. x ) = .0. /\ ( x .x. .0. ) = .0. ) ) )
39 32 38 anbi12d 
 |-  ( ( ( ( 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. ) ) ) )
40 14 39 raleqbidv 
 |-  ( ( ( ( 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. ) ) ) )
41 13 40 sbcied 
 |-  ( ( ( 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. ) ) ) )
42 11 41 sbcied 
 |-  ( ( 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. ) ) ) )
43 8 9 42 sbc2ie 
 |-  ( [. 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. ) ) )
44 7 43 anbi12i 
 |-  ( ( ( 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. ) ) ) )
45 44 anbi2i 
 |-  ( ( 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. ) ) ) ) )
46 fveq2 
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
47 46 eleq1d 
 |-  ( r = R -> ( ( mulGrp ` r ) e. Mnd <-> ( mulGrp ` R ) e. Mnd ) )
48 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
49 48 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
50 fveq2 
 |-  ( r = R -> ( +g ` r ) = ( +g ` R ) )
51 50 3 eqtr4di 
 |-  ( r = R -> ( +g ` r ) = .+ )
52 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
53 52 4 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
54 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
55 54 5 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
56 55 sbceq1d 
 |-  ( 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 ) ) ) )
57 53 56 sbceqbid 
 |-  ( 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 ) ) ) )
58 51 57 sbceqbid 
 |-  ( 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 ) ) ) )
59 49 58 sbceqbid 
 |-  ( 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 ) ) ) )
60 47 59 anbi12d 
 |-  ( 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 ) ) ) ) )
61 df-srg 
 |-  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 ) ) ) }
62 60 61 elrab2 
 |-  ( 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 ) ) ) ) )
63 3anass 
 |-  ( ( 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. ) ) ) ) )
64 45 62 63 3bitr4i 
 |-  ( 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. ) ) ) )