Step | Hyp | Ref
| Expression |
1 | | rrgsupp.i |
. . . . . . . . 9
β’ (π β πΌ β π) |
2 | | rrgsupp.x |
. . . . . . . . . 10
β’ (π β π β πΈ) |
3 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β π β πΈ) |
4 | | fvexd 6858 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β (πβπ¦) β V) |
5 | | fconstmpt 5695 |
. . . . . . . . . 10
β’ (πΌ Γ {π}) = (π¦ β πΌ β¦ π) |
6 | 5 | a1i 11 |
. . . . . . . . 9
β’ (π β (πΌ Γ {π}) = (π¦ β πΌ β¦ π)) |
7 | | rrgsupp.y |
. . . . . . . . . 10
β’ (π β π:πΌβΆπ΅) |
8 | 7 | feqmptd 6911 |
. . . . . . . . 9
β’ (π β π = (π¦ β πΌ β¦ (πβπ¦))) |
9 | 1, 3, 4, 6, 8 | offval2 7638 |
. . . . . . . 8
β’ (π β ((πΌ Γ {π}) βf Β· π) = (π¦ β πΌ β¦ (π Β· (πβπ¦)))) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β ((πΌ Γ {π}) βf Β· π) = (π¦ β πΌ β¦ (π Β· (πβπ¦)))) |
11 | 10 | fveq1d 6845 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (((πΌ Γ {π}) βf Β· π)βπ₯) = ((π¦ β πΌ β¦ (π Β· (πβπ¦)))βπ₯)) |
12 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π₯ β πΌ) |
13 | | ovex 7391 |
. . . . . . 7
β’ (π Β· (πβπ₯)) β V |
14 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = π₯ β (πβπ¦) = (πβπ₯)) |
15 | 14 | oveq2d 7374 |
. . . . . . . 8
β’ (π¦ = π₯ β (π Β· (πβπ¦)) = (π Β· (πβπ₯))) |
16 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β πΌ β¦ (π Β· (πβπ¦))) = (π¦ β πΌ β¦ (π Β· (πβπ¦))) |
17 | 15, 16 | fvmptg 6947 |
. . . . . . 7
β’ ((π₯ β πΌ β§ (π Β· (πβπ₯)) β V) β ((π¦ β πΌ β¦ (π Β· (πβπ¦)))βπ₯) = (π Β· (πβπ₯))) |
18 | 12, 13, 17 | sylancl 587 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β ((π¦ β πΌ β¦ (π Β· (πβπ¦)))βπ₯) = (π Β· (πβπ₯))) |
19 | 11, 18 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (((πΌ Γ {π}) βf Β· π)βπ₯) = (π Β· (πβπ₯))) |
20 | 19 | neeq1d 3000 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((((πΌ Γ {π}) βf Β· π)βπ₯) β 0 β (π Β· (πβπ₯)) β 0 )) |
21 | 20 | rabbidva 3413 |
. . 3
β’ (π β {π₯ β πΌ β£ (((πΌ Γ {π}) βf Β· π)βπ₯) β 0 } = {π₯ β πΌ β£ (π Β· (πβπ₯)) β 0 }) |
22 | | rrgsupp.r |
. . . . . . 7
β’ (π β π
β Ring) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β π
β Ring) |
24 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β π β πΈ) |
25 | 7 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β π΅) |
26 | | rrgval.e |
. . . . . . 7
β’ πΈ = (RLRegβπ
) |
27 | | rrgval.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
28 | | rrgval.t |
. . . . . . 7
β’ Β· =
(.rβπ
) |
29 | | rrgval.z |
. . . . . . 7
β’ 0 =
(0gβπ
) |
30 | 26, 27, 28, 29 | rrgeq0 20776 |
. . . . . 6
β’ ((π
β Ring β§ π β πΈ β§ (πβπ₯) β π΅) β ((π Β· (πβπ₯)) = 0 β (πβπ₯) = 0 )) |
31 | 23, 24, 25, 30 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β ((π Β· (πβπ₯)) = 0 β (πβπ₯) = 0 )) |
32 | 31 | necon3bid 2985 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((π Β· (πβπ₯)) β 0 β (πβπ₯) β 0 )) |
33 | 32 | rabbidva 3413 |
. . 3
β’ (π β {π₯ β πΌ β£ (π Β· (πβπ₯)) β 0 } = {π₯ β πΌ β£ (πβπ₯) β 0 }) |
34 | 21, 33 | eqtrd 2773 |
. 2
β’ (π β {π₯ β πΌ β£ (((πΌ Γ {π}) βf Β· π)βπ₯) β 0 } = {π₯ β πΌ β£ (πβπ₯) β 0 }) |
35 | | ovex 7391 |
. . . . . 6
β’ (π Β· (πβπ¦)) β V |
36 | 35, 16 | fnmpti 6645 |
. . . . 5
β’ (π¦ β πΌ β¦ (π Β· (πβπ¦))) Fn πΌ |
37 | | fneq1 6594 |
. . . . 5
β’ (((πΌ Γ {π}) βf Β· π) = (π¦ β πΌ β¦ (π Β· (πβπ¦))) β (((πΌ Γ {π}) βf Β· π) Fn πΌ β (π¦ β πΌ β¦ (π Β· (πβπ¦))) Fn πΌ)) |
38 | 36, 37 | mpbiri 258 |
. . . 4
β’ (((πΌ Γ {π}) βf Β· π) = (π¦ β πΌ β¦ (π Β· (πβπ¦))) β ((πΌ Γ {π}) βf Β· π) Fn πΌ) |
39 | 9, 38 | syl 17 |
. . 3
β’ (π β ((πΌ Γ {π}) βf Β· π) Fn πΌ) |
40 | 29 | fvexi 6857 |
. . . 4
β’ 0 β
V |
41 | 40 | a1i 11 |
. . 3
β’ (π β 0 β V) |
42 | | suppvalfn 8101 |
. . 3
β’ ((((πΌ Γ {π}) βf Β· π) Fn πΌ β§ πΌ β π β§ 0 β V) β (((πΌ Γ {π}) βf Β· π) supp 0 ) = {π₯ β πΌ β£ (((πΌ Γ {π}) βf Β· π)βπ₯) β 0 }) |
43 | 39, 1, 41, 42 | syl3anc 1372 |
. 2
β’ (π β (((πΌ Γ {π}) βf Β· π) supp 0 ) = {π₯ β πΌ β£ (((πΌ Γ {π}) βf Β· π)βπ₯) β 0 }) |
44 | 7 | ffnd 6670 |
. . 3
β’ (π β π Fn πΌ) |
45 | | suppvalfn 8101 |
. . 3
β’ ((π Fn πΌ β§ πΌ β π β§ 0 β V) β (π supp 0 ) = {π₯ β πΌ β£ (πβπ₯) β 0 }) |
46 | 44, 1, 41, 45 | syl3anc 1372 |
. 2
β’ (π β (π supp 0 ) = {π₯ β πΌ β£ (πβπ₯) β 0 }) |
47 | 34, 43, 46 | 3eqtr4d 2783 |
1
β’ (π β (((πΌ Γ {π}) βf Β· π) supp 0 ) = (π supp 0 )) |