Metamath Proof Explorer


Theorem mnringmulrd

Description: The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses mnringmulrd.1 No typesetting found for |- F = ( R MndRing M ) with typecode |-
mnringmulrd.2 B = Base F
mnringmulrd.3 · ˙ = R
mnringmulrd.4 0 ˙ = 0 R
mnringmulrd.5 A = Base M
mnringmulrd.6 + ˙ = + M
mnringmulrd.7 φ R U
mnringmulrd.8 φ M W
Assertion mnringmulrd φ x B , y B F a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = F

Proof

Step Hyp Ref Expression
1 mnringmulrd.1 Could not format F = ( R MndRing M ) : No typesetting found for |- F = ( R MndRing M ) with typecode |-
2 mnringmulrd.2 B = Base F
3 mnringmulrd.3 · ˙ = R
4 mnringmulrd.4 0 ˙ = 0 R
5 mnringmulrd.5 A = Base M
6 mnringmulrd.6 + ˙ = + M
7 mnringmulrd.7 φ R U
8 mnringmulrd.8 φ M W
9 eqid R freeLMod A = R freeLMod A
10 1 2 5 9 7 8 mnringbaserd φ B = Base R freeLMod A
11 5 fvexi A V
12 11 11 mpoex a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ V
13 12 a1i φ a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ V
14 1 ovexi F V
15 14 a1i φ F V
16 ovex R freeLMod A V
17 16 a1i φ R freeLMod A V
18 2 10 eqtr3id φ Base F = Base R freeLMod A
19 1 5 9 7 8 mnringaddgd φ + R freeLMod A = + F
20 19 eqcomd φ + F = + R freeLMod A
21 13 15 17 18 20 gsumpropd φ F a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙
22 10 10 21 mpoeq123dv φ x B , y B F a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙
23 fvex Base R freeLMod A V
24 23 23 mpoex x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ V
25 mulrid 𝑟 = Slot ndx
26 25 setsid R freeLMod A V x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ V x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = R freeLMod A sSet ndx x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙
27 16 24 26 mp2an x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = R freeLMod A sSet ndx x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙
28 eqid Base R freeLMod A = Base R freeLMod A
29 1 3 4 5 6 9 28 7 8 mnringvald φ F = R freeLMod A sSet ndx x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙
30 29 fveq2d φ F = R freeLMod A sSet ndx x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙
31 27 30 eqtr4id φ x Base R freeLMod A , y Base R freeLMod A R freeLMod A a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = F
32 22 31 eqtrd φ x B , y B F a A , b A i A if i = a + ˙ b x a · ˙ y b 0 ˙ = F