Step | Hyp | Ref
| Expression |
1 | | suppmptcfin.f |
. . . 4
β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) |
2 | | eqeq1 2736 |
. . . . . 6
β’ (π₯ = π£ β (π₯ = π β π£ = π)) |
3 | 2 | ifbid 4551 |
. . . . 5
β’ (π₯ = π£ β if(π₯ = π, 1 , 0 ) = if(π£ = π, 1 , 0 )) |
4 | 3 | cbvmptv 5261 |
. . . 4
β’ (π₯ β π β¦ if(π₯ = π, 1 , 0 )) = (π£ β π β¦ if(π£ = π, 1 , 0 )) |
5 | 1, 4 | eqtri 2760 |
. . 3
β’ πΉ = (π£ β π β¦ if(π£ = π, 1 , 0 )) |
6 | | simp2 1137 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β π β π« π΅) |
7 | | suppmptcfin.0 |
. . . . 5
β’ 0 =
(0gβπ
) |
8 | 7 | fvexi 6905 |
. . . 4
β’ 0 β
V |
9 | 8 | a1i 11 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β 0 β V) |
10 | | suppmptcfin.1 |
. . . . . 6
β’ 1 =
(1rβπ
) |
11 | 10 | fvexi 6905 |
. . . . 5
β’ 1 β
V |
12 | 11 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β 1 β V) |
13 | 8 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β 0 β V) |
14 | 12, 13 | ifcld 4574 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β if(π£ = π, 1 , 0 ) β
V) |
15 | 5, 6, 9, 14 | mptsuppd 8171 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ supp 0 ) = {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 }) |
16 | | snfi 9043 |
. . 3
β’ {π} β Fin |
17 | | 2a1 28 |
. . . . . 6
β’ (π£ = π β (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π))) |
18 | | iffalse 4537 |
. . . . . . . . . 10
β’ (Β¬
π£ = π β if(π£ = π, 1 , 0 ) = 0 ) |
19 | 18 | adantr 481 |
. . . . . . . . 9
β’ ((Β¬
π£ = π β§ ((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π)) β if(π£ = π, 1 , 0 ) = 0 ) |
20 | 19 | neeq1d 3000 |
. . . . . . . 8
β’ ((Β¬
π£ = π β§ ((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π)) β (if(π£ = π, 1 , 0 ) β 0 β 0 β 0 )) |
21 | | eqid 2732 |
. . . . . . . . 9
β’ 0 = 0 |
22 | | eqneqall 2951 |
. . . . . . . . 9
β’ ( 0 = 0 β (
0 β
0 β
π£ = π)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
β’ ( 0 β 0 β π£ = π) |
24 | 20, 23 | syl6bi 252 |
. . . . . . 7
β’ ((Β¬
π£ = π β§ ((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π)) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
25 | 24 | ex 413 |
. . . . . 6
β’ (Β¬
π£ = π β (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π))) |
26 | 17, 25 | pm2.61i 182 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ π£ β π) β (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
27 | 26 | ralrimiva 3146 |
. . . 4
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β βπ£ β π (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
28 | | rabsssn 4670 |
. . . 4
β’ ({π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β {π} β βπ£ β π (if(π£ = π, 1 , 0 ) β 0 β π£ = π)) |
29 | 27, 28 | sylibr 233 |
. . 3
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β {π}) |
30 | | ssfi 9172 |
. . 3
β’ (({π} β Fin β§ {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β {π}) β {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β
Fin) |
31 | 16, 29, 30 | sylancr 587 |
. 2
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β {π£ β π β£ if(π£ = π, 1 , 0 ) β 0 } β
Fin) |
32 | 15, 31 | eqeltrd 2833 |
1
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ supp 0 ) β
Fin) |