Step | Hyp | Ref
| Expression |
1 | | fcdmnn0supp 12474 |
. . 3
β’ ((πΌ β π β§ πΊ:πΌβΆβ0) β (πΊ supp 0) = (β‘πΊ β β)) |
2 | 1 | 3ad2antr2 1190 |
. 2
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΊ supp 0) = (β‘πΊ β β)) |
3 | | simpr2 1196 |
. . 3
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ:πΌβΆβ0) |
4 | | eldifi 4087 |
. . . . . 6
β’ (π₯ β (πΌ β (β‘πΉ β β)) β π₯ β πΌ) |
5 | | simpr3 1197 |
. . . . . . . 8
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ βr β€ πΉ) |
6 | 3 | ffnd 6670 |
. . . . . . . . 9
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ Fn πΌ) |
7 | | psrbag.d |
. . . . . . . . . . . 12
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
8 | 7 | psrbagfOLD 21337 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ πΉ β π·) β πΉ:πΌβΆβ0) |
9 | 8 | 3ad2antr1 1189 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΉ:πΌβΆβ0) |
10 | 9 | ffnd 6670 |
. . . . . . . . 9
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΉ Fn πΌ) |
11 | | simpl 484 |
. . . . . . . . 9
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΌ β π) |
12 | | inidm 4179 |
. . . . . . . . 9
β’ (πΌ β© πΌ) = πΌ |
13 | | eqidd 2734 |
. . . . . . . . 9
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΊβπ₯) = (πΊβπ₯)) |
14 | | eqidd 2734 |
. . . . . . . . 9
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΉβπ₯) = (πΉβπ₯)) |
15 | 6, 10, 11, 11, 12, 13, 14 | ofrfval 7628 |
. . . . . . . 8
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΊ βr β€ πΉ β βπ₯ β πΌ (πΊβπ₯) β€ (πΉβπ₯))) |
16 | 5, 15 | mpbid 231 |
. . . . . . 7
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β βπ₯ β πΌ (πΊβπ₯) β€ (πΉβπ₯)) |
17 | 16 | r19.21bi 3233 |
. . . . . 6
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΊβπ₯) β€ (πΉβπ₯)) |
18 | 4, 17 | sylan2 594 |
. . . . 5
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β€ (πΉβπ₯)) |
19 | 11, 9 | jca 513 |
. . . . . . 7
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΌ β π β§ πΉ:πΌβΆβ0)) |
20 | | fcdmnn0supp 12474 |
. . . . . . 7
β’ ((πΌ β π β§ πΉ:πΌβΆβ0) β (πΉ supp 0) = (β‘πΉ β β)) |
21 | | eqimss 4001 |
. . . . . . 7
β’ ((πΉ supp 0) = (β‘πΉ β β) β (πΉ supp 0) β (β‘πΉ β β)) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ supp 0) β (β‘πΉ β β)) |
23 | | c0ex 11154 |
. . . . . . 7
β’ 0 β
V |
24 | 23 | a1i 11 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β 0 β
V) |
25 | 9, 22, 11, 24 | suppssr 8128 |
. . . . 5
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΉβπ₯) = 0) |
26 | 18, 25 | breqtrd 5132 |
. . . 4
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β€ 0) |
27 | | ffvelcdm 7033 |
. . . . . 6
β’ ((πΊ:πΌβΆβ0 β§ π₯ β πΌ) β (πΊβπ₯) β
β0) |
28 | 3, 4, 27 | syl2an 597 |
. . . . 5
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β
β0) |
29 | 28 | nn0ge0d 12481 |
. . . 4
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β 0 β€ (πΊβπ₯)) |
30 | 28 | nn0red 12479 |
. . . . 5
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β β) |
31 | | 0re 11162 |
. . . . 5
β’ 0 β
β |
32 | | letri3 11245 |
. . . . 5
β’ (((πΊβπ₯) β β β§ 0 β β)
β ((πΊβπ₯) = 0 β ((πΊβπ₯) β€ 0 β§ 0 β€ (πΊβπ₯)))) |
33 | 30, 31, 32 | sylancl 587 |
. . . 4
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β ((πΊβπ₯) = 0 β ((πΊβπ₯) β€ 0 β§ 0 β€ (πΊβπ₯)))) |
34 | 26, 29, 33 | mpbir2and 712 |
. . 3
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) = 0) |
35 | 3, 34 | suppss 8126 |
. 2
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΊ supp 0) β (β‘πΉ β β)) |
36 | 2, 35 | eqsstrrd 3984 |
1
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (β‘πΊ β β) β (β‘πΉ β β)) |