Step | Hyp | Ref
| Expression |
1 | | dmdprdsplitlem.5 |
. . . . 5
β’ (π β (πΊ Ξ£g πΉ) β (πΊ DProd (π βΎ π΄))) |
2 | | dmdprdsplitlem.1 |
. . . . . . . 8
β’ (π β πΊdom DProd π) |
3 | | dmdprdsplitlem.2 |
. . . . . . . 8
β’ (π β dom π = πΌ) |
4 | 2, 3 | dprdf2 19794 |
. . . . . . 7
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
5 | | dmdprdsplitlem.3 |
. . . . . . 7
β’ (π β π΄ β πΌ) |
6 | 4, 5 | fssresd 6713 |
. . . . . 6
β’ (π β (π βΎ π΄):π΄βΆ(SubGrpβπΊ)) |
7 | | fdm 6681 |
. . . . . 6
β’ ((π βΎ π΄):π΄βΆ(SubGrpβπΊ) β dom (π βΎ π΄) = π΄) |
8 | | dmdprdsplitlem.0 |
. . . . . . 7
β’ 0 =
(0gβπΊ) |
9 | | eqid 2733 |
. . . . . . 7
β’ {β β Xπ β
π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } = {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } |
10 | 8, 9 | eldprd 19791 |
. . . . . 6
β’ (dom
(π βΎ π΄) = π΄ β ((πΊ Ξ£g πΉ) β (πΊ DProd (π βΎ π΄)) β (πΊdom DProd (π βΎ π΄) β§ βπ β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } (πΊ Ξ£g πΉ) = (πΊ Ξ£g π)))) |
11 | 6, 7, 10 | 3syl 18 |
. . . . 5
β’ (π β ((πΊ Ξ£g πΉ) β (πΊ DProd (π βΎ π΄)) β (πΊdom DProd (π βΎ π΄) β§ βπ β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } (πΊ Ξ£g πΉ) = (πΊ Ξ£g π)))) |
12 | 1, 11 | mpbid 231 |
. . . 4
β’ (π β (πΊdom DProd (π βΎ π΄) β§ βπ β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) |
13 | 12 | simprd 497 |
. . 3
β’ (π β βπ β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } (πΊ Ξ£g πΉ) = (πΊ Ξ£g π)) |
14 | 13 | adantr 482 |
. 2
β’ ((π β§ π β (πΌ β π΄)) β βπ β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } (πΊ Ξ£g πΉ) = (πΊ Ξ£g π)) |
15 | | simprr 772 |
. . . . . 6
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (πΊ Ξ£g πΉ) = (πΊ Ξ£g π)) |
16 | 12 | simpld 496 |
. . . . . . . . . . 11
β’ (π β πΊdom DProd (π βΎ π΄)) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β πΊdom DProd (π βΎ π΄)) |
18 | 6, 7 | syl 17 |
. . . . . . . . . . 11
β’ (π β dom (π βΎ π΄) = π΄) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β dom (π βΎ π΄) = π΄) |
20 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 }) |
21 | | eqid 2733 |
. . . . . . . . . 10
β’
(BaseβπΊ) =
(BaseβπΊ) |
22 | 9, 17, 19, 20, 21 | dprdff 19799 |
. . . . . . . . 9
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π:π΄βΆ(BaseβπΊ)) |
23 | 22 | feqmptd 6914 |
. . . . . . . 8
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π = (π β π΄ β¦ (πβπ))) |
24 | 5 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π΄ β πΌ) |
25 | 24 | resmptd 5998 |
. . . . . . . . 9
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) βΎ π΄) = (π β π΄ β¦ if(π β π΄, (πβπ), 0 ))) |
26 | | iftrue 4496 |
. . . . . . . . . 10
β’ (π β π΄ β if(π β π΄, (πβπ), 0 ) = (πβπ)) |
27 | 26 | mpteq2ia 5212 |
. . . . . . . . 9
β’ (π β π΄ β¦ if(π β π΄, (πβπ), 0 )) = (π β π΄ β¦ (πβπ)) |
28 | 25, 27 | eqtrdi 2789 |
. . . . . . . 8
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) βΎ π΄) = (π β π΄ β¦ (πβπ))) |
29 | 23, 28 | eqtr4d 2776 |
. . . . . . 7
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π = ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) βΎ π΄)) |
30 | 29 | oveq2d 7377 |
. . . . . 6
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (πΊ Ξ£g π) = (πΊ Ξ£g ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) βΎ π΄))) |
31 | | eqid 2733 |
. . . . . . 7
β’
(CntzβπΊ) =
(CntzβπΊ) |
32 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β πΊdom DProd π) |
33 | | dprdgrp 19792 |
. . . . . . . 8
β’ (πΊdom DProd π β πΊ β Grp) |
34 | | grpmnd 18763 |
. . . . . . . 8
β’ (πΊ β Grp β πΊ β Mnd) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . 7
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β πΊ β Mnd) |
36 | 2, 3 | dprddomcld 19788 |
. . . . . . . 8
β’ (π β πΌ β V) |
37 | 36 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β πΌ β V) |
38 | | dmdprdsplitlem.w |
. . . . . . . 8
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } |
39 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β dom π = πΌ) |
40 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β πΊdom DProd (π βΎ π΄)) |
41 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β dom (π βΎ π΄) = π΄) |
42 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 }) |
43 | 9, 40, 41, 42 | dprdfcl 19800 |
. . . . . . . . . . 11
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β§ π β π΄) β (πβπ) β ((π βΎ π΄)βπ)) |
44 | | fvres 6865 |
. . . . . . . . . . . 12
β’ (π β π΄ β ((π βΎ π΄)βπ) = (πβπ)) |
45 | 44 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β§ π β π΄) β ((π βΎ π΄)βπ) = (πβπ)) |
46 | 43, 45 | eleqtrd 2836 |
. . . . . . . . . 10
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β§ π β π΄) β (πβπ) β (πβπ)) |
47 | 4 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π:πΌβΆ(SubGrpβπΊ)) |
48 | 47 | ffvelcdmda 7039 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β (πβπ) β (SubGrpβπΊ)) |
49 | 8 | subg0cl 18944 |
. . . . . . . . . . . 12
β’ ((πβπ) β (SubGrpβπΊ) β 0 β (πβπ)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β 0 β (πβπ)) |
51 | 50 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β§ Β¬ π β π΄) β 0 β (πβπ)) |
52 | 46, 51 | ifclda 4525 |
. . . . . . . . 9
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β πΌ) β if(π β π΄, (πβπ), 0 ) β (πβπ)) |
53 | 36 | mptexd 7178 |
. . . . . . . . . . 11
β’ (π β (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) β
V) |
54 | 53 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) β
V) |
55 | | funmpt 6543 |
. . . . . . . . . . 11
β’ Fun
(π β πΌ β¦ if(π β π΄, (πβπ), 0 )) |
56 | 55 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β Fun (π β πΌ β¦ if(π β π΄, (πβπ), 0 ))) |
57 | 9, 17, 19, 20 | dprdffsupp 19801 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π finSupp 0 ) |
58 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β§ π β π΄) β π β π΄) |
59 | | eldifn 4091 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΌ β (π supp 0 )) β Β¬ π β (π supp 0 )) |
60 | 59 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β§ π β π΄) β Β¬ π β (π supp 0 )) |
61 | 58, 60 | eldifd 3925 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β§ π β π΄) β π β (π΄ β (π supp 0 ))) |
62 | | ssidd 3971 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (π supp 0 ) β (π supp 0 )) |
63 | 36, 5 | ssexd 5285 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β V) |
64 | 63 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π΄ β V) |
65 | 8 | fvexi 6860 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β 0 β V) |
67 | 22, 62, 64, 66 | suppssr 8131 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (π΄ β (π supp 0 ))) β (πβπ) = 0 ) |
68 | 67 | adantlr 714 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β§ π β (π΄ β (π supp 0 ))) β (πβπ) = 0 ) |
69 | 61, 68 | syldan 592 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β§ π β π΄) β (πβπ) = 0 ) |
70 | 69 | ifeq1da 4521 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β if(π β π΄, (πβπ), 0 ) = if(π β π΄, 0 , 0 )) |
71 | | ifid 4530 |
. . . . . . . . . . . 12
β’ if(π β π΄, 0 , 0 ) = 0 |
72 | 70, 71 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β (π supp 0 ))) β if(π β π΄, (πβπ), 0 ) = 0 ) |
73 | 72, 37 | suppss2 8135 |
. . . . . . . . . 10
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) supp 0 ) β (π supp 0 )) |
74 | | fsuppsssupp 9329 |
. . . . . . . . . 10
β’ ((((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) β V β§ Fun
(π β πΌ β¦ if(π β π΄, (πβπ), 0 ))) β§ (π finSupp 0 β§ ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) supp 0 ) β (π supp 0 ))) β (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) finSupp 0
) |
75 | 54, 56, 57, 73, 74 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) finSupp 0
) |
76 | 38, 32, 39, 52, 75 | dprdwd 19798 |
. . . . . . . 8
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) β π) |
77 | 38, 32, 39, 76, 21 | dprdff 19799 |
. . . . . . 7
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (π β πΌ β¦ if(π β π΄, (πβπ), 0 )):πΌβΆ(BaseβπΊ)) |
78 | 38, 32, 39, 76, 31 | dprdfcntz 19802 |
. . . . . . 7
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ran (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) β
((CntzβπΊ)βran
(π β πΌ β¦ if(π β π΄, (πβπ), 0 )))) |
79 | | eldifn 4091 |
. . . . . . . . . 10
β’ (π β (πΌ β π΄) β Β¬ π β π΄) |
80 | 79 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β π΄)) β Β¬ π β π΄) |
81 | 80 | iffalsed 4501 |
. . . . . . . 8
β’ ((((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β§ π β (πΌ β π΄)) β if(π β π΄, (πβπ), 0 ) = 0 ) |
82 | 81, 37 | suppss2 8135 |
. . . . . . 7
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) supp 0 ) β π΄) |
83 | 21, 8, 31, 35, 37, 77, 78, 82, 75 | gsumzres 19694 |
. . . . . 6
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (πΊ Ξ£g ((π β πΌ β¦ if(π β π΄, (πβπ), 0 )) βΎ π΄)) = (πΊ Ξ£g (π β πΌ β¦ if(π β π΄, (πβπ), 0 )))) |
84 | 15, 30, 83 | 3eqtrd 2777 |
. . . . 5
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π β πΌ β¦ if(π β π΄, (πβπ), 0 )))) |
85 | | dmdprdsplitlem.4 |
. . . . . . 7
β’ (π β πΉ β π) |
86 | 85 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β πΉ β π) |
87 | 8, 38, 32, 39, 86, 76 | dprdf11 19810 |
. . . . 5
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ((πΊ Ξ£g πΉ) = (πΊ Ξ£g (π β πΌ β¦ if(π β π΄, (πβπ), 0 ))) β πΉ = (π β πΌ β¦ if(π β π΄, (πβπ), 0 )))) |
88 | 84, 87 | mpbid 231 |
. . . 4
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β πΉ = (π β πΌ β¦ if(π β π΄, (πβπ), 0 ))) |
89 | 88 | fveq1d 6848 |
. . 3
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (πΉβπ) = ((π β πΌ β¦ if(π β π΄, (πβπ), 0 ))βπ)) |
90 | | eldifi 4090 |
. . . . 5
β’ (π β (πΌ β π΄) β π β πΌ) |
91 | 90 | ad2antlr 726 |
. . . 4
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β π β πΌ) |
92 | | eleq1 2822 |
. . . . . 6
β’ (π = π β (π β π΄ β π β π΄)) |
93 | | fveq2 6846 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
94 | 92, 93 | ifbieq1d 4514 |
. . . . 5
β’ (π = π β if(π β π΄, (πβπ), 0 ) = if(π β π΄, (πβπ), 0 )) |
95 | | eqid 2733 |
. . . . 5
β’ (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) = (π β πΌ β¦ if(π β π΄, (πβπ), 0 )) |
96 | | fvex 6859 |
. . . . . 6
β’ (πβπ) β V |
97 | 96, 65 | ifex 4540 |
. . . . 5
β’ if(π β π΄, (πβπ), 0 ) β
V |
98 | 94, 95, 97 | fvmpt3i 6957 |
. . . 4
β’ (π β πΌ β ((π β πΌ β¦ if(π β π΄, (πβπ), 0 ))βπ) = if(π β π΄, (πβπ), 0 )) |
99 | 91, 98 | syl 17 |
. . 3
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β ((π β πΌ β¦ if(π β π΄, (πβπ), 0 ))βπ) = if(π β π΄, (πβπ), 0 )) |
100 | | eldifn 4091 |
. . . . 5
β’ (π β (πΌ β π΄) β Β¬ π β π΄) |
101 | 100 | ad2antlr 726 |
. . . 4
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β Β¬ π β π΄) |
102 | 101 | iffalsed 4501 |
. . 3
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β if(π β π΄, (πβπ), 0 ) = 0 ) |
103 | 89, 99, 102 | 3eqtrd 2777 |
. 2
β’ (((π β§ π β (πΌ β π΄)) β§ (π β {β β Xπ β π΄ ((π βΎ π΄)βπ) β£ β finSupp 0 } β§ (πΊ Ξ£g πΉ) = (πΊ Ξ£g π))) β (πΉβπ) = 0 ) |
104 | 14, 103 | rexlimddv 3155 |
1
β’ ((π β§ π β (πΌ β π΄)) β (πΉβπ) = 0 ) |