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 ⊢ DProd = g ∈ Grp , s ∈ h | h : dom ⁡ h ⟶ SubGrp ⁡ g ∧ ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g ⟼ ran ⁡ f ∈ h ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h ⟼ ∑ 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 ⊆ Cntz ⁡ g ⁡ h ⁡ y
23 22 12 15 wral wff ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ 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 ∩ 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 ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g
34 23 33 wa wff ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g
35 34 11 6 wral wff ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g
36 10 35 wa wff h : dom ⁡ h ⟶ SubGrp ⁡ g ∧ ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g
37 36 4 cab class h | h : dom ⁡ h ⟶ SubGrp ⁡ g ∧ ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ 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 ⨉ x ∈ 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 ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h
46 cgsu class Σ𝑔
47 38 cv setvar f
48 8 47 46 co class ∑ g f
49 38 45 48 cmpt class f ∈ h ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h ⟼ ∑ g f
50 49 crn class ran ⁡ f ∈ h ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h ⟼ ∑ g f
51 1 3 2 37 50 cmpo class g ∈ Grp , s ∈ h | h : dom ⁡ h ⟶ SubGrp ⁡ g ∧ ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g ⟼ ran ⁡ f ∈ h ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h ⟼ ∑ g f
52 0 51 wceq wff DProd = g ∈ Grp , s ∈ h | h : dom ⁡ h ⟶ SubGrp ⁡ g ∧ ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g ⟼ ran ⁡ f ∈ h ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h ⟼ ∑ g f