Metamath Proof Explorer

Theorem prdssgrpd

Description: The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 prdssgrpd.y 
 |-  Y = ( S Xs_ R )
2 prdssgrpd.i 
 |-  ( ph -> I e. W )
3 prdssgrpd.s 
 |-  ( ph -> S e. V )
4 prdssgrpd.r 
 |-  ( ph -> R : I --> Smgrp )
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 --> Smgrp )
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 prdsplusgsgrpcl 
 |-  ( ( 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. Smgrp )
19 18 adantlr 
 |-  ( ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) /\ c e. ( Base ` Y ) ) ) /\ y e. I ) -> ( R ` y ) e. Smgrp )
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 sgrpass 
 |-  ( ( ( R ` y ) e. Smgrp /\ ( ( 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 --> Smgrp )
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 prdsplusgsgrpcl 
 |-  ( ( 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 1 ovexi 
 |-  Y e. _V
54 53 a1i 
 |-  ( ph -> Y e. _V )
55 5 6 17 52 54 issgrpd 
 |-  ( ph -> Y e. Smgrp )