Step | Hyp | Ref
| Expression |
1 | | lcomfsupp.j |
. . . 4
β’ (π β πΊ finSupp π) |
2 | 1 | fsuppimpd 9319 |
. . 3
β’ (π β (πΊ supp π) β Fin) |
3 | | lcomf.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
4 | | lcomf.k |
. . . . 5
β’ πΎ = (BaseβπΉ) |
5 | | lcomf.s |
. . . . 5
β’ Β· = (
Β·π βπ) |
6 | | lcomf.b |
. . . . 5
β’ π΅ = (Baseβπ) |
7 | | lcomf.w |
. . . . 5
β’ (π β π β LMod) |
8 | | lcomf.g |
. . . . 5
β’ (π β πΊ:πΌβΆπΎ) |
9 | | lcomf.h |
. . . . 5
β’ (π β π»:πΌβΆπ΅) |
10 | | lcomf.i |
. . . . 5
β’ (π β πΌ β π) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | lcomf 20405 |
. . . 4
β’ (π β (πΊ βf Β· π»):πΌβΆπ΅) |
12 | | eldifi 4090 |
. . . . . 6
β’ (π₯ β (πΌ β (πΊ supp π)) β π₯ β πΌ) |
13 | 8 | ffnd 6673 |
. . . . . . . 8
β’ (π β πΊ Fn πΌ) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β πΊ Fn πΌ) |
15 | 9 | ffnd 6673 |
. . . . . . . 8
β’ (π β π» Fn πΌ) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π» Fn πΌ) |
17 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β πΌ β π) |
18 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π₯ β πΌ) |
19 | | fnfvof 7638 |
. . . . . . 7
β’ (((πΊ Fn πΌ β§ π» Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β ((πΊ βf Β· π»)βπ₯) = ((πΊβπ₯) Β· (π»βπ₯))) |
20 | 14, 16, 17, 18, 19 | syl22anc 838 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β ((πΊ βf Β· π»)βπ₯) = ((πΊβπ₯) Β· (π»βπ₯))) |
21 | 12, 20 | sylan2 594 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β (πΊ supp π))) β ((πΊ βf Β· π»)βπ₯) = ((πΊβπ₯) Β· (π»βπ₯))) |
22 | | ssidd 3971 |
. . . . . . 7
β’ (π β (πΊ supp π) β (πΊ supp π)) |
23 | | lcomfsupp.y |
. . . . . . . . 9
β’ π = (0gβπΉ) |
24 | 23 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π β π β V) |
26 | 8, 22, 10, 25 | suppssr 8131 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β (πΊ supp π))) β (πΊβπ₯) = π) |
27 | 26 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β (πΊ supp π))) β ((πΊβπ₯) Β· (π»βπ₯)) = (π Β· (π»βπ₯))) |
28 | 9 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (π»βπ₯) β π΅) |
29 | | lcomfsupp.z |
. . . . . . . 8
β’ 0 =
(0gβπ) |
30 | 6, 3, 5, 23, 29 | lmod0vs 20399 |
. . . . . . 7
β’ ((π β LMod β§ (π»βπ₯) β π΅) β (π Β· (π»βπ₯)) = 0 ) |
31 | 7, 28, 30 | syl2an2r 684 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (π Β· (π»βπ₯)) = 0 ) |
32 | 12, 31 | sylan2 594 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β (πΊ supp π))) β (π Β· (π»βπ₯)) = 0 ) |
33 | 21, 27, 32 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π₯ β (πΌ β (πΊ supp π))) β ((πΊ βf Β· π»)βπ₯) = 0 ) |
34 | 11, 33 | suppss 8129 |
. . 3
β’ (π β ((πΊ βf Β· π») supp 0 ) β (πΊ supp π)) |
35 | 2, 34 | ssfid 9217 |
. 2
β’ (π β ((πΊ βf Β· π») supp 0 ) β
Fin) |
36 | 13, 15, 10, 10 | offun 7635 |
. . 3
β’ (π β Fun (πΊ βf Β· π»)) |
37 | | ovexd 7396 |
. . 3
β’ (π β (πΊ βf Β· π») β V) |
38 | 29 | fvexi 6860 |
. . . 4
β’ 0 β
V |
39 | 38 | a1i 11 |
. . 3
β’ (π β 0 β V) |
40 | | funisfsupp 9317 |
. . 3
β’ ((Fun
(πΊ βf
Β·
π») β§ (πΊ βf Β· π») β V β§ 0 β V) β ((πΊ βf Β· π») finSupp 0 β ((πΊ βf Β· π») supp 0 ) β
Fin)) |
41 | 36, 37, 39, 40 | syl3anc 1372 |
. 2
β’ (π β ((πΊ βf Β· π») finSupp 0 β ((πΊ βf Β· π») supp 0 ) β
Fin)) |
42 | 35, 41 | mpbird 257 |
1
β’ (π β (πΊ βf Β· π») finSupp 0 ) |