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 Xs_ R )
prdscmnd.i 
|- ( ph -> I e. W )
prdscmnd.s 
|- ( ph -> S e. V )
prdscmnd.r 
|- ( ph -> R : I --> CMnd )
Assertion prdscmnd 
|- ( ph -> Y e. CMnd )

Proof

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