Step | Hyp | Ref
| Expression |
1 | | suppmptcfin.f |
. . . 4
β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) |
2 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = π£ β (π₯ = π β π£ = π)) |
3 | 2 | ifbid 4513 |
. . . . 5
β’ (π₯ = π£ β if(π₯ = π, 1 , 0 ) = if(π£ = π, 1 , 0 )) |
4 | 3 | cbvmptv 5222 |
. . . 4
β’ (π₯ β π β¦ if(π₯ = π, 1 , 0 )) = (π£ β π β¦ if(π£ = π, 1 , 0 )) |
5 | 1, 4 | eqtri 2761 |
. . 3
β’ πΉ = (π£ β π β¦ if(π£ = π, 1 , 0 )) |
6 | | simp2 1138 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β π β π« π΅) |
7 | | suppmptcfin.0 |
. . . . 5
β’ 0 =
(0gβπ
) |
8 | 7 | fvexi 6860 |
. . . 4
β’ 0 β
V |
9 | 8 | a1i 11 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β 0 β V) |
10 | | suppmptcfin.1 |
. . . . . 6
β’ 1 =
(1rβπ
) |
11 | 10 | fvexi 6860 |
. . . . 5
β’ 1 β
V |
12 | 11 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β 1 β V) |
13 | 8 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β 0 β V) |
14 | 12, 13 | ifcld 4536 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β if(π£ = π, 1 , 0 ) β
V) |
15 | 5, 6, 9, 14 | mptsuppd 8122 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ supp 0 ) = {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 }) |
16 | | snfi 8994 |
. . 3
β’ {π} β Fin |
17 | | 2a1 28 |
. . . . . 6
β’ (π£ = π β (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π))) |
18 | | iffalse 4499 |
. . . . . . . . . 10
β’ (Β¬
π£ = π β if(π£ = π, 1 , 0 ) = 0 ) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((Β¬
π£ = π β§ ((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π)) β if(π£ = π, 1 , 0 ) = 0 ) |
20 | 19 | neeq1d 3000 |
. . . . . . . 8
β’ ((Β¬
π£ = π β§ ((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π)) β (if(π£ = π, 1 , 0 ) β 0 β 0 β 0 )) |
21 | | eqid 2733 |
. . . . . . . . 9
β’ 0 = 0 |
22 | | eqneqall 2951 |
. . . . . . . . 9
β’ ( 0 = 0 β (
0 β
0 β
π£ = π)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
β’ ( 0 β 0 β π£ = π) |
24 | 20, 23 | syl6bi 253 |
. . . . . . 7
β’ ((Β¬
π£ = π β§ ((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π)) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
25 | 24 | ex 414 |
. . . . . 6
β’ (Β¬
π£ = π β (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π))) |
26 | 17, 25 | pm2.61i 182 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
27 | 26 | ralrimiva 3140 |
. . . 4
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β βπ£ β π (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
28 | | rabsssn 4632 |
. . . 4
β’ ({π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β {π} β βπ£ β π (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
29 | 27, 28 | sylibr 233 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β {π}) |
30 | | ssfi 9123 |
. . 3
β’ (({π} β Fin β§ {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β {π}) β {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β
Fin) |
31 | 16, 29, 30 | sylancr 588 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β
Fin) |
32 | 15, 31 | eqeltrd 2834 |
1
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ supp 0 ) β
Fin) |