This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( 𝑆 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 )