Detailed syntax breakdown of Definition df-dprd
Step | Hyp | Ref
| Expression |
1 | | cdprd 19605 |
. 2
class
DProd |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cgrp 18586 |
. . 3
class
Grp |
5 | | vh |
. . . . . . . 8
setvar ℎ |
6 | 5 | cv 1538 |
. . . . . . 7
class ℎ |
7 | 6 | cdm 5590 |
. . . . . 6
class dom ℎ |
8 | 2 | cv 1538 |
. . . . . . 7
class 𝑔 |
9 | | csubg 18758 |
. . . . . . 7
class
SubGrp |
10 | 8, 9 | cfv 6437 |
. . . . . 6
class
(SubGrp‘𝑔) |
11 | 7, 10, 6 | wf 6433 |
. . . . 5
wff ℎ:dom ℎ⟶(SubGrp‘𝑔) |
12 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
13 | 12 | cv 1538 |
. . . . . . . . . 10
class 𝑥 |
14 | 13, 6 | cfv 6437 |
. . . . . . . . 9
class (ℎ‘𝑥) |
15 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
16 | 15 | cv 1538 |
. . . . . . . . . . 11
class 𝑦 |
17 | 16, 6 | cfv 6437 |
. . . . . . . . . 10
class (ℎ‘𝑦) |
18 | | ccntz 18930 |
. . . . . . . . . . 11
class
Cntz |
19 | 8, 18 | cfv 6437 |
. . . . . . . . . 10
class
(Cntz‘𝑔) |
20 | 17, 19 | cfv 6437 |
. . . . . . . . 9
class
((Cntz‘𝑔)‘(ℎ‘𝑦)) |
21 | 14, 20 | wss 3888 |
. . . . . . . 8
wff (ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) |
22 | 13 | csn 4562 |
. . . . . . . . 9
class {𝑥} |
23 | 7, 22 | cdif 3885 |
. . . . . . . 8
class (dom
ℎ ∖ {𝑥}) |
24 | 21, 15, 23 | wral 3065 |
. . . . . . 7
wff
∀𝑦 ∈
(dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) |
25 | 6, 23 | cima 5593 |
. . . . . . . . . . 11
class (ℎ “ (dom ℎ ∖ {𝑥})) |
26 | 25 | cuni 4840 |
. . . . . . . . . 10
class ∪ (ℎ
“ (dom ℎ ∖
{𝑥})) |
27 | | cmrc 17301 |
. . . . . . . . . . 11
class
mrCls |
28 | 10, 27 | cfv 6437 |
. . . . . . . . . 10
class
(mrCls‘(SubGrp‘𝑔)) |
29 | 26, 28 | cfv 6437 |
. . . . . . . . 9
class
((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥}))) |
30 | 14, 29 | cin 3887 |
. . . . . . . 8
class ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) |
31 | | c0g 17159 |
. . . . . . . . . 10
class
0g |
32 | 8, 31 | cfv 6437 |
. . . . . . . . 9
class
(0g‘𝑔) |
33 | 32 | csn 4562 |
. . . . . . . 8
class
{(0g‘𝑔)} |
34 | 30, 33 | wceq 1539 |
. . . . . . 7
wff ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)} |
35 | 24, 34 | wa 396 |
. . . . . 6
wff
(∀𝑦 ∈
(dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)}) |
36 | 35, 12, 7 | wral 3065 |
. . . . 5
wff
∀𝑥 ∈ dom
ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)}) |
37 | 11, 36 | wa 396 |
. . . 4
wff (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)})) |
38 | 37, 5 | cab 2716 |
. . 3
class {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)}))} |
39 | | vf |
. . . . 5
setvar 𝑓 |
40 | | cfsupp 9137 |
. . . . . . 7
class
finSupp |
41 | 6, 32, 40 | wbr 5075 |
. . . . . 6
wff ℎ finSupp
(0g‘𝑔) |
42 | 3 | cv 1538 |
. . . . . . . 8
class 𝑠 |
43 | 42 | cdm 5590 |
. . . . . . 7
class dom 𝑠 |
44 | 13, 42 | cfv 6437 |
. . . . . . 7
class (𝑠‘𝑥) |
45 | 12, 43, 44 | cixp 8694 |
. . . . . 6
class X𝑥 ∈
dom 𝑠(𝑠‘𝑥) |
46 | 41, 5, 45 | crab 3069 |
. . . . 5
class {ℎ ∈ X𝑥 ∈
dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} |
47 | 39 | cv 1538 |
. . . . . 6
class 𝑓 |
48 | | cgsu 17160 |
. . . . . 6
class
Σg |
49 | 8, 47, 48 | co 7284 |
. . . . 5
class (𝑔 Σg
𝑓) |
50 | 39, 46, 49 | cmpt 5158 |
. . . 4
class (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) |
51 | 50 | crn 5591 |
. . 3
class ran
(𝑓 ∈ {ℎ ∈ X𝑥 ∈
dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓)) |
52 | 2, 3, 4, 38, 51 | cmpo 7286 |
. 2
class (𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) |
53 | 1, 52 | wceq 1539 |
1
wff DProd =
(𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ
“ (dom ℎ ∖
{𝑥})))) =
{(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) |