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	$⊢ φ \to I \in W$
	prdscmnd.s	$⊢ φ \to S \in V$
	prdscmnd.r	$⊢ φ \to R : I ⟶ CMnd$
Assertion	prdscmnd	$⊢ φ \to Y \in CMnd$

Proof

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

Metamath Proof Explorer

Theorem prdscmnd

Proof