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 )

Metamath Proof Explorer

Theorem prdsgrpd

Proof