Step | Hyp | Ref
| Expression |
1 | | dpjidcl.3 |
. . . 4
β’ (π β π΄ β (πΊ DProd π)) |
2 | | dpjfval.2 |
. . . . 5
β’ (π β dom π = πΌ) |
3 | | dpjidcl.0 |
. . . . . 6
β’ 0 =
(0gβπΊ) |
4 | | dpjidcl.w |
. . . . . 6
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } |
5 | 3, 4 | eldprd 19791 |
. . . . 5
β’ (dom
π = πΌ β (π΄ β (πΊ DProd π) β (πΊdom DProd π β§ βπ β π π΄ = (πΊ Ξ£g π)))) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (π β (π΄ β (πΊ DProd π) β (πΊdom DProd π β§ βπ β π π΄ = (πΊ Ξ£g π)))) |
7 | 1, 6 | mpbid 231 |
. . 3
β’ (π β (πΊdom DProd π β§ βπ β π π΄ = (πΊ Ξ£g π))) |
8 | 7 | simprd 497 |
. 2
β’ (π β βπ β π π΄ = (πΊ Ξ£g π)) |
9 | | dpjfval.1 |
. . . . 5
β’ (π β πΊdom DProd π) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β πΊdom DProd π) |
11 | 2 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β dom π = πΌ) |
12 | 9 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β πΊdom DProd π) |
13 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β dom π = πΌ) |
14 | | dpjfval.p |
. . . . . 6
β’ π = (πΊdProjπ) |
15 | | simpr 486 |
. . . . . 6
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π₯ β πΌ) |
16 | 12, 13, 14, 15 | dpjf 19844 |
. . . . 5
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πβπ₯):(πΊ DProd π)βΆ(πβπ₯)) |
17 | 1 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π΄ β (πΊ DProd π)) |
18 | 16, 17 | ffvelcdmd 7040 |
. . . 4
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((πβπ₯)βπ΄) β (πβπ₯)) |
19 | 9, 2 | dprddomcld 19788 |
. . . . . . 7
β’ (π β πΌ β V) |
20 | 19 | mptexd 7178 |
. . . . . 6
β’ (π β (π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β V) |
21 | 20 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β (π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β V) |
22 | | funmpt 6543 |
. . . . . 6
β’ Fun
(π₯ β πΌ β¦ ((πβπ₯)βπ΄)) |
23 | 22 | a1i 11 |
. . . . 5
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β Fun (π₯ β πΌ β¦ ((πβπ₯)βπ΄))) |
24 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π β π) |
25 | 4, 10, 11, 24 | dprdffsupp 19801 |
. . . . 5
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π finSupp 0 ) |
26 | | eldifi 4090 |
. . . . . . . 8
β’ (π₯ β (πΌ β (π supp 0 )) β π₯ β πΌ) |
27 | | eqid 2733 |
. . . . . . . . . 10
β’
(proj1βπΊ) = (proj1βπΊ) |
28 | 12, 13, 14, 27, 15 | dpjval 19843 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πβπ₯) = ((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))) |
29 | 28 | fveq1d 6848 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((πβπ₯)βπ΄) = (((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄)) |
30 | 26, 29 | sylan2 594 |
. . . . . . 7
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β ((πβπ₯)βπ΄) = (((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄)) |
31 | | simplrr 777 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β π΄ = (πΊ Ξ£g π)) |
32 | | eqid 2733 |
. . . . . . . . . . 11
β’
(BaseβπΊ) =
(BaseβπΊ) |
33 | | eqid 2733 |
. . . . . . . . . . 11
β’
(CntzβπΊ) =
(CntzβπΊ) |
34 | | dprdgrp 19792 |
. . . . . . . . . . . . 13
β’ (πΊdom DProd π β πΊ β Grp) |
35 | | grpmnd 18763 |
. . . . . . . . . . . . 13
β’ (πΊ β Grp β πΊ β Mnd) |
36 | 10, 34, 35 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β πΊ β Mnd) |
37 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β πΊ β Mnd) |
38 | 19 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β πΌ β V) |
39 | 4, 10, 11, 24, 32 | dprdff 19799 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π:πΌβΆ(BaseβπΊ)) |
40 | 39 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β π:πΌβΆ(BaseβπΊ)) |
41 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π β π) |
42 | 4, 12, 13, 41, 33 | dprdfcntz 19802 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ran π β ((CntzβπΊ)βran π)) |
43 | 26, 42 | sylan2 594 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β ran π β ((CntzβπΊ)βran π)) |
44 | | snssi 4772 |
. . . . . . . . . . . . 13
β’ (π₯ β (πΌ β (π supp 0 )) β {π₯} β (πΌ β (π supp 0 ))) |
45 | 44 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β {π₯} β (πΌ β (π supp 0 ))) |
46 | 45 | difss2d 4098 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β {π₯} β πΌ) |
47 | | suppssdm 8112 |
. . . . . . . . . . . . . . 15
β’ (π supp 0 ) β dom π |
48 | 47, 39 | fssdm 6692 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β (π supp 0 ) β πΌ) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β (π supp 0 ) β πΌ) |
50 | | ssconb 4101 |
. . . . . . . . . . . . 13
β’ (({π₯} β πΌ β§ (π supp 0 ) β πΌ) β ({π₯} β (πΌ β (π supp 0 )) β (π supp 0 ) β (πΌ β {π₯}))) |
51 | 46, 49, 50 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β ({π₯} β (πΌ β (π supp 0 )) β (π supp 0 ) β (πΌ β {π₯}))) |
52 | 45, 51 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β (π supp 0 ) β (πΌ β {π₯})) |
53 | 25 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β π finSupp 0 ) |
54 | 32, 3, 33, 37, 38, 40, 43, 52, 53 | gsumzres 19694 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β (πΊ Ξ£g
(π βΎ (πΌ β {π₯}))) = (πΊ Ξ£g π)) |
55 | 31, 54 | eqtr4d 2776 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β π΄ = (πΊ Ξ£g (π βΎ (πΌ β {π₯})))) |
56 | | eqid 2733 |
. . . . . . . . . . 11
β’ {β β Xπ β
(πΌ β {π₯})((π βΎ (πΌ β {π₯}))βπ) β£ β finSupp 0 } = {β β Xπ β (πΌ β {π₯})((π βΎ (πΌ β {π₯}))βπ) β£ β finSupp 0 } |
57 | | difss 4095 |
. . . . . . . . . . . . . 14
β’ (πΌ β {π₯}) β πΌ |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΌ β {π₯}) β πΌ) |
59 | 12, 13, 58 | dprdres 19815 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊdom DProd (π βΎ (πΌ β {π₯})) β§ (πΊ DProd (π βΎ (πΌ β {π₯}))) β (πΊ DProd π))) |
60 | 59 | simpld 496 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β πΊdom DProd (π βΎ (πΌ β {π₯}))) |
61 | 12, 13 | dprdf2 19794 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π:πΌβΆ(SubGrpβπΊ)) |
62 | | fssres 6712 |
. . . . . . . . . . . . 13
β’ ((π:πΌβΆ(SubGrpβπΊ) β§ (πΌ β {π₯}) β πΌ) β (π βΎ (πΌ β {π₯})):(πΌ β {π₯})βΆ(SubGrpβπΊ)) |
63 | 61, 57, 62 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π βΎ (πΌ β {π₯})):(πΌ β {π₯})βΆ(SubGrpβπΊ)) |
64 | 63 | fdmd 6683 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β dom (π βΎ (πΌ β {π₯})) = (πΌ β {π₯})) |
65 | 39 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π:πΌβΆ(BaseβπΊ)) |
66 | 65 | feqmptd 6914 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π = (π β πΌ β¦ (πβπ))) |
67 | 66 | reseq1d 5940 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π βΎ (πΌ β {π₯})) = ((π β πΌ β¦ (πβπ)) βΎ (πΌ β {π₯}))) |
68 | | resmpt 5995 |
. . . . . . . . . . . . . 14
β’ ((πΌ β {π₯}) β πΌ β ((π β πΌ β¦ (πβπ)) βΎ (πΌ β {π₯})) = (π β (πΌ β {π₯}) β¦ (πβπ))) |
69 | 57, 68 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ ((π β πΌ β¦ (πβπ)) βΎ (πΌ β {π₯})) = (π β (πΌ β {π₯}) β¦ (πβπ)) |
70 | 67, 69 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π βΎ (πΌ β {π₯})) = (π β (πΌ β {π₯}) β¦ (πβπ))) |
71 | | eldifi 4090 |
. . . . . . . . . . . . . . 15
β’ (π β (πΌ β {π₯}) β π β πΌ) |
72 | 4, 12, 13, 41 | dprdfcl 19800 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π β πΌ) β (πβπ) β (πβπ)) |
73 | 71, 72 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π β (πΌ β {π₯})) β (πβπ) β (πβπ)) |
74 | | fvres 6865 |
. . . . . . . . . . . . . . 15
β’ (π β (πΌ β {π₯}) β ((π βΎ (πΌ β {π₯}))βπ) = (πβπ)) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π β (πΌ β {π₯})) β ((π βΎ (πΌ β {π₯}))βπ) = (πβπ)) |
76 | 73, 75 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π β (πΌ β {π₯})) β (πβπ) β ((π βΎ (πΌ β {π₯}))βπ)) |
77 | 19 | difexd 5290 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΌ β {π₯}) β V) |
78 | 77 | mptexd 7178 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (πΌ β {π₯}) β¦ (πβπ)) β V) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π β (πΌ β {π₯}) β¦ (πβπ)) β V) |
80 | | funmpt 6543 |
. . . . . . . . . . . . . . 15
β’ Fun
(π β (πΌ β {π₯}) β¦ (πβπ)) |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β Fun (π β (πΌ β {π₯}) β¦ (πβπ))) |
82 | 25 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π finSupp 0 ) |
83 | | ssdif 4103 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β {π₯}) β πΌ β ((πΌ β {π₯}) β (π supp 0 )) β (πΌ β (π supp 0 ))) |
84 | 57, 83 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β {π₯}) β (π supp 0 )) β (πΌ β (π supp 0 )) |
85 | 84 | sseli 3944 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΌ β {π₯}) β (π supp 0 )) β π β (πΌ β (π supp 0 ))) |
86 | | ssidd 3971 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π supp 0 ) β (π supp 0 )) |
87 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β πΌ β V) |
88 | 3 | fvexi 6860 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
V |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β 0 β V) |
90 | 65, 86, 87, 89 | suppssr 8131 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π β (πΌ β (π supp 0 ))) β (πβπ) = 0 ) |
91 | 85, 90 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π β ((πΌ β {π₯}) β (π supp 0 ))) β (πβπ) = 0 ) |
92 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΌ β {π₯}) β V) |
93 | 91, 92 | suppss2 8135 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((π β (πΌ β {π₯}) β¦ (πβπ)) supp 0 ) β (π supp 0 )) |
94 | | fsuppsssupp 9329 |
. . . . . . . . . . . . . 14
β’ ((((π β (πΌ β {π₯}) β¦ (πβπ)) β V β§ Fun (π β (πΌ β {π₯}) β¦ (πβπ))) β§ (π finSupp 0 β§ ((π β (πΌ β {π₯}) β¦ (πβπ)) supp 0 ) β (π supp 0 ))) β (π β (πΌ β {π₯}) β¦ (πβπ)) finSupp 0 ) |
95 | 79, 81, 82, 93, 94 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π β (πΌ β {π₯}) β¦ (πβπ)) finSupp 0 ) |
96 | 56, 60, 64, 76, 95 | dprdwd 19798 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π β (πΌ β {π₯}) β¦ (πβπ)) β {β β Xπ β (πΌ β {π₯})((π βΎ (πΌ β {π₯}))βπ) β£ β finSupp 0 }) |
97 | 70, 96 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π βΎ (πΌ β {π₯})) β {β β Xπ β (πΌ β {π₯})((π βΎ (πΌ β {π₯}))βπ) β£ β finSupp 0 }) |
98 | 3, 56, 60, 64, 97 | eldprdi 19805 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ Ξ£g (π βΎ (πΌ β {π₯}))) β (πΊ DProd (π βΎ (πΌ β {π₯})))) |
99 | 26, 98 | sylan2 594 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β (πΊ Ξ£g
(π βΎ (πΌ β {π₯}))) β (πΊ DProd (π βΎ (πΌ β {π₯})))) |
100 | 55, 99 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β π΄ β (πΊ DProd (π βΎ (πΌ β {π₯})))) |
101 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
102 | | eqid 2733 |
. . . . . . . . . 10
β’
(LSSumβπΊ) =
(LSSumβπΊ) |
103 | 61, 15 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πβπ₯) β (SubGrpβπΊ)) |
104 | | dprdsubg 19811 |
. . . . . . . . . . 11
β’ (πΊdom DProd (π βΎ (πΌ β {π₯})) β (πΊ DProd (π βΎ (πΌ β {π₯}))) β (SubGrpβπΊ)) |
105 | 60, 104 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ DProd (π βΎ (πΌ β {π₯}))) β (SubGrpβπΊ)) |
106 | 12, 13, 15, 3 | dpjdisj 19840 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((πβπ₯) β© (πΊ DProd (π βΎ (πΌ β {π₯})))) = { 0 }) |
107 | 12, 13, 15, 33 | dpjcntz 19839 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πβπ₯) β ((CntzβπΊ)β(πΊ DProd (π βΎ (πΌ β {π₯}))))) |
108 | 101, 102,
3, 33, 103, 105, 106, 107, 27 | pj1rid 19492 |
. . . . . . . . 9
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β§ π΄ β (πΊ DProd (π βΎ (πΌ β {π₯})))) β (((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄) = 0 ) |
109 | 26, 108 | sylanl2 680 |
. . . . . . . 8
β’ ((((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β§ π΄ β (πΊ DProd (π βΎ (πΌ β {π₯})))) β (((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄) = 0 ) |
110 | 100, 109 | mpdan 686 |
. . . . . . 7
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β (((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄) = 0 ) |
111 | 30, 110 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β (πΌ β (π supp 0 ))) β ((πβπ₯)βπ΄) = 0 ) |
112 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β πΌ β V) |
113 | 111, 112 | suppss2 8135 |
. . . . 5
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β ((π₯ β πΌ β¦ ((πβπ₯)βπ΄)) supp 0 ) β (π supp 0 )) |
114 | | fsuppsssupp 9329 |
. . . . 5
β’ ((((π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β V β§ Fun (π₯ β πΌ β¦ ((πβπ₯)βπ΄))) β§ (π finSupp 0 β§ ((π₯ β πΌ β¦ ((πβπ₯)βπ΄)) supp 0 ) β (π supp 0 ))) β (π₯ β πΌ β¦ ((πβπ₯)βπ΄)) finSupp 0 ) |
115 | 21, 23, 25, 113, 114 | syl22anc 838 |
. . . 4
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β (π₯ β πΌ β¦ ((πβπ₯)βπ΄)) finSupp 0 ) |
116 | 4, 10, 11, 18, 115 | dprdwd 19798 |
. . 3
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β (π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β π) |
117 | | simprr 772 |
. . . 4
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π΄ = (πΊ Ξ£g π)) |
118 | 39 | feqmptd 6914 |
. . . . . 6
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π = (π₯ β πΌ β¦ (πβπ₯))) |
119 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π΄ = (πΊ Ξ£g π)) |
120 | 12, 34, 35 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β πΊ β Mnd) |
121 | 4, 12, 13, 41 | dprdffsupp 19801 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π finSupp 0 ) |
122 | | disjdif 4435 |
. . . . . . . . . . . . 13
β’ ({π₯} β© (πΌ β {π₯})) = β
|
123 | 122 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ({π₯} β© (πΌ β {π₯})) = β
) |
124 | | undif2 4440 |
. . . . . . . . . . . . 13
β’ ({π₯} βͺ (πΌ β {π₯})) = ({π₯} βͺ πΌ) |
125 | 15 | snssd 4773 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β {π₯} β πΌ) |
126 | | ssequn1 4144 |
. . . . . . . . . . . . . 14
β’ ({π₯} β πΌ β ({π₯} βͺ πΌ) = πΌ) |
127 | 125, 126 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ({π₯} βͺ πΌ) = πΌ) |
128 | 124, 127 | eqtr2id 2786 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β πΌ = ({π₯} βͺ (πΌ β {π₯}))) |
129 | 32, 3, 101, 33, 120, 87, 65, 42, 121, 123, 128 | gsumzsplit 19712 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ Ξ£g π) = ((πΊ Ξ£g (π βΎ {π₯}))(+gβπΊ)(πΊ Ξ£g (π βΎ (πΌ β {π₯}))))) |
130 | 65, 125 | feqresmpt 6915 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π βΎ {π₯}) = (π β {π₯} β¦ (πβπ))) |
131 | 130 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ Ξ£g (π βΎ {π₯})) = (πΊ Ξ£g (π β {π₯} β¦ (πβπ)))) |
132 | 65, 15 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πβπ₯) β (BaseβπΊ)) |
133 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
134 | 32, 133 | gsumsn 19739 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Mnd β§ π₯ β πΌ β§ (πβπ₯) β (BaseβπΊ)) β (πΊ Ξ£g (π β {π₯} β¦ (πβπ))) = (πβπ₯)) |
135 | 120, 15, 132, 134 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ Ξ£g (π β {π₯} β¦ (πβπ))) = (πβπ₯)) |
136 | 131, 135 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ Ξ£g (π βΎ {π₯})) = (πβπ₯)) |
137 | 136 | oveq1d 7376 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((πΊ Ξ£g (π βΎ {π₯}))(+gβπΊ)(πΊ Ξ£g (π βΎ (πΌ β {π₯})))) = ((πβπ₯)(+gβπΊ)(πΊ Ξ£g (π βΎ (πΌ β {π₯}))))) |
138 | 119, 129,
137 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π΄ = ((πβπ₯)(+gβπΊ)(πΊ Ξ£g (π βΎ (πΌ β {π₯}))))) |
139 | 12, 13, 15, 102 | dpjlsm 19841 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πΊ DProd π) = ((πβπ₯)(LSSumβπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))) |
140 | 17, 139 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β π΄ β ((πβπ₯)(LSSumβπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))) |
141 | 4, 10, 11, 24 | dprdfcl 19800 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (πβπ₯) β (πβπ₯)) |
142 | 101, 102,
3, 33, 103, 105, 106, 107, 27, 140, 141, 98 | pj1eq 19490 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (π΄ = ((πβπ₯)(+gβπΊ)(πΊ Ξ£g (π βΎ (πΌ β {π₯})))) β ((((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄) = (πβπ₯) β§ (((πΊ DProd (π βΎ (πΌ β {π₯})))(proj1βπΊ)(πβπ₯))βπ΄) = (πΊ Ξ£g (π βΎ (πΌ β {π₯})))))) |
143 | 138, 142 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄) = (πβπ₯) β§ (((πΊ DProd (π βΎ (πΌ β {π₯})))(proj1βπΊ)(πβπ₯))βπ΄) = (πΊ Ξ£g (π βΎ (πΌ β {π₯}))))) |
144 | 143 | simpld 496 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β (((πβπ₯)(proj1βπΊ)(πΊ DProd (π βΎ (πΌ β {π₯}))))βπ΄) = (πβπ₯)) |
145 | 29, 144 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β§ π₯ β πΌ) β ((πβπ₯)βπ΄) = (πβπ₯)) |
146 | 145 | mpteq2dva 5209 |
. . . . . 6
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β (π₯ β πΌ β¦ ((πβπ₯)βπ΄)) = (π₯ β πΌ β¦ (πβπ₯))) |
147 | 118, 146 | eqtr4d 2776 |
. . . . 5
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π = (π₯ β πΌ β¦ ((πβπ₯)βπ΄))) |
148 | 147 | oveq2d 7377 |
. . . 4
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β (πΊ Ξ£g π) = (πΊ Ξ£g (π₯ β πΌ β¦ ((πβπ₯)βπ΄)))) |
149 | 117, 148 | eqtrd 2773 |
. . 3
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β π΄ = (πΊ Ξ£g (π₯ β πΌ β¦ ((πβπ₯)βπ΄)))) |
150 | 116, 149 | jca 513 |
. 2
β’ ((π β§ (π β π β§ π΄ = (πΊ Ξ£g π))) β ((π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β π β§ π΄ = (πΊ Ξ£g (π₯ β πΌ β¦ ((πβπ₯)βπ΄))))) |
151 | 8, 150 | rexlimddv 3155 |
1
β’ (π β ((π₯ β πΌ β¦ ((πβπ₯)βπ΄)) β π β§ π΄ = (πΊ Ξ£g (π₯ β πΌ β¦ ((πβπ₯)βπ΄))))) |