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=BaseG
Assertion dprdssv ⊢GDProdS⊆B

Proof

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