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	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
	prdscmnd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdscmnd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdscmnd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ CMnd )
Assertion	prdscmnd	⊢ ( 𝜑 → 𝑌 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		prdscmnd.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
2		prdscmnd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3		prdscmnd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdscmnd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ CMnd )
5		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
6		eqidd	⊢ ( 𝜑 → ( +_g ‘ 𝑌 ) = ( +_g ‘ 𝑌 ) )
7		cmnmnd	⊢ ( 𝑎 ∈ CMnd → 𝑎 ∈ Mnd )
8	7	ssriv	⊢ CMnd ⊆ Mnd
9		fss	⊢ ( ( 𝑅 : 𝐼 ⟶ CMnd ∧ CMnd ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd )
10	4 8 9	sylancl	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
11	1 2 3 10	prdsmndd	⊢ ( 𝜑 → 𝑌 ∈ Mnd )
12	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 : 𝐼 ⟶ CMnd )
13	12	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑐 ) ∈ CMnd )
14		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
15	3	elexd	⊢ ( 𝜑 → 𝑆 ∈ V )
16	15	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → 𝑆 ∈ V )
17	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → 𝑆 ∈ V )
18	2	elexd	⊢ ( 𝜑 → 𝐼 ∈ V )
19	18	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → 𝐼 ∈ V )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → 𝐼 ∈ V )
21	4	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
22	21	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 Fn 𝐼 )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
24		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
25		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → 𝑐 ∈ 𝐼 )
26	1 14 17 20 23 24 25	prdsbasprj	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑐 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑐 ) ) )
27		simpl3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
28	1 14 17 20 23 27 25	prdsbasprj	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑐 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑐 ) ) )
29		eqid	⊢ ( Base ‘ ( 𝑅 ‘ 𝑐 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑐 ) )
30		eqid	⊢ ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) = ( +_g ‘ ( 𝑅 ‘ 𝑐 ) )
31	29 30	cmncom	⊢ ( ( ( 𝑅 ‘ 𝑐 ) ∈ CMnd ∧ ( 𝑎 ‘ 𝑐 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑐 ) ) ∧ ( 𝑏 ‘ 𝑐 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑐 ) ) ) → ( ( 𝑎 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑏 ‘ 𝑐 ) ) = ( ( 𝑏 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑎 ‘ 𝑐 ) ) )
32	13 26 28 31	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑐 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑏 ‘ 𝑐 ) ) = ( ( 𝑏 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑎 ‘ 𝑐 ) ) )
33	32	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑐 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑏 ‘ 𝑐 ) ) ) = ( 𝑐 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑎 ‘ 𝑐 ) ) ) )
34		simp2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
35		simp3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
36		eqid	⊢ ( +_g ‘ 𝑌 ) = ( +_g ‘ 𝑌 )
37	1 14 16 19 22 34 35 36	prdsplusgval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( +_g ‘ 𝑌 ) 𝑏 ) = ( 𝑐 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑏 ‘ 𝑐 ) ) ) )
38	1 14 16 19 22 35 34 36	prdsplusgval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑏 ( +_g ‘ 𝑌 ) 𝑎 ) = ( 𝑐 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑐 ) ( +_g ‘ ( 𝑅 ‘ 𝑐 ) ) ( 𝑎 ‘ 𝑐 ) ) ) )
39	33 37 38	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( +_g ‘ 𝑌 ) 𝑏 ) = ( 𝑏 ( +_g ‘ 𝑌 ) 𝑎 ) )
40	5 6 11 39	iscmnd	⊢ ( 𝜑 → 𝑌 ∈ CMnd )

Metamath Proof Explorer

Theorem prdscmnd

Proof