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	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsgrpd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsgrpd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsgrpd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
Assertion	prdsgrpd	⊢ ( 𝜑 → 𝑌 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		prdsgrpd.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsgrpd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3		prdsgrpd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsgrpd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
5		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
6		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) )
7		grpmnd	⊢ ( 𝑎 ∈ Grp → 𝑎 ∈ Mnd )
8	7	ssriv	⊢ Grp ⊆ Mnd
9		fss	⊢ ( ( 𝑅 : 𝐼 ⟶ Grp ∧ Grp ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd )
10	4 8 9	sylancl	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
11	1 2 3 10	prds0g	⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑌 ) )
12	1 2 3 10	prdsmndd	⊢ ( 𝜑 → 𝑌 ∈ Mnd )
13		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
14		eqid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
15	3	elexd	⊢ ( 𝜑 → 𝑆 ∈ V )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑆 ∈ V )
17	2	elexd	⊢ ( 𝜑 → 𝐼 ∈ V )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝐼 ∈ V )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 : 𝐼 ⟶ Grp )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
21		eqid	⊢ ( 0g ∘ 𝑅 ) = ( 0g ∘ 𝑅 )
22		eqid	⊢ ( 𝑏 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) = ( 𝑏 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) )
23	1 13 14 16 18 19 20 21 22	prdsinvlem	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑏 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑏 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) ( +g ‘ 𝑌 ) 𝑎 ) = ( 0g ∘ 𝑅 ) ) )
24	23	simpld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑏 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) ∈ ( Base ‘ 𝑌 ) )
25	23	simprd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑏 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) ) ( +g ‘ 𝑌 ) 𝑎 ) = ( 0g ∘ 𝑅 ) )
26	5 6 11 12 24 25	isgrpd2	⊢ ( 𝜑 → 𝑌 ∈ Grp )