Definition df-dprd 20015

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

Assertion

Ref	Expression
df-dprd	⊢ DProd = (𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)))

Distinct variable group:   𝑔,ℎ,𝑓,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-dprd

Step	Hyp	Ref	Expression
1		cdprd 20013	. 2 class DProd
2		vg	. . 3 setvar 𝑔
3		vs	. . 3 setvar 𝑠
4		cgrp 18951	. . 3 class Grp
5		vh	. . . . . . . 8 setvar ℎ
6	5	cv 1539	. . . . . . 7 class ℎ
7	6	cdm 5685	. . . . . 6 class dom ℎ
8	2	cv 1539	. . . . . . 7 class 𝑔
9		csubg 19138	. . . . . . 7 class SubGrp
10	8, 9	cfv 6561	. . . . . 6 class (SubGrp‘𝑔)
11	7, 10, 6	wf 6557	. . . . 5 wff ℎ:dom ℎ⟶(SubGrp‘𝑔)
12		vx	. . . . . . . . . . 11 setvar 𝑥
13	12	cv 1539	. . . . . . . . . 10 class 𝑥
14	13, 6	cfv 6561	. . . . . . . . 9 class (ℎ‘𝑥)
15		vy	. . . . . . . . . . . 12 setvar 𝑦
16	15	cv 1539	. . . . . . . . . . 11 class 𝑦
17	16, 6	cfv 6561	. . . . . . . . . 10 class (ℎ‘𝑦)
18		ccntz 19333	. . . . . . . . . . 11 class Cntz
19	8, 18	cfv 6561	. . . . . . . . . 10 class (Cntz‘𝑔)
20	17, 19	cfv 6561	. . . . . . . . 9 class ((Cntz‘𝑔)‘(ℎ‘𝑦))
21	14, 20	wss 3951	. . . . . . . 8 wff (ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦))
22	13	csn 4626	. . . . . . . . 9 class {𝑥}
23	7, 22	cdif 3948	. . . . . . . 8 class (dom ℎ ∖ {𝑥})
24	21, 15, 23	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦))
25	6, 23	cima 5688	. . . . . . . . . . 11 class (ℎ “ (dom ℎ ∖ {𝑥}))
26	25	cuni 4907	. . . . . . . . . 10 class ∪ (ℎ “ (dom ℎ ∖ {𝑥}))
27		cmrc 17626	. . . . . . . . . . 11 class mrCls
28	10, 27	cfv 6561	. . . . . . . . . 10 class (mrCls‘(SubGrp‘𝑔))
29	26, 28	cfv 6561	. . . . . . . . 9 class ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))
30	14, 29	cin 3950	. . . . . . . 8 class ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥}))))
31		c0g 17484	. . . . . . . . . 10 class 0g
32	8, 31	cfv 6561	. . . . . . . . 9 class (0g‘𝑔)
33	32	csn 4626	. . . . . . . 8 class {(0g‘𝑔)}
34	30, 33	wceq 1540	. . . . . . 7 wff ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}
35	24, 34	wa 395	. . . . . 6 wff (∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)})
36	35, 12, 7	wral 3061	. . . . 5 wff ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)})
37	11, 36	wa 395	. . . 4 wff (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))
38	37, 5	cab 2714	. . 3 class {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))}
39		vf	. . . . 5 setvar 𝑓
40		cfsupp 9401	. . . . . . 7 class finSupp
41	6, 32, 40	wbr 5143	. . . . . 6 wff ℎ finSupp (0g‘𝑔)
42	3	cv 1539	. . . . . . . 8 class 𝑠
43	42	cdm 5685	. . . . . . 7 class dom 𝑠
44	13, 42	cfv 6561	. . . . . . 7 class (𝑠‘𝑥)
45	12, 43, 44	cixp 8937	. . . . . 6 class X𝑥 ∈ dom 𝑠(𝑠‘𝑥)
46	41, 5, 45	crab 3436	. . . . 5 class {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)}
47	39	cv 1539	. . . . . 6 class 𝑓
48		cgsu 17485	. . . . . 6 class Σg
49	8, 47, 48	co 7431	. . . . 5 class (𝑔 Σg 𝑓)
50	39, 46, 49	cmpt 5225	. . . 4 class (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))
51	50	crn 5686	. . 3 class ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))
52	2, 3, 4, 38, 51	cmpo 7433	. 2 class (𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)))
53	1, 52	wceq 1540	1 wff DProd = (𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)))

This definition is referenced by:  reldmdprd  20017  dmdprd  20018  dprdval  20023