Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. 2
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ ๐บdom DProd ๐) |
2 | | reldmdprd 19916 |
. . . . . 6
โข Rel dom
DProd |
3 | 2 | brrelex2i 5726 |
. . . . 5
โข (๐บdom DProd ๐ โ ๐ โ V) |
4 | 3 | adantr 480 |
. . . 4
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ ๐ โ V) |
5 | 2 | brrelex1i 5725 |
. . . . . 6
โข (๐บdom DProd ๐ โ ๐บ โ V) |
6 | | breq1 5144 |
. . . . . . . 8
โข (๐ = ๐บ โ (๐dom DProd ๐ โ ๐บdom DProd ๐ )) |
7 | | oveq1 7411 |
. . . . . . . . 9
โข (๐ = ๐บ โ (๐ DProd ๐ ) = (๐บ DProd ๐ )) |
8 | | fveq2 6884 |
. . . . . . . . . . . . . 14
โข (๐ = ๐บ โ (0gโ๐) = (0gโ๐บ)) |
9 | | dprdval.0 |
. . . . . . . . . . . . . 14
โข 0 =
(0gโ๐บ) |
10 | 8, 9 | eqtr4di 2784 |
. . . . . . . . . . . . 13
โข (๐ = ๐บ โ (0gโ๐) = 0 ) |
11 | 10 | breq2d 5153 |
. . . . . . . . . . . 12
โข (๐ = ๐บ โ (โ finSupp (0gโ๐) โ โ finSupp 0 )) |
12 | 11 | rabbidv 3434 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} = {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 }) |
13 | | oveq1 7411 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ (๐ ฮฃg ๐) = (๐บ ฮฃg ๐)) |
14 | 12, 13 | mpteq12dv 5232 |
. . . . . . . . . 10
โข (๐ = ๐บ โ (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) = (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) |
15 | 14 | rneqd 5930 |
. . . . . . . . 9
โข (๐ = ๐บ โ ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) |
16 | 7, 15 | eqeq12d 2742 |
. . . . . . . 8
โข (๐ = ๐บ โ ((๐ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)))) |
17 | 6, 16 | imbi12d 344 |
. . . . . . 7
โข (๐ = ๐บ โ ((๐dom DProd ๐ โ (๐ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) โ (๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))))) |
18 | | df-br 5142 |
. . . . . . . . 9
โข (๐dom DProd ๐ โ โจ๐, ๐ โฉ โ dom DProd ) |
19 | | fvex 6897 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ๐) โ V |
20 | 19 | rgenw 3059 |
. . . . . . . . . . . . . . . 16
โข
โ๐ โ dom
๐ (๐ โ๐) โ V |
21 | | ixpexg 8915 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
dom ๐ (๐ โ๐) โ V โ X๐ โ
dom ๐ (๐ โ๐) โ V) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข X๐ โ
dom ๐ (๐ โ๐) โ V |
23 | 22 | mptrabex 7221 |
. . . . . . . . . . . . . 14
โข (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
24 | 23 | rnex 7899 |
. . . . . . . . . . . . 13
โข ran
(๐ โ {โ โ X๐ โ
dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
25 | 24 | rgen2w 3060 |
. . . . . . . . . . . 12
โข
โ๐ โ Grp
โ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
26 | | df-dprd 19914 |
. . . . . . . . . . . . 13
โข DProd =
(๐ โ Grp, ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))} โฆ ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
27 | 26 | fmpox 8049 |
. . . . . . . . . . . 12
โข
(โ๐ โ
Grp โ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V โ DProd
:โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})โถV) |
28 | 25, 27 | mpbi 229 |
. . . . . . . . . . 11
โข DProd
:โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})โถV |
29 | 28 | fdmi 6722 |
. . . . . . . . . 10
โข dom DProd
= โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}) |
30 | 29 | eleq2i 2819 |
. . . . . . . . 9
โข
(โจ๐, ๐ โฉ โ dom DProd โ
โจ๐, ๐ โฉ โ โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})) |
31 | | opeliunxp 5736 |
. . . . . . . . 9
โข
(โจ๐, ๐ โฉ โ โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}) โ (๐ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})) |
32 | 18, 30, 31 | 3bitri 297 |
. . . . . . . 8
โข (๐dom DProd ๐ โ (๐ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})) |
33 | 26 | ovmpt4g 7550 |
. . . . . . . . 9
โข ((๐ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))} โง ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V) โ (๐ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
34 | 24, 33 | mp3an3 1446 |
. . . . . . . 8
โข ((๐ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}) โ (๐ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
35 | 32, 34 | sylbi 216 |
. . . . . . 7
โข (๐dom DProd ๐ โ (๐ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
36 | 17, 35 | vtoclg 3537 |
. . . . . 6
โข (๐บ โ V โ (๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)))) |
37 | 5, 36 | mpcom 38 |
. . . . 5
โข (๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) |
38 | 37 | sbcth 3787 |
. . . 4
โข (๐ โ V โ [๐ / ๐ ](๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)))) |
39 | 4, 38 | syl 17 |
. . 3
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ [๐ / ๐ ](๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)))) |
40 | | simpr 484 |
. . . . . 6
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ ๐ = ๐) |
41 | 40 | breq2d 5153 |
. . . . 5
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐บdom DProd ๐ โ ๐บdom DProd ๐)) |
42 | 40 | oveq2d 7420 |
. . . . . 6
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐บ DProd ๐ ) = (๐บ DProd ๐)) |
43 | 40 | dmeqd 5898 |
. . . . . . . . . . . . 13
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ dom ๐ = dom ๐) |
44 | | simplr 766 |
. . . . . . . . . . . . 13
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ dom ๐ = ๐ผ) |
45 | 43, 44 | eqtrd 2766 |
. . . . . . . . . . . 12
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ dom ๐ = ๐ผ) |
46 | 45 | ixpeq1d 8902 |
. . . . . . . . . . 11
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ X๐ โ dom ๐ (๐ โ๐) = X๐ โ ๐ผ (๐ โ๐)) |
47 | 40 | fveq1d 6886 |
. . . . . . . . . . . 12
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐ โ๐) = (๐โ๐)) |
48 | 47 | ixpeq2dv 8906 |
. . . . . . . . . . 11
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ X๐ โ ๐ผ (๐ โ๐) = X๐ โ ๐ผ (๐โ๐)) |
49 | 46, 48 | eqtrd 2766 |
. . . . . . . . . 10
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ X๐ โ dom ๐ (๐ โ๐) = X๐ โ ๐ผ (๐โ๐)) |
50 | 49 | rabeqdv 3441 |
. . . . . . . . 9
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } = {โ โ X๐ โ ๐ผ (๐โ๐) โฃ โ finSupp 0 }) |
51 | | dprdval.w |
. . . . . . . . 9
โข ๐ = {โ โ X๐ โ ๐ผ (๐โ๐) โฃ โ finSupp 0 } |
52 | 50, 51 | eqtr4di 2784 |
. . . . . . . 8
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } = ๐) |
53 | | eqidd 2727 |
. . . . . . . 8
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐บ ฮฃg ๐) = (๐บ ฮฃg ๐)) |
54 | 52, 53 | mpteq12dv 5232 |
. . . . . . 7
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)) = (๐ โ ๐ โฆ (๐บ ฮฃg ๐))) |
55 | 54 | rneqd 5930 |
. . . . . 6
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐))) |
56 | 42, 55 | eqeq12d 2742 |
. . . . 5
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ ((๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)) โ (๐บ DProd ๐) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐)))) |
57 | 41, 56 | imbi12d 344 |
. . . 4
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ ((๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) โ (๐บdom DProd ๐ โ (๐บ DProd ๐) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐))))) |
58 | 4, 57 | sbcied 3817 |
. . 3
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ ([๐ / ๐ ](๐บdom DProd ๐ โ (๐บ DProd ๐ ) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) โ (๐บdom DProd ๐ โ (๐บ DProd ๐) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐))))) |
59 | 39, 58 | mpbid 231 |
. 2
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ (๐บdom DProd ๐ โ (๐บ DProd ๐) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐)))) |
60 | 1, 59 | mpd 15 |
1
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ (๐บ DProd ๐) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐))) |