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 + ˙ = + R
issrg.t · ˙ = R
issrg.0 0 ˙ = 0 R
Assertion issrg R SRing R CMnd G Mnd x B y B z B x · ˙ y + ˙ z = x · ˙ y + ˙ x · ˙ z x + ˙ y · ˙ z = x · ˙ z + ˙ y · ˙ z 0 ˙ · ˙ x = 0 ˙ x · ˙ 0 ˙ = 0 ˙

Proof

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