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

Proof

Step Hyp Ref Expression
1 prdscmnd.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 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 )