Step | Hyp | Ref
| Expression |
1 | | gsumzsplit.b |
. . 3
β’ π΅ = (BaseβπΊ) |
2 | | gsumzsplit.0 |
. . 3
β’ 0 =
(0gβπΊ) |
3 | | gsumzsplit.p |
. . 3
β’ + =
(+gβπΊ) |
4 | | gsumzsplit.z |
. . 3
β’ π = (CntzβπΊ) |
5 | | gsumzsplit.g |
. . 3
β’ (π β πΊ β Mnd) |
6 | | gsumzsplit.a |
. . 3
β’ (π β π΄ β π) |
7 | | gsumzsplit.f |
. . . 4
β’ (π β πΉ:π΄βΆπ΅) |
8 | 2 | fvexi 6860 |
. . . . 5
β’ 0 β
V |
9 | 8 | a1i 11 |
. . . 4
β’ (π β 0 β V) |
10 | | gsumzsplit.w |
. . . 4
β’ (π β πΉ finSupp 0 ) |
11 | 7, 6, 9, 10 | fsuppmptif 9343 |
. . 3
β’ (π β (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) finSupp 0
) |
12 | 7, 6, 9, 10 | fsuppmptif 9343 |
. . 3
β’ (π β (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) finSupp 0
) |
13 | 1 | submacs 18645 |
. . . . 5
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
14 | | acsmre 17540 |
. . . . 5
β’
((SubMndβπΊ)
β (ACSβπ΅) β
(SubMndβπΊ) β
(Mooreβπ΅)) |
15 | 5, 13, 14 | 3syl 18 |
. . . 4
β’ (π β (SubMndβπΊ) β (Mooreβπ΅)) |
16 | 7 | frnd 6680 |
. . . 4
β’ (π β ran πΉ β π΅) |
17 | | eqid 2733 |
. . . . 5
β’
(mrClsβ(SubMndβπΊ)) = (mrClsβ(SubMndβπΊ)) |
18 | 17 | mrccl 17499 |
. . . 4
β’
(((SubMndβπΊ)
β (Mooreβπ΅)
β§ ran πΉ β π΅) β
((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ)) |
19 | 15, 16, 18 | syl2anc 585 |
. . 3
β’ (π β
((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ)) |
20 | | gsumzsplit.c |
. . . . 5
β’ (π β ran πΉ β (πβran πΉ)) |
21 | | eqid 2733 |
. . . . . 6
β’ (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) = (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) |
22 | 4, 17, 21 | cntzspan 19630 |
. . . . 5
β’ ((πΊ β Mnd β§ ran πΉ β (πβran πΉ)) β (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd) |
23 | 5, 20, 22 | syl2anc 585 |
. . . 4
β’ (π β (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd) |
24 | 21, 4 | submcmn2 19625 |
. . . . 5
β’
(((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ) β ((πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd β
((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)))) |
25 | 19, 24 | syl 17 |
. . . 4
β’ (π β ((πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd β
((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)))) |
26 | 23, 25 | mpbid 231 |
. . 3
β’ (π β
((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ))) |
27 | 15, 17, 16 | mrcssidd 17513 |
. . . . . . 7
β’ (π β ran πΉ β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β ran πΉ β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
29 | 7 | ffnd 6673 |
. . . . . . 7
β’ (π β πΉ Fn π΄) |
30 | | fnfvelrn 7035 |
. . . . . . 7
β’ ((πΉ Fn π΄ β§ π β π΄) β (πΉβπ) β ran πΉ) |
31 | 29, 30 | sylan 581 |
. . . . . 6
β’ ((π β§ π β π΄) β (πΉβπ) β ran πΉ) |
32 | 28, 31 | sseldd 3949 |
. . . . 5
β’ ((π β§ π β π΄) β (πΉβπ) β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
33 | 2 | subm0cl 18630 |
. . . . . . 7
β’
(((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ) β 0 β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
34 | 19, 33 | syl 17 |
. . . . . 6
β’ (π β 0 β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
35 | 34 | adantr 482 |
. . . . 5
β’ ((π β§ π β π΄) β 0 β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
36 | 32, 35 | ifcld 4536 |
. . . 4
β’ ((π β§ π β π΄) β if(π β πΆ, (πΉβπ), 0 ) β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
37 | 36 | fmpttd 7067 |
. . 3
β’ (π β (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )):π΄βΆ((mrClsβ(SubMndβπΊ))βran πΉ)) |
38 | 32, 35 | ifcld 4536 |
. . . 4
β’ ((π β§ π β π΄) β if(π β π·, (πΉβπ), 0 ) β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
39 | 38 | fmpttd 7067 |
. . 3
β’ (π β (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )):π΄βΆ((mrClsβ(SubMndβπΊ))βran πΉ)) |
40 | 1, 2, 3, 4, 5, 6, 11, 12, 19, 26, 37, 39 | gsumzadd 19707 |
. 2
β’ (π β (πΊ Ξ£g ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βf
+ (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )))) = ((πΊ Ξ£g (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 ))) + (πΊ Ξ£g (π β π΄ β¦ if(π β π·, (πΉβπ), 0 ))))) |
41 | 7 | feqmptd 6914 |
. . . . 5
β’ (π β πΉ = (π β π΄ β¦ (πΉβπ))) |
42 | | iftrue 4496 |
. . . . . . . . . 10
β’ (π β πΆ β if(π β πΆ, (πΉβπ), 0 ) = (πΉβπ)) |
43 | 42 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β πΆ) β if(π β πΆ, (πΉβπ), 0 ) = (πΉβπ)) |
44 | | gsumzsplit.i |
. . . . . . . . . . . . . . 15
β’ (π β (πΆ β© π·) = β
) |
45 | | noel 4294 |
. . . . . . . . . . . . . . . 16
β’ Β¬
π β
β
|
46 | | eleq2 2823 |
. . . . . . . . . . . . . . . 16
β’ ((πΆ β© π·) = β
β (π β (πΆ β© π·) β π β β
)) |
47 | 45, 46 | mtbiri 327 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β© π·) = β
β Β¬ π β (πΆ β© π·)) |
48 | 44, 47 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β Β¬ π β (πΆ β© π·)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β Β¬ π β (πΆ β© π·)) |
50 | | elin 3930 |
. . . . . . . . . . . . 13
β’ (π β (πΆ β© π·) β (π β πΆ β§ π β π·)) |
51 | 49, 50 | sylnib 328 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β Β¬ (π β πΆ β§ π β π·)) |
52 | | imnan 401 |
. . . . . . . . . . . 12
β’ ((π β πΆ β Β¬ π β π·) β Β¬ (π β πΆ β§ π β π·)) |
53 | 51, 52 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (π β πΆ β Β¬ π β π·)) |
54 | 53 | imp 408 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π β πΆ) β Β¬ π β π·) |
55 | 54 | iffalsed 4501 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β πΆ) β if(π β π·, (πΉβπ), 0 ) = 0 ) |
56 | 43, 55 | oveq12d 7379 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β πΆ) β (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )) = ((πΉβπ) + 0 )) |
57 | 7 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (πΉβπ) β π΅) |
58 | 1, 3, 2 | mndrid 18585 |
. . . . . . . . . 10
β’ ((πΊ β Mnd β§ (πΉβπ) β π΅) β ((πΉβπ) + 0 ) = (πΉβπ)) |
59 | 5, 57, 58 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ((πΉβπ) + 0 ) = (πΉβπ)) |
60 | 59 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β πΆ) β ((πΉβπ) + 0 ) = (πΉβπ)) |
61 | 56, 60 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π β πΆ) β (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )) = (πΉβπ)) |
62 | 53 | con2d 134 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (π β π· β Β¬ π β πΆ)) |
63 | 62 | imp 408 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π β π·) β Β¬ π β πΆ) |
64 | 63 | iffalsed 4501 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β π·) β if(π β πΆ, (πΉβπ), 0 ) = 0 ) |
65 | | iftrue 4496 |
. . . . . . . . . 10
β’ (π β π· β if(π β π·, (πΉβπ), 0 ) = (πΉβπ)) |
66 | 65 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β π·) β if(π β π·, (πΉβπ), 0 ) = (πΉβπ)) |
67 | 64, 66 | oveq12d 7379 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π·) β (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )) = ( 0 + (πΉβπ))) |
68 | 1, 3, 2 | mndlid 18584 |
. . . . . . . . . 10
β’ ((πΊ β Mnd β§ (πΉβπ) β π΅) β ( 0 + (πΉβπ)) = (πΉβπ)) |
69 | 5, 57, 68 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ( 0 + (πΉβπ)) = (πΉβπ)) |
70 | 69 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π β π·) β ( 0 + (πΉβπ)) = (πΉβπ)) |
71 | 67, 70 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π β π·) β (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )) = (πΉβπ)) |
72 | | gsumzsplit.u |
. . . . . . . . . 10
β’ (π β π΄ = (πΆ βͺ π·)) |
73 | 72 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β (π β π΄ β π β (πΆ βͺ π·))) |
74 | | elun 4112 |
. . . . . . . . 9
β’ (π β (πΆ βͺ π·) β (π β πΆ β¨ π β π·)) |
75 | 73, 74 | bitrdi 287 |
. . . . . . . 8
β’ (π β (π β π΄ β (π β πΆ β¨ π β π·))) |
76 | 75 | biimpa 478 |
. . . . . . 7
β’ ((π β§ π β π΄) β (π β πΆ β¨ π β π·)) |
77 | 61, 71, 76 | mpjaodan 958 |
. . . . . 6
β’ ((π β§ π β π΄) β (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )) = (πΉβπ)) |
78 | 77 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π β π΄ β¦ (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 ))) = (π β π΄ β¦ (πΉβπ))) |
79 | 41, 78 | eqtr4d 2776 |
. . . 4
β’ (π β πΉ = (π β π΄ β¦ (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )))) |
80 | 1, 2 | mndidcl 18579 |
. . . . . . . 8
β’ (πΊ β Mnd β 0 β π΅) |
81 | 5, 80 | syl 17 |
. . . . . . 7
β’ (π β 0 β π΅) |
82 | 81 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β 0 β π΅) |
83 | 57, 82 | ifcld 4536 |
. . . . 5
β’ ((π β§ π β π΄) β if(π β πΆ, (πΉβπ), 0 ) β π΅) |
84 | 57, 82 | ifcld 4536 |
. . . . 5
β’ ((π β§ π β π΄) β if(π β π·, (πΉβπ), 0 ) β π΅) |
85 | | eqidd 2734 |
. . . . 5
β’ (π β (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) = (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 ))) |
86 | | eqidd 2734 |
. . . . 5
β’ (π β (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) = (π β π΄ β¦ if(π β π·, (πΉβπ), 0 ))) |
87 | 6, 83, 84, 85, 86 | offval2 7641 |
. . . 4
β’ (π β ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βf
+ (π β π΄ β¦ if(π β π·, (πΉβπ), 0 ))) = (π β π΄ β¦ (if(π β πΆ, (πΉβπ), 0 ) + if(π β π·, (πΉβπ), 0 )))) |
88 | 79, 87 | eqtr4d 2776 |
. . 3
β’ (π β πΉ = ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βf
+ (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )))) |
89 | 88 | oveq2d 7377 |
. 2
β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βf
+ (π β π΄ β¦ if(π β π·, (πΉβπ), 0 ))))) |
90 | 41 | reseq1d 5940 |
. . . . . 6
β’ (π β (πΉ βΎ πΆ) = ((π β π΄ β¦ (πΉβπ)) βΎ πΆ)) |
91 | | ssun1 4136 |
. . . . . . . 8
β’ πΆ β (πΆ βͺ π·) |
92 | 91, 72 | sseqtrrid 4001 |
. . . . . . 7
β’ (π β πΆ β π΄) |
93 | 42 | mpteq2ia 5212 |
. . . . . . . 8
β’ (π β πΆ β¦ if(π β πΆ, (πΉβπ), 0 )) = (π β πΆ β¦ (πΉβπ)) |
94 | | resmpt 5995 |
. . . . . . . 8
β’ (πΆ β π΄ β ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βΎ πΆ) = (π β πΆ β¦ if(π β πΆ, (πΉβπ), 0 ))) |
95 | | resmpt 5995 |
. . . . . . . 8
β’ (πΆ β π΄ β ((π β π΄ β¦ (πΉβπ)) βΎ πΆ) = (π β πΆ β¦ (πΉβπ))) |
96 | 93, 94, 95 | 3eqtr4a 2799 |
. . . . . . 7
β’ (πΆ β π΄ β ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βΎ πΆ) = ((π β π΄ β¦ (πΉβπ)) βΎ πΆ)) |
97 | 92, 96 | syl 17 |
. . . . . 6
β’ (π β ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βΎ πΆ) = ((π β π΄ β¦ (πΉβπ)) βΎ πΆ)) |
98 | 90, 97 | eqtr4d 2776 |
. . . . 5
β’ (π β (πΉ βΎ πΆ) = ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βΎ πΆ)) |
99 | 98 | oveq2d 7377 |
. . . 4
β’ (π β (πΊ Ξ£g (πΉ βΎ πΆ)) = (πΊ Ξ£g ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βΎ πΆ))) |
100 | 83 | fmpttd 7067 |
. . . . 5
β’ (π β (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )):π΄βΆπ΅) |
101 | 37 | frnd 6680 |
. . . . . 6
β’ (π β ran (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
102 | 4 | cntzidss 19126 |
. . . . . 6
β’
((((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)) β§ ran (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) β
((mrClsβ(SubMndβπΊ))βran πΉ)) β ran (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) β (πβran (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )))) |
103 | 26, 101, 102 | syl2anc 585 |
. . . . 5
β’ (π β ran (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) β (πβran (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )))) |
104 | | eldifn 4091 |
. . . . . . . 8
β’ (π β (π΄ β πΆ) β Β¬ π β πΆ) |
105 | 104 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (π΄ β πΆ)) β Β¬ π β πΆ) |
106 | 105 | iffalsed 4501 |
. . . . . 6
β’ ((π β§ π β (π΄ β πΆ)) β if(π β πΆ, (πΉβπ), 0 ) = 0 ) |
107 | 106, 6 | suppss2 8135 |
. . . . 5
β’ (π β ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) supp 0 ) β πΆ) |
108 | 1, 2, 4, 5, 6, 100, 103, 107, 11 | gsumzres 19694 |
. . . 4
β’ (π β (πΊ Ξ£g ((π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )) βΎ πΆ)) = (πΊ Ξ£g (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )))) |
109 | 99, 108 | eqtrd 2773 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ πΆ)) = (πΊ Ξ£g (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 )))) |
110 | 41 | reseq1d 5940 |
. . . . . 6
β’ (π β (πΉ βΎ π·) = ((π β π΄ β¦ (πΉβπ)) βΎ π·)) |
111 | | ssun2 4137 |
. . . . . . . 8
β’ π· β (πΆ βͺ π·) |
112 | 111, 72 | sseqtrrid 4001 |
. . . . . . 7
β’ (π β π· β π΄) |
113 | 65 | mpteq2ia 5212 |
. . . . . . . 8
β’ (π β π· β¦ if(π β π·, (πΉβπ), 0 )) = (π β π· β¦ (πΉβπ)) |
114 | | resmpt 5995 |
. . . . . . . 8
β’ (π· β π΄ β ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) βΎ π·) = (π β π· β¦ if(π β π·, (πΉβπ), 0 ))) |
115 | | resmpt 5995 |
. . . . . . . 8
β’ (π· β π΄ β ((π β π΄ β¦ (πΉβπ)) βΎ π·) = (π β π· β¦ (πΉβπ))) |
116 | 113, 114,
115 | 3eqtr4a 2799 |
. . . . . . 7
β’ (π· β π΄ β ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) βΎ π·) = ((π β π΄ β¦ (πΉβπ)) βΎ π·)) |
117 | 112, 116 | syl 17 |
. . . . . 6
β’ (π β ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) βΎ π·) = ((π β π΄ β¦ (πΉβπ)) βΎ π·)) |
118 | 110, 117 | eqtr4d 2776 |
. . . . 5
β’ (π β (πΉ βΎ π·) = ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) βΎ π·)) |
119 | 118 | oveq2d 7377 |
. . . 4
β’ (π β (πΊ Ξ£g (πΉ βΎ π·)) = (πΊ Ξ£g ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) βΎ π·))) |
120 | 84 | fmpttd 7067 |
. . . . 5
β’ (π β (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )):π΄βΆπ΅) |
121 | 39 | frnd 6680 |
. . . . . 6
β’ (π β ran (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
122 | 4 | cntzidss 19126 |
. . . . . 6
β’
((((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)) β§ ran (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) β
((mrClsβ(SubMndβπΊ))βran πΉ)) β ran (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) β (πβran (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )))) |
123 | 26, 121, 122 | syl2anc 585 |
. . . . 5
β’ (π β ran (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) β (πβran (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )))) |
124 | | eldifn 4091 |
. . . . . . . 8
β’ (π β (π΄ β π·) β Β¬ π β π·) |
125 | 124 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (π΄ β π·)) β Β¬ π β π·) |
126 | 125 | iffalsed 4501 |
. . . . . 6
β’ ((π β§ π β (π΄ β π·)) β if(π β π·, (πΉβπ), 0 ) = 0 ) |
127 | 126, 6 | suppss2 8135 |
. . . . 5
β’ (π β ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) supp 0 ) β π·) |
128 | 1, 2, 4, 5, 6, 120, 123, 127, 12 | gsumzres 19694 |
. . . 4
β’ (π β (πΊ Ξ£g ((π β π΄ β¦ if(π β π·, (πΉβπ), 0 )) βΎ π·)) = (πΊ Ξ£g (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )))) |
129 | 119, 128 | eqtrd 2773 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ π·)) = (πΊ Ξ£g (π β π΄ β¦ if(π β π·, (πΉβπ), 0 )))) |
130 | 109, 129 | oveq12d 7379 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ πΆ)) + (πΊ Ξ£g (πΉ βΎ π·))) = ((πΊ Ξ£g (π β π΄ β¦ if(π β πΆ, (πΉβπ), 0 ))) + (πΊ Ξ£g (π β π΄ β¦ if(π β π·, (πΉβπ), 0 ))))) |
131 | 40, 89, 130 | 3eqtr4d 2783 |
1
β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (πΉ βΎ πΆ)) + (πΊ Ξ£g (πΉ βΎ π·)))) |