Metamath Proof Explorer

Theorem prdsmndd

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

Ref Expression
Hypotheses prdsmndd.y 
|- Y = ( S Xs_ R )
prdsmndd.i 
|- ( ph -> I e. W )
prdsmndd.s 
|- ( ph -> S e. V )
prdsmndd.r 
|- ( ph -> R : I --> Mnd )
Assertion prdsmndd 
|- ( ph -> Y e. Mnd )

Proof

Step Hyp Ref Expression
1 prdsmndd.y 
 |-  Y = ( S Xs_ R )
2 prdsmndd.i 
 |-  ( ph -> I e. W )
3 prdsmndd.s 
 |-  ( ph -> S e. V )
4 prdsmndd.r 
 |-  ( ph -> R : I --> Mnd )
5 eqidd 
 |-  ( ph -> ( Base ` Y ) = ( Base ` Y ) )
6 eqidd 
 |-  ( ph -> ( +g ` Y ) = ( +g ` Y ) )
7 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
8 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
9 3 elexd 
 |-  ( ph -> S e. _V )
10 9 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> S e. _V )
11 2 elexd 
 |-  ( ph -> I e. _V )
12 11 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> I e. _V )
13 4 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> R : I --> Mnd )
14 simprl 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> a e. ( Base ` Y ) )
15 simprr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> b e. ( Base ` Y ) )
16 1 7 8 10 12 13 14 15 prdsplusgcl 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> ( a ( +g ` Y ) b ) e. ( Base ` Y ) )
17 16 3impb 
 |-  ( ( ph /\ a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) -> ( a ( +g ` Y ) b ) e. ( Base ` Y ) )
18 4 ffvelcdmda 
 |-  ( ( ph /\ y e. I ) -> ( R ` y ) e. Mnd )
19 18 adantlr 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( R ` y ) e. Mnd )
20 9 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> S e. _V )
21 11 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> I e. _V )
22 4 ffnd 
 |-  ( ph -> R Fn I )
23 22 ad2antrr 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> R Fn I )
24 simplr1 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> a e. ( Base ` Y ) )
25 simpr 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> y e. I )
26 1 7 20 21 23 24 25 prdsbasprj 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( a ` y ) e. ( Base ` ( R ` y ) ) )
27 simplr2 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> b e. ( Base ` Y ) )
28 1 7 20 21 23 27 25 prdsbasprj 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( b ` y ) e. ( Base ` ( R ` y ) ) )
29 simplr3 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> c e. ( Base ` Y ) )
30 1 7 20 21 23 29 25 prdsbasprj 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( c ` y ) e. ( Base ` ( R ` y ) ) )
31 eqid 
 |-  ( Base ` ( R ` y ) ) = ( Base ` ( R ` y ) )
32 eqid 
 |-  ( +g ` ( R ` y ) ) = ( +g ` ( R ` y ) )
33 31 32 mndass 
 |-  ( ( ( R ` y ) e. Mnd /\ ( ( a ` y ) e. ( Base ` ( R ` y ) ) /\ ( b ` y ) e. ( Base ` ( R ` y ) ) /\ ( c ` y ) e. ( Base ` ( R ` y ) ) ) ) -> ( ( ( a ` y ) ( +g ` ( R ` y ) ) ( b ` y ) ) ( +g ` ( R ` y ) ) ( c ` y ) ) = ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) ) )
34 19 26 28 30 33 syl13anc 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( ( ( a ` y ) ( +g ` ( R ` y ) ) ( b ` y ) ) ( +g ` ( R ` y ) ) ( c ` y ) ) = ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) ) )
35 1 7 20 21 23 24 27 8 25 prdsplusgfval 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( ( a ( +g ` Y ) b ) ` y ) = ( ( a ` y ) ( +g ` ( R ` y ) ) ( b ` y ) ) )
36 35 oveq1d 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( ( ( a ( +g ` Y ) b ) ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) = ( ( ( a ` y ) ( +g ` ( R ` y ) ) ( b ` y ) ) ( +g ` ( R ` y ) ) ( c ` y ) ) )
37 1 7 20 21 23 27 29 8 25 prdsplusgfval 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( ( b ( +g ` Y ) c ) ` y ) = ( ( b ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) )
38 37 oveq2d 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ( +g ` Y ) c ) ` y ) ) = ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) ) )
39 34 36 38 3eqtr4d 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( ( ( a ( +g ` Y ) b ) ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) = ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ( +g ` Y ) c ) ` y ) ) )
40 39 mpteq2dva 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> ( y e. I |-> ( ( ( a ( +g ` Y ) b ) ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) ) = ( y e. I |-> ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ( +g ` Y ) c ) ` y ) ) ) )
41 9 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> S e. _V )
42 11 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> I e. _V )
43 22 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> R Fn I )
44 16 3adantr3 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> ( a ( +g ` Y ) b ) e. ( Base ` Y ) )
45 simpr3 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> c e. ( Base ` Y ) )
46 1 7 41 42 43 44 45 8 prdsplusgval 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> ( ( a ( +g ` Y ) b ) ( +g ` Y ) c ) = ( y e. I |-> ( ( ( a ( +g ` Y ) b ) ` y ) ( +g ` ( R ` y ) ) ( c ` y ) ) ) )
47 simpr1 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> a e. ( Base ` Y ) )
48 4 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> R : I --> Mnd )
49 simpr2 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> b e. ( Base ` Y ) )
50 1 7 8 41 42 48 49 45 prdsplusgcl 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> ( b ( +g ` Y ) c ) e. ( Base ` Y ) )
51 1 7 41 42 43 47 50 8 prdsplusgval 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> ( a ( +g ` Y ) ( b ( +g ` Y ) c ) ) = ( y e. I |-> ( ( a ` y ) ( +g ` ( R ` y ) ) ( ( b ( +g ` Y ) c ) ` y ) ) ) )
52 40 46 51 3eqtr4d 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) -> ( ( a ( +g ` Y ) b ) ( +g ` Y ) c ) = ( a ( +g ` Y ) ( b ( +g ` Y ) c ) ) )
53 eqid 
 |-  ( 0g o. R ) = ( 0g o. R )
54 1 7 8 9 11 4 53 prdsidlem 
 |-  ( ph -> ( ( 0g o. R ) e. ( Base ` Y ) /\ A. a e. ( Base ` Y ) ( ( ( 0g o. R ) ( +g ` Y ) a ) = a /\ ( a ( +g ` Y ) ( 0g o. R ) ) = a ) ) )
55 54 simpld 
 |-  ( ph -> ( 0g o. R ) e. ( Base ` Y ) )
56 54 simprd 
 |-  ( ph -> A. a e. ( Base ` Y ) ( ( ( 0g o. R ) ( +g ` Y ) a ) = a /\ ( a ( +g ` Y ) ( 0g o. R ) ) = a ) )
57 56 r19.21bi 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> ( ( ( 0g o. R ) ( +g ` Y ) a ) = a /\ ( a ( +g ` Y ) ( 0g o. R ) ) = a ) )
58 57 simpld 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> ( ( 0g o. R ) ( +g ` Y ) a ) = a )
59 57 simprd 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> ( a ( +g ` Y ) ( 0g o. R ) ) = a )
60 5 6 17 52 55 58 59 ismndd 
 |-  ( ph -> Y e. Mnd )