Step | Hyp | Ref
| Expression |
1 | | eldprdi.1 |
. . . . . 6
β’ (π β πΊdom DProd π) |
2 | | dprdgrp 19869 |
. . . . . 6
β’ (πΊdom DProd π β πΊ β Grp) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β πΊ β Grp) |
4 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
5 | | dprdfinv.b |
. . . . . 6
β’ π = (invgβπΊ) |
6 | 4, 5 | grpinvf 18867 |
. . . . 5
β’ (πΊ β Grp β π:(BaseβπΊ)βΆ(BaseβπΊ)) |
7 | 3, 6 | syl 17 |
. . . 4
β’ (π β π:(BaseβπΊ)βΆ(BaseβπΊ)) |
8 | | eldprdi.w |
. . . . 5
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } |
9 | | eldprdi.2 |
. . . . 5
β’ (π β dom π = πΌ) |
10 | | eldprdi.3 |
. . . . 5
β’ (π β πΉ β π) |
11 | 8, 1, 9, 10, 4 | dprdff 19876 |
. . . 4
β’ (π β πΉ:πΌβΆ(BaseβπΊ)) |
12 | | fcompt 7127 |
. . . 4
β’ ((π:(BaseβπΊ)βΆ(BaseβπΊ) β§ πΉ:πΌβΆ(BaseβπΊ)) β (π β πΉ) = (π₯ β πΌ β¦ (πβ(πΉβπ₯)))) |
13 | 7, 11, 12 | syl2anc 584 |
. . 3
β’ (π β (π β πΉ) = (π₯ β πΌ β¦ (πβ(πΉβπ₯)))) |
14 | 1, 9 | dprdf2 19871 |
. . . . . 6
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
15 | 14 | ffvelcdmda 7083 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β (SubGrpβπΊ)) |
16 | 8, 1, 9, 10 | dprdfcl 19877 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯) β (πβπ₯)) |
17 | 5 | subginvcl 19009 |
. . . . 5
β’ (((πβπ₯) β (SubGrpβπΊ) β§ (πΉβπ₯) β (πβπ₯)) β (πβ(πΉβπ₯)) β (πβπ₯)) |
18 | 15, 16, 17 | syl2anc 584 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (πβ(πΉβπ₯)) β (πβπ₯)) |
19 | 1, 9 | dprddomcld 19865 |
. . . . . 6
β’ (π β πΌ β V) |
20 | 19 | mptexd 7222 |
. . . . 5
β’ (π β (π₯ β πΌ β¦ (πβ(πΉβπ₯))) β V) |
21 | | funmpt 6583 |
. . . . . 6
β’ Fun
(π₯ β πΌ β¦ (πβ(πΉβπ₯))) |
22 | 21 | a1i 11 |
. . . . 5
β’ (π β Fun (π₯ β πΌ β¦ (πβ(πΉβπ₯)))) |
23 | 8, 1, 9, 10 | dprdffsupp 19878 |
. . . . 5
β’ (π β πΉ finSupp 0 ) |
24 | | ssidd 4004 |
. . . . . . . . 9
β’ (π β (πΉ supp 0 ) β (πΉ supp 0 )) |
25 | | eldprdi.0 |
. . . . . . . . . . 11
β’ 0 =
(0gβπΊ) |
26 | 25 | fvexi 6902 |
. . . . . . . . . 10
β’ 0 β
V |
27 | 26 | a1i 11 |
. . . . . . . . 9
β’ (π β 0 β V) |
28 | 11, 24, 19, 27 | suppssr 8177 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β (πΉ supp 0 ))) β (πΉβπ₯) = 0 ) |
29 | 28 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β (πΉ supp 0 ))) β (πβ(πΉβπ₯)) = (πβ 0 )) |
30 | 25, 5 | grpinvid 18880 |
. . . . . . . . 9
β’ (πΊ β Grp β (πβ 0 ) = 0 ) |
31 | 3, 30 | syl 17 |
. . . . . . . 8
β’ (π β (πβ 0 ) = 0 ) |
32 | 31 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β (πΉ supp 0 ))) β (πβ 0 ) = 0 ) |
33 | 29, 32 | eqtrd 2772 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β (πΉ supp 0 ))) β (πβ(πΉβπ₯)) = 0 ) |
34 | 33, 19 | suppss2 8181 |
. . . . 5
β’ (π β ((π₯ β πΌ β¦ (πβ(πΉβπ₯))) supp 0 ) β (πΉ supp 0 )) |
35 | | fsuppsssupp 9375 |
. . . . 5
β’ ((((π₯ β πΌ β¦ (πβ(πΉβπ₯))) β V β§ Fun (π₯ β πΌ β¦ (πβ(πΉβπ₯)))) β§ (πΉ finSupp 0 β§ ((π₯ β πΌ β¦ (πβ(πΉβπ₯))) supp 0 ) β (πΉ supp 0 ))) β (π₯ β πΌ β¦ (πβ(πΉβπ₯))) finSupp 0 ) |
36 | 20, 22, 23, 34, 35 | syl22anc 837 |
. . . 4
β’ (π β (π₯ β πΌ β¦ (πβ(πΉβπ₯))) finSupp 0 ) |
37 | 8, 1, 9, 18, 36 | dprdwd 19875 |
. . 3
β’ (π β (π₯ β πΌ β¦ (πβ(πΉβπ₯))) β π) |
38 | 13, 37 | eqeltrd 2833 |
. 2
β’ (π β (π β πΉ) β π) |
39 | | eqid 2732 |
. . 3
β’
(CntzβπΊ) =
(CntzβπΊ) |
40 | 8, 1, 9, 10, 39 | dprdfcntz 19879 |
. . 3
β’ (π β ran πΉ β ((CntzβπΊ)βran πΉ)) |
41 | 4, 25, 39, 5, 3, 19, 11, 40, 23 | gsumzinv 19807 |
. 2
β’ (π β (πΊ Ξ£g (π β πΉ)) = (πβ(πΊ Ξ£g πΉ))) |
42 | 38, 41 | jca 512 |
1
β’ (π β ((π β πΉ) β π β§ (πΊ Ξ£g (π β πΉ)) = (πβ(πΊ Ξ£g πΉ)))) |