Metamath Proof Explorer

Theorem prdsgrpd

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

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

Proof

Step Hyp Ref Expression
1 prdsgrpd.y 
 |-  Y = ( S Xs_ R )
2 prdsgrpd.i 
 |-  ( ph -> I e. W )
3 prdsgrpd.s 
 |-  ( ph -> S e. V )
4 prdsgrpd.r 
 |-  ( ph -> R : I --> Grp )
5 eqidd 
 |-  ( ph -> ( Base ` Y ) = ( Base ` Y ) )
6 eqidd 
 |-  ( ph -> ( +g ` Y ) = ( +g ` Y ) )
7 grpmnd 
 |-  ( a e. Grp -> a e. Mnd )
8 7 ssriv 
 |-  Grp C_ Mnd
9 fss 
 |-  ( ( R : I --> Grp /\ Grp C_ Mnd ) -> R : I --> Mnd )
10 4 8 9 sylancl 
 |-  ( ph -> R : I --> Mnd )
11 1 2 3 10 prds0g 
 |-  ( ph -> ( 0g o. R ) = ( 0g ` Y ) )
12 1 2 3 10 prdsmndd 
 |-  ( ph -> Y e. Mnd )
13 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
14 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
15 3 elexd 
 |-  ( ph -> S e. _V )
16 15 adantr 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> S e. _V )
17 2 elexd 
 |-  ( ph -> I e. _V )
18 17 adantr 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> I e. _V )
19 4 adantr 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> R : I --> Grp )
20 simpr 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> a e. ( Base ` Y ) )
21 eqid 
 |-  ( 0g o. R ) = ( 0g o. R )
22 eqid 
 |-  ( b e. I |-> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) ) = ( b e. I |-> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) )
23 1 13 14 16 18 19 20 21 22 prdsinvlem 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> ( ( b e. I |-> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) ) e. ( Base ` Y ) /\ ( ( b e. I |-> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) ) ( +g ` Y ) a ) = ( 0g o. R ) ) )
24 23 simpld 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> ( b e. I |-> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) ) e. ( Base ` Y ) )
25 23 simprd 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> ( ( b e. I |-> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) ) ( +g ` Y ) a ) = ( 0g o. R ) )
26 5 6 11 12 24 25 isgrpd2 
 |-  ( ph -> Y e. Grp )