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	$⊢ DProd = (g \in Grp, s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\} ⟼ ran (f \in \{h \in \underset{x \in dom s}{⨉} s (x) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f))$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-dprd

Detailed syntax breakdown