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 8 grpmndd ⊢ G dom ⁡ DProd S → G ∈ Mnd
10 9 adantr ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → G ∈ Mnd
11 reldmdprd ⊢ Rel ⁡ dom ⁡ DProd
12 11 brrelex2i ⊢ G dom ⁡ DProd S → S ∈ V
13 12 dmexd ⊢ G dom ⁡ DProd S → dom ⁡ S ∈ V
14 13 adantr ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → dom ⁡ S ∈ V
15 simpl ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → G dom ⁡ DProd S
16 eqidd ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → dom ⁡ S = dom ⁡ S
17 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
18 4 15 16 17 1 dprdff ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → f : dom ⁡ S ⟶ B
19 4 15 16 17 7 dprdfcntz ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → ran ⁡ f ⊆ Cntz ⁡ G ⁡ ran ⁡ f
20 4 15 16 17 dprdffsupp ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → finSupp 0 G⁡ f
21 1 3 7 10 14 18 19 20 gsumzcl ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → ∑ G f ∈ B
22 eleq1 ⊢ x = ∑ G f → x ∈ B ↔ ∑ G f ∈ B
23 21 22 syl5ibrcom ⊢ G dom ⁡ DProd S ∧ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h → x = ∑ G f → x ∈ B
24 23 rexlimdva ⊢ G dom ⁡ DProd S → ∃ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h x = ∑ G f → x ∈ B
25 24 imp ⊢ G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ dom ⁡ S S ⁡ i | finSupp 0 G⁡ h x = ∑ G f → x ∈ B
26 6 25 sylbi ⊢ x ∈ G DProd S → x ∈ B
27 26 ssriv ⊢ G DProd S ⊆ B