Step | Hyp | Ref
| Expression |
1 | | gsumzadd.b |
. 2
β’ π΅ = (BaseβπΊ) |
2 | | gsumzadd.0 |
. 2
β’ 0 =
(0gβπΊ) |
3 | | gsumzadd.p |
. 2
β’ + =
(+gβπΊ) |
4 | | gsumzadd.z |
. 2
β’ π = (CntzβπΊ) |
5 | | gsumzadd.g |
. 2
β’ (π β πΊ β Mnd) |
6 | | gsumzadd.a |
. 2
β’ (π β π΄ β π) |
7 | | gsumzadd.fn |
. 2
β’ (π β πΉ finSupp 0 ) |
8 | | gsumzadd.hn |
. 2
β’ (π β π» finSupp 0 ) |
9 | | eqid 2733 |
. 2
β’ ((πΉ βͺ π») supp 0 ) = ((πΉ βͺ π») supp 0 ) |
10 | | gsumzadd.f |
. . 3
β’ (π β πΉ:π΄βΆπ) |
11 | | gsumzadd.s |
. . . 4
β’ (π β π β (SubMndβπΊ)) |
12 | 1 | submss 18628 |
. . . 4
β’ (π β (SubMndβπΊ) β π β π΅) |
13 | 11, 12 | syl 17 |
. . 3
β’ (π β π β π΅) |
14 | 10, 13 | fssd 6690 |
. 2
β’ (π β πΉ:π΄βΆπ΅) |
15 | | gsumzadd.h |
. . 3
β’ (π β π»:π΄βΆπ) |
16 | 15, 13 | fssd 6690 |
. 2
β’ (π β π»:π΄βΆπ΅) |
17 | | gsumzadd.c |
. . 3
β’ (π β π β (πβπ)) |
18 | 10 | frnd 6680 |
. . 3
β’ (π β ran πΉ β π) |
19 | 4 | cntzidss 19126 |
. . 3
β’ ((π β (πβπ) β§ ran πΉ β π) β ran πΉ β (πβran πΉ)) |
20 | 17, 18, 19 | syl2anc 585 |
. 2
β’ (π β ran πΉ β (πβran πΉ)) |
21 | 15 | frnd 6680 |
. . 3
β’ (π β ran π» β π) |
22 | 4 | cntzidss 19126 |
. . 3
β’ ((π β (πβπ) β§ ran π» β π) β ran π» β (πβran π»)) |
23 | 17, 21, 22 | syl2anc 585 |
. 2
β’ (π β ran π» β (πβran π»)) |
24 | 3 | submcl 18631 |
. . . . . . 7
β’ ((π β (SubMndβπΊ) β§ π₯ β π β§ π¦ β π) β (π₯ + π¦) β π) |
25 | 24 | 3expb 1121 |
. . . . . 6
β’ ((π β (SubMndβπΊ) β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) |
26 | 11, 25 | sylan 581 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) |
27 | | inidm 4182 |
. . . . 5
β’ (π΄ β© π΄) = π΄ |
28 | 26, 10, 15, 6, 6, 27 | off 7639 |
. . . 4
β’ (π β (πΉ βf + π»):π΄βΆπ) |
29 | 28 | frnd 6680 |
. . 3
β’ (π β ran (πΉ βf + π») β π) |
30 | 4 | cntzidss 19126 |
. . 3
β’ ((π β (πβπ) β§ ran (πΉ βf + π») β π) β ran (πΉ βf + π») β (πβran (πΉ βf + π»))) |
31 | 17, 29, 30 | syl2anc 585 |
. 2
β’ (π β ran (πΉ βf + π») β (πβran (πΉ βf + π»))) |
32 | 17 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β π β (πβπ)) |
33 | 13 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β π β π΅) |
34 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β πΊ β Mnd) |
35 | | vex 3451 |
. . . . . . . 8
β’ π₯ β V |
36 | 35 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β π₯ β V) |
37 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β π β (SubMndβπΊ)) |
38 | | simpl 484 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ π β (π΄ β π₯)) β π₯ β π΄) |
39 | | fssres 6712 |
. . . . . . . 8
β’ ((π»:π΄βΆπ β§ π₯ β π΄) β (π» βΎ π₯):π₯βΆπ) |
40 | 15, 38, 39 | syl2an 597 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (π» βΎ π₯):π₯βΆπ) |
41 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β ran π» β (πβran π»)) |
42 | | resss 5966 |
. . . . . . . . 9
β’ (π» βΎ π₯) β π» |
43 | 42 | rnssi 5899 |
. . . . . . . 8
β’ ran
(π» βΎ π₯) β ran π» |
44 | 4 | cntzidss 19126 |
. . . . . . . 8
β’ ((ran
π» β (πβran π») β§ ran (π» βΎ π₯) β ran π») β ran (π» βΎ π₯) β (πβran (π» βΎ π₯))) |
45 | 41, 43, 44 | sylancl 587 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β ran (π» βΎ π₯) β (πβran (π» βΎ π₯))) |
46 | 15 | ffund 6676 |
. . . . . . . . . 10
β’ (π β Fun π») |
47 | 46 | funresd 6548 |
. . . . . . . . 9
β’ (π β Fun (π» βΎ π₯)) |
48 | 47 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β Fun (π» βΎ π₯)) |
49 | 8 | fsuppimpd 9319 |
. . . . . . . . . 10
β’ (π β (π» supp 0 ) β
Fin) |
50 | 49 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (π» supp 0 ) β
Fin) |
51 | 15, 6 | fexd 7181 |
. . . . . . . . . . 11
β’ (π β π» β V) |
52 | 2 | fvexi 6860 |
. . . . . . . . . . 11
β’ 0 β
V |
53 | | ressuppss 8118 |
. . . . . . . . . . 11
β’ ((π» β V β§ 0 β V)
β ((π» βΎ π₯) supp 0 ) β (π» supp 0 )) |
54 | 51, 52, 53 | sylancl 587 |
. . . . . . . . . 10
β’ (π β ((π» βΎ π₯) supp 0 ) β (π» supp 0 )) |
55 | 54 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β ((π» βΎ π₯) supp 0 ) β (π» supp 0 )) |
56 | 50, 55 | ssfid 9217 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β ((π» βΎ π₯) supp 0 ) β
Fin) |
57 | | resfunexg 7169 |
. . . . . . . . . . 11
β’ ((Fun
π» β§ π₯ β V) β (π» βΎ π₯) β V) |
58 | 46, 35, 57 | sylancl 587 |
. . . . . . . . . 10
β’ (π β (π» βΎ π₯) β V) |
59 | | isfsupp 9315 |
. . . . . . . . . 10
β’ (((π» βΎ π₯) β V β§ 0 β V) β ((π» βΎ π₯) finSupp 0 β (Fun (π» βΎ π₯) β§ ((π» βΎ π₯) supp 0 ) β
Fin))) |
60 | 58, 52, 59 | sylancl 587 |
. . . . . . . . 9
β’ (π β ((π» βΎ π₯) finSupp 0 β (Fun (π» βΎ π₯) β§ ((π» βΎ π₯) supp 0 ) β
Fin))) |
61 | 60 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β ((π» βΎ π₯) finSupp 0 β (Fun (π» βΎ π₯) β§ ((π» βΎ π₯) supp 0 ) β
Fin))) |
62 | 48, 56, 61 | mpbir2and 712 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (π» βΎ π₯) finSupp 0 ) |
63 | 2, 4, 34, 36, 37, 40, 45, 62 | gsumzsubmcl 19703 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (πΊ Ξ£g (π» βΎ π₯)) β π) |
64 | 63 | snssd 4773 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β {(πΊ Ξ£g (π» βΎ π₯))} β π) |
65 | 1, 4 | cntz2ss 19121 |
. . . . 5
β’ ((π β π΅ β§ {(πΊ Ξ£g (π» βΎ π₯))} β π) β (πβπ) β (πβ{(πΊ Ξ£g (π» βΎ π₯))})) |
66 | 33, 64, 65 | syl2anc 585 |
. . . 4
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (πβπ) β (πβ{(πΊ Ξ£g (π» βΎ π₯))})) |
67 | 32, 66 | sstrd 3958 |
. . 3
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β π β (πβ{(πΊ Ξ£g (π» βΎ π₯))})) |
68 | | eldifi 4090 |
. . . . 5
β’ (π β (π΄ β π₯) β π β π΄) |
69 | 68 | adantl 483 |
. . . 4
β’ ((π₯ β π΄ β§ π β (π΄ β π₯)) β π β π΄) |
70 | | ffvelcdm 7036 |
. . . 4
β’ ((πΉ:π΄βΆπ β§ π β π΄) β (πΉβπ) β π) |
71 | 10, 69, 70 | syl2an 597 |
. . 3
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (πΉβπ) β π) |
72 | 67, 71 | sseldd 3949 |
. 2
β’ ((π β§ (π₯ β π΄ β§ π β (π΄ β π₯))) β (πΉβπ) β (πβ{(πΊ Ξ£g (π» βΎ π₯))})) |
73 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 14,
16, 20, 23, 31, 72 | gsumzaddlem 19706 |
1
β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) |