Metamath Proof Explorer


Theorem prdscmnd

Description: The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdscmnd.y Y = S 𝑠 R
prdscmnd.i φ I W
prdscmnd.s φ S V
prdscmnd.r φ R : I CMnd
Assertion prdscmnd φ Y CMnd

Proof

Step Hyp Ref Expression
1 prdscmnd.y Y = S 𝑠 R
2 prdscmnd.i φ I W
3 prdscmnd.s φ S V
4 prdscmnd.r φ R : I CMnd
5 eqidd φ Base Y = Base Y
6 eqidd φ + Y = + Y
7 cmnmnd a CMnd a Mnd
8 7 ssriv CMnd Mnd
9 fss R : I CMnd CMnd Mnd R : I Mnd
10 4 8 9 sylancl φ R : I Mnd
11 1 2 3 10 prdsmndd φ Y Mnd
12 4 3ad2ant1 φ a Base Y b Base Y R : I CMnd
13 12 ffvelrnda φ a Base Y b Base Y c I R c CMnd
14 eqid Base Y = Base Y
15 3 elexd φ S V
16 15 3ad2ant1 φ a Base Y b Base Y S V
17 16 adantr φ a Base Y b Base Y c I S V
18 2 elexd φ I V
19 18 3ad2ant1 φ a Base Y b Base Y I V
20 19 adantr φ a Base Y b Base Y c I I V
21 4 ffnd φ R Fn I
22 21 3ad2ant1 φ a Base Y b Base Y R Fn I
23 22 adantr φ a Base Y b Base Y c I R Fn I
24 simpl2 φ a Base Y b Base Y c I a Base Y
25 simpr φ a Base Y b Base Y c I c I
26 1 14 17 20 23 24 25 prdsbasprj φ a Base Y b Base Y c I a c Base R c
27 simpl3 φ a Base Y b Base Y c I b Base Y
28 1 14 17 20 23 27 25 prdsbasprj φ a Base Y b Base Y c I b c Base R c
29 eqid Base R c = Base R c
30 eqid + R c = + R c
31 29 30 cmncom R c CMnd a c Base R c b c Base R c a c + R c b c = b c + R c a c
32 13 26 28 31 syl3anc φ a Base Y b Base Y c I a c + R c b c = b c + R c a c
33 32 mpteq2dva φ a Base Y b Base Y c I a c + R c b c = c I b c + R c a c
34 simp2 φ a Base Y b Base Y a Base Y
35 simp3 φ a Base Y b Base Y b Base Y
36 eqid + Y = + Y
37 1 14 16 19 22 34 35 36 prdsplusgval φ a Base Y b Base Y a + Y b = c I a c + R c b c
38 1 14 16 19 22 35 34 36 prdsplusgval φ a Base Y b Base Y b + Y a = c I b c + R c a c
39 33 37 38 3eqtr4d φ a Base Y b Base Y a + Y b = b + Y a
40 5 6 11 39 iscmnd φ Y CMnd