Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. 2
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ ๐บdom DProd ๐) |
2 | | reldmdprd 19866 |
. . . . . 6
โข Rel dom
DProd |
3 | 2 | brrelex2i 5733 |
. . . . 5
โข (๐บdom DProd ๐ โ ๐ โ V) |
4 | 3 | adantr 481 |
. . . 4
โข ((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โ ๐ โ V) |
5 | 2 | brrelex1i 5732 |
. . . . . 6
โข (๐บdom DProd ๐ โ ๐บ โ V) |
6 | | breq1 5151 |
. . . . . . . 8
โข (๐ = ๐บ โ (๐dom DProd ๐ โ ๐บdom DProd ๐ )) |
7 | | oveq1 7415 |
. . . . . . . . 9
โข (๐ = ๐บ โ (๐ DProd ๐ ) = (๐บ DProd ๐ )) |
8 | | fveq2 6891 |
. . . . . . . . . . . . . 14
โข (๐ = ๐บ โ (0gโ๐) = (0gโ๐บ)) |
9 | | dprdval.0 |
. . . . . . . . . . . . . 14
โข 0 =
(0gโ๐บ) |
10 | 8, 9 | eqtr4di 2790 |
. . . . . . . . . . . . 13
โข (๐ = ๐บ โ (0gโ๐) = 0 ) |
11 | 10 | breq2d 5160 |
. . . . . . . . . . . 12
โข (๐ = ๐บ โ (โ finSupp (0gโ๐) โ โ finSupp 0 )) |
12 | 11 | rabbidv 3440 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} = {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 }) |
13 | | oveq1 7415 |
. . . . . . . . . . 11
โข (๐ = ๐บ โ (๐ ฮฃg ๐) = (๐บ ฮฃg ๐)) |
14 | 12, 13 | mpteq12dv 5239 |
. . . . . . . . . 10
โข (๐ = ๐บ โ (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) = (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) |
15 | 14 | rneqd 5937 |
. . . . . . . . 9
โข (๐ = ๐บ โ ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) = ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐))) |
16 | 7, 15 | eqeq12d 2748 |
. . . . . . . 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 5149 |
. . . . . . . . 9
โข (๐dom DProd ๐ โ โจ๐, ๐ โฉ โ dom DProd ) |
19 | | fvex 6904 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ๐) โ V |
20 | 19 | rgenw 3065 |
. . . . . . . . . . . . . . . 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 7226 |
. . . . . . . . . . . . . 14
โข (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
24 | 23 | rnex 7902 |
. . . . . . . . . . . . 13
โข ran
(๐ โ {โ โ X๐ โ
dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
25 | 24 | rgen2w 3066 |
. . . . . . . . . . . 12
โข
โ๐ โ Grp
โ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐)) โ V |
26 | | df-dprd 19864 |
. . . . . . . . . . . . 13
โข DProd =
(๐ โ Grp, ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))} โฆ ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp (0gโ๐)} โฆ (๐ ฮฃg ๐))) |
27 | 26 | fmpox 8052 |
. . . . . . . . . . . 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 6729 |
. . . . . . . . . 10
โข dom DProd
= โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))}) |
30 | 29 | eleq2i 2825 |
. . . . . . . . 9
โข
(โจ๐, ๐ โฉ โ dom DProd โ
โจ๐, ๐ โฉ โ โช ๐ โ Grp ({๐} ร {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})) |
31 | | opeliunxp 5743 |
. . . . . . . . 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 296 |
. . . . . . . 8
โข (๐dom DProd ๐ โ (๐ โ Grp โง ๐ โ {โ โฃ (โ:dom โโถ(SubGrpโ๐) โง โ๐ โ dom โ(โ๐ฆ โ (dom โ โ {๐})(โโ๐) โ ((Cntzโ๐)โ(โโ๐ฆ)) โง ((โโ๐) โฉ ((mrClsโ(SubGrpโ๐))โโช (โ
โ (dom โ โ
{๐})))) =
{(0gโ๐)}))})) |
33 | 26 | ovmpt4g 7554 |
. . . . . . . . 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 1450 |
. . . . . . . 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 3556 |
. . . . . 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 3792 |
. . . 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 485 |
. . . . . 6
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ ๐ = ๐) |
41 | 40 | breq2d 5160 |
. . . . 5
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐บdom DProd ๐ โ ๐บdom DProd ๐)) |
42 | 40 | oveq2d 7424 |
. . . . . 6
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐บ DProd ๐ ) = (๐บ DProd ๐)) |
43 | 40 | dmeqd 5905 |
. . . . . . . . . . . . 13
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ dom ๐ = dom ๐) |
44 | | simplr 767 |
. . . . . . . . . . . . 13
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ dom ๐ = ๐ผ) |
45 | 43, 44 | eqtrd 2772 |
. . . . . . . . . . . 12
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ dom ๐ = ๐ผ) |
46 | 45 | ixpeq1d 8902 |
. . . . . . . . . . 11
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ X๐ โ dom ๐ (๐ โ๐) = X๐ โ ๐ผ (๐ โ๐)) |
47 | 40 | fveq1d 6893 |
. . . . . . . . . . . 12
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐ โ๐) = (๐โ๐)) |
48 | 47 | ixpeq2dv 8906 |
. . . . . . . . . . 11
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ X๐ โ ๐ผ (๐ โ๐) = X๐ โ ๐ผ (๐โ๐)) |
49 | 46, 48 | eqtrd 2772 |
. . . . . . . . . 10
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ X๐ โ dom ๐ (๐ โ๐) = X๐ โ ๐ผ (๐โ๐)) |
50 | 49 | rabeqdv 3447 |
. . . . . . . . 9
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } = {โ โ X๐ โ ๐ผ (๐โ๐) โฃ โ finSupp 0 }) |
51 | | dprdval.w |
. . . . . . . . 9
โข ๐ = {โ โ X๐ โ ๐ผ (๐โ๐) โฃ โ finSupp 0 } |
52 | 50, 51 | eqtr4di 2790 |
. . . . . . . 8
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } = ๐) |
53 | | eqidd 2733 |
. . . . . . . 8
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐บ ฮฃg ๐) = (๐บ ฮฃg ๐)) |
54 | 52, 53 | mpteq12dv 5239 |
. . . . . . 7
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)) = (๐ โ ๐ โฆ (๐บ ฮฃg ๐))) |
55 | 54 | rneqd 5937 |
. . . . . 6
โข (((๐บdom DProd ๐ โง dom ๐ = ๐ผ) โง ๐ = ๐) โ ran (๐ โ {โ โ X๐ โ dom ๐ (๐ โ๐) โฃ โ finSupp 0 } โฆ (๐บ ฮฃg
๐)) = ran (๐ โ ๐ โฆ (๐บ ฮฃg ๐))) |
56 | 42, 55 | eqeq12d 2748 |
. . . . 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 3822 |
. . 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 ๐))) |