Step | Hyp | Ref
| Expression |
1 | | cdprd 19862 |
. 2
class
DProd |
2 | | vg |
. . 3
setvar ๐ |
3 | | vs |
. . 3
setvar ๐ |
4 | | cgrp 18818 |
. . 3
class
Grp |
5 | | vh |
. . . . . . . 8
setvar โ |
6 | 5 | cv 1540 |
. . . . . . 7
class โ |
7 | 6 | cdm 5676 |
. . . . . 6
class dom โ |
8 | 2 | cv 1540 |
. . . . . . 7
class ๐ |
9 | | csubg 18999 |
. . . . . . 7
class
SubGrp |
10 | 8, 9 | cfv 6543 |
. . . . . 6
class
(SubGrpโ๐) |
11 | 7, 10, 6 | wf 6539 |
. . . . 5
wff โ:dom โโถ(SubGrpโ๐) |
12 | | vx |
. . . . . . . . . . 11
setvar ๐ฅ |
13 | 12 | cv 1540 |
. . . . . . . . . 10
class ๐ฅ |
14 | 13, 6 | cfv 6543 |
. . . . . . . . 9
class (โโ๐ฅ) |
15 | | vy |
. . . . . . . . . . . 12
setvar ๐ฆ |
16 | 15 | cv 1540 |
. . . . . . . . . . 11
class ๐ฆ |
17 | 16, 6 | cfv 6543 |
. . . . . . . . . 10
class (โโ๐ฆ) |
18 | | ccntz 19178 |
. . . . . . . . . . 11
class
Cntz |
19 | 8, 18 | cfv 6543 |
. . . . . . . . . 10
class
(Cntzโ๐) |
20 | 17, 19 | cfv 6543 |
. . . . . . . . 9
class
((Cntzโ๐)โ(โโ๐ฆ)) |
21 | 14, 20 | wss 3948 |
. . . . . . . 8
wff (โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) |
22 | 13 | csn 4628 |
. . . . . . . . 9
class {๐ฅ} |
23 | 7, 22 | cdif 3945 |
. . . . . . . 8
class (dom
โ โ {๐ฅ}) |
24 | 21, 15, 23 | wral 3061 |
. . . . . . 7
wff
โ๐ฆ โ
(dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) |
25 | 6, 23 | cima 5679 |
. . . . . . . . . . 11
class (โ โ (dom โ โ {๐ฅ})) |
26 | 25 | cuni 4908 |
. . . . . . . . . 10
class โช (โ
โ (dom โ โ
{๐ฅ})) |
27 | | cmrc 17526 |
. . . . . . . . . . 11
class
mrCls |
28 | 10, 27 | cfv 6543 |
. . . . . . . . . 10
class
(mrClsโ(SubGrpโ๐)) |
29 | 26, 28 | cfv 6543 |
. . . . . . . . 9
class
((mrClsโ(SubGrpโ๐))โโช (โ โ (dom โ โ {๐ฅ}))) |
30 | 14, 29 | cin 3947 |
. . . . . . . 8
class ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) |
31 | | c0g 17384 |
. . . . . . . . . 10
class
0g |
32 | 8, 31 | cfv 6543 |
. . . . . . . . 9
class
(0gโ๐) |
33 | 32 | csn 4628 |
. . . . . . . 8
class
{(0gโ๐)} |
34 | 30, 33 | wceq 1541 |
. . . . . . 7
wff ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)} |
35 | 24, 34 | wa 396 |
. . . . . 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 396 |
. . . 4
wff (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)})) |
38 | 37, 5 | cab 2709 |
. . 3
class {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))} |
39 | | vf |
. . . . 5
setvar ๐ |
40 | | cfsupp 9360 |
. . . . . . 7
class
finSupp |
41 | 6, 32, 40 | wbr 5148 |
. . . . . 6
wff โ finSupp
(0gโ๐) |
42 | 3 | cv 1540 |
. . . . . . . 8
class ๐ |
43 | 42 | cdm 5676 |
. . . . . . 7
class dom ๐ |
44 | 13, 42 | cfv 6543 |
. . . . . . 7
class (๐ โ๐ฅ) |
45 | 12, 43, 44 | cixp 8890 |
. . . . . 6
class X๐ฅ โ
dom ๐ (๐ โ๐ฅ) |
46 | 41, 5, 45 | crab 3432 |
. . . . 5
class {โ โ X๐ฅ โ
dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} |
47 | 39 | cv 1540 |
. . . . . 6
class ๐ |
48 | | cgsu 17385 |
. . . . . 6
class
ฮฃg |
49 | 8, 47, 48 | co 7408 |
. . . . 5
class (๐ ฮฃg
๐) |
50 | 39, 46, 49 | cmpt 5231 |
. . . 4
class (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) |
51 | 50 | crn 5677 |
. . 3
class ran
(๐ โ {โ โ X๐ฅ โ
dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) |
52 | 2, 3, 4, 38, 51 | cmpo 7410 |
. 2
class (๐ โ Grp, ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))} โฆ ran (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
53 | 1, 52 | wceq 1541 |
1
wff DProd =
(๐ โ Grp, ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ฅ โ dom โ(โ๐ฆ โ (dom โ โ {๐ฅ})(โโ๐ฅ) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐ฅ) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐ฅ})))) =
{(0gโ๐)}))} โฆ ran (๐ โ {โ โ X๐ฅ โ dom ๐ (๐ โ๐ฅ) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |