Metamath Proof Explorer

Theorem dprdssv

Description: The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprdssv.b ⊢ B = Base G
Assertion dprdssv ⊢ G DProd S ⊆ B

Proof

Step Hyp Ref Expression
1 dprdssv.b ⊢ B = Base G
2 eqid ⊢ dom ⁡ S = dom ⁡ S
3 eqid ⊢ 0 G = 0 G
4 eqid ⊢ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h = h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h
5 3 4 eldprd ⊢ dom ⁡ S = dom ⁡ S → x ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h x = ∑ G f
6 2 5 ax-mp ⊢ x ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h x = ∑ G f
7 eqid ⊢ Cntz ⁡ G = Cntz ⁡ G
8 dprdgrp ⊢ G dom ⁡ DProd S → G ∈ Grp
9 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
10 8 9 syl ⊢ G dom ⁡ DProd S → G ∈ Mnd
11 10 adantr ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → G ∈ Mnd
12 reldmdprd ⊢ Rel ⁡ dom ⁡ DProd
13 12 brrelex2i ⊢ G dom ⁡ DProd S → S ∈ V
14 13 dmexd ⊢ G dom ⁡ DProd S → dom ⁡ S ∈ V
15 14 adantr ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → dom ⁡ S ∈ V
16 simpl ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → G dom ⁡ DProd S
17 eqidd ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → dom ⁡ S = dom ⁡ S
18 simpr ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h
19 4 16 17 18 1 dprdff ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → f : dom ⁡ S ⟶ B
20 4 16 17 18 7 dprdfcntz ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → ran ⁡ f ⊆ Cntz ⁡ G ⁡ ran ⁡ f
21 4 16 17 18 dprdffsupp ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → finSupp 0 G⁡ f
22 1 3 7 11 15 19 20 21 gsumzcl ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → ∑ G f ∈ B
23 eleq1 ⊢ x = ∑ G f → x ∈ B ↔ ∑ G f ∈ B
24 22 23 syl5ibrcom ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → x = ∑ G f → x ∈ B
25 24 rexlimdva ⊢ G dom ⁡ DProd S → ∃ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h x = ∑ G f → x ∈ B
26 25 imp ⊢ G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h x = ∑ G f → x ∈ B
27 6 26 sylbi ⊢ x ∈ G DProd S → x ∈ B
28 27 ssriv ⊢ G DProd S ⊆ B