# Metamath Proof Explorer

## Definition df-dprd

Description: Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Assertion df-dprd ${⊢}\mathrm{DProd}=\left({g}\in \mathrm{Grp},{s}\in \left\{{h}|\left({h}:\mathrm{dom}{h}⟶\mathrm{SubGrp}\left({g}\right)\wedge \forall {x}\in \mathrm{dom}{h}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)\right)\right\}⟼\mathrm{ran}\left({f}\in \left\{{h}\in \underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)|{finSupp}_{{0}_{{g}}}\left({h}\right)\right\}⟼{\sum }_{{g}}{f}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cdprd ${class}\mathrm{DProd}$
1 vg ${setvar}{g}$
2 cgrp ${class}\mathrm{Grp}$
3 vs ${setvar}{s}$
4 vh ${setvar}{h}$
5 4 cv ${setvar}{h}$
6 5 cdm ${class}\mathrm{dom}{h}$
7 csubg ${class}\mathrm{SubGrp}$
8 1 cv ${setvar}{g}$
9 8 7 cfv ${class}\mathrm{SubGrp}\left({g}\right)$
10 6 9 5 wf ${wff}{h}:\mathrm{dom}{h}⟶\mathrm{SubGrp}\left({g}\right)$
11 vx ${setvar}{x}$
12 vy ${setvar}{y}$
13 11 cv ${setvar}{x}$
14 13 csn ${class}\left\{{x}\right\}$
15 6 14 cdif ${class}\left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)$
16 13 5 cfv ${class}{h}\left({x}\right)$
17 ccntz ${class}\mathrm{Cntz}$
18 8 17 cfv ${class}\mathrm{Cntz}\left({g}\right)$
19 12 cv ${setvar}{y}$
20 19 5 cfv ${class}{h}\left({y}\right)$
21 20 18 cfv ${class}\mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)$
22 16 21 wss ${wff}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)$
23 22 12 15 wral ${wff}\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)$
24 cmrc ${class}\mathrm{mrCls}$
25 9 24 cfv ${class}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)$
26 5 15 cima ${class}{h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]$
27 26 cuni ${class}\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]$
28 27 25 cfv ${class}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)$
29 16 28 cin ${class}\left({h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)\right)$
30 c0g ${class}{0}_{𝑔}$
31 8 30 cfv ${class}{0}_{{g}}$
32 31 csn ${class}\left\{{0}_{{g}}\right\}$
33 29 32 wceq ${wff}{h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}$
34 23 33 wa ${wff}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)$
35 34 11 6 wral ${wff}\forall {x}\in \mathrm{dom}{h}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)$
36 10 35 wa ${wff}\left({h}:\mathrm{dom}{h}⟶\mathrm{SubGrp}\left({g}\right)\wedge \forall {x}\in \mathrm{dom}{h}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)\right)$
37 36 4 cab ${class}\left\{{h}|\left({h}:\mathrm{dom}{h}⟶\mathrm{SubGrp}\left({g}\right)\wedge \forall {x}\in \mathrm{dom}{h}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)\right)\right\}$
38 vf ${setvar}{f}$
39 3 cv ${setvar}{s}$
40 39 cdm ${class}\mathrm{dom}{s}$
41 13 39 cfv ${class}{s}\left({x}\right)$
42 11 40 41 cixp ${class}\underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)$
43 cfsupp ${class}\mathrm{finSupp}$
44 5 31 43 wbr ${wff}{finSupp}_{{0}_{{g}}}\left({h}\right)$
45 44 4 42 crab ${class}\left\{{h}\in \underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)|{finSupp}_{{0}_{{g}}}\left({h}\right)\right\}$
46 cgsu ${class}{\Sigma }_{𝑔}$
47 38 cv ${setvar}{f}$
48 8 47 46 co ${class}\left({\sum }_{{g}},{f}\right)$
49 38 45 48 cmpt ${class}\left({f}\in \left\{{h}\in \underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)|{finSupp}_{{0}_{{g}}}\left({h}\right)\right\}⟼{\sum }_{{g}}{f}\right)$
50 49 crn ${class}\mathrm{ran}\left({f}\in \left\{{h}\in \underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)|{finSupp}_{{0}_{{g}}}\left({h}\right)\right\}⟼{\sum }_{{g}}{f}\right)$
51 1 3 2 37 50 cmpo ${class}\left({g}\in \mathrm{Grp},{s}\in \left\{{h}|\left({h}:\mathrm{dom}{h}⟶\mathrm{SubGrp}\left({g}\right)\wedge \forall {x}\in \mathrm{dom}{h}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)\right)\right\}⟼\mathrm{ran}\left({f}\in \left\{{h}\in \underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)|{finSupp}_{{0}_{{g}}}\left({h}\right)\right\}⟼{\sum }_{{g}}{f}\right)\right)$
52 0 51 wceq ${wff}\mathrm{DProd}=\left({g}\in \mathrm{Grp},{s}\in \left\{{h}|\left({h}:\mathrm{dom}{h}⟶\mathrm{SubGrp}\left({g}\right)\wedge \forall {x}\in \mathrm{dom}{h}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\mathrm{dom}{h}\setminus \left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{h}\left({x}\right)\subseteq \mathrm{Cntz}\left({g}\right)\left({h}\left({y}\right)\right)\wedge {h}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({g}\right)\right)\left(\bigcup {h}\left[\mathrm{dom}{h}\setminus \left\{{x}\right\}\right]\right)=\left\{{0}_{{g}}\right\}\right)\right)\right\}⟼\mathrm{ran}\left({f}\in \left\{{h}\in \underset{{x}\in \mathrm{dom}{s}}{⨉}{s}\left({x}\right)|{finSupp}_{{0}_{{g}}}\left({h}\right)\right\}⟼{\sum }_{{g}}{f}\right)\right)$