Step | Hyp | Ref
| Expression |
1 | | df-ofr 7671 |
. . . . . 6
β’
βr β€ = {β¨π, πβ© β£ βπ β (dom π β© dom π)(πβπ) β€ (πβπ)} |
2 | 1 | relopabiv 5821 |
. . . . 5
β’ Rel
βr β€ |
3 | 2 | brrelex1i 5733 |
. . . 4
β’ (πΊ βr β€ πΉ β πΊ β V) |
4 | 3 | 3ad2ant3 1136 |
. . 3
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΊ β V) |
5 | | simp2 1138 |
. . 3
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΊ:πΌβΆβ0) |
6 | | fcdmnn0suppg 12530 |
. . 3
β’ ((πΊ β V β§ πΊ:πΌβΆβ0) β (πΊ supp 0) = (β‘πΊ β β)) |
7 | 4, 5, 6 | syl2anc 585 |
. 2
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (πΊ supp 0) = (β‘πΊ β β)) |
8 | | eldifi 4127 |
. . . . . 6
β’ (π₯ β (πΌ β (β‘πΉ β β)) β π₯ β πΌ) |
9 | | simp3 1139 |
. . . . . . . 8
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΊ βr β€ πΉ) |
10 | 5 | ffnd 6719 |
. . . . . . . . 9
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΊ Fn πΌ) |
11 | | psrbag.d |
. . . . . . . . . . . 12
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
12 | 11 | psrbagf 21471 |
. . . . . . . . . . 11
β’ (πΉ β π· β πΉ:πΌβΆβ0) |
13 | 12 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΉ:πΌβΆβ0) |
14 | 13 | ffnd 6719 |
. . . . . . . . 9
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΉ Fn πΌ) |
15 | | simp1 1137 |
. . . . . . . . 9
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β πΉ β π·) |
16 | | inidm 4219 |
. . . . . . . . 9
β’ (πΌ β© πΌ) = πΌ |
17 | | eqidd 2734 |
. . . . . . . . 9
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β πΌ) β (πΊβπ₯) = (πΊβπ₯)) |
18 | | eqidd 2734 |
. . . . . . . . 9
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β πΌ) β (πΉβπ₯) = (πΉβπ₯)) |
19 | 10, 14, 4, 15, 16, 17, 18 | ofrfvalg 7678 |
. . . . . . . 8
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (πΊ βr β€ πΉ β βπ₯ β πΌ (πΊβπ₯) β€ (πΉβπ₯))) |
20 | 9, 19 | mpbid 231 |
. . . . . . 7
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β βπ₯ β πΌ (πΊβπ₯) β€ (πΉβπ₯)) |
21 | 20 | r19.21bi 3249 |
. . . . . 6
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β πΌ) β (πΊβπ₯) β€ (πΉβπ₯)) |
22 | 8, 21 | sylan2 594 |
. . . . 5
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β€ (πΉβπ₯)) |
23 | | fcdmnn0suppg 12530 |
. . . . . . . 8
β’ ((πΉ β π· β§ πΉ:πΌβΆβ0) β (πΉ supp 0) = (β‘πΉ β β)) |
24 | 15, 13, 23 | syl2anc 585 |
. . . . . . 7
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (πΉ supp 0) = (β‘πΉ β β)) |
25 | | eqimss 4041 |
. . . . . . 7
β’ ((πΉ supp 0) = (β‘πΉ β β) β (πΉ supp 0) β (β‘πΉ β β)) |
26 | 24, 25 | syl 17 |
. . . . . 6
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (πΉ supp 0) β (β‘πΉ β β)) |
27 | | c0ex 11208 |
. . . . . . 7
β’ 0 β
V |
28 | 27 | a1i 11 |
. . . . . 6
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β 0 β
V) |
29 | 13, 26, 15, 28 | suppssrg 8182 |
. . . . 5
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΉβπ₯) = 0) |
30 | 22, 29 | breqtrd 5175 |
. . . 4
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β€ 0) |
31 | | ffvelcdm 7084 |
. . . . . 6
β’ ((πΊ:πΌβΆβ0 β§ π₯ β πΌ) β (πΊβπ₯) β
β0) |
32 | 5, 8, 31 | syl2an 597 |
. . . . 5
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β
β0) |
33 | 32 | nn0ge0d 12535 |
. . . 4
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β 0 β€ (πΊβπ₯)) |
34 | 32 | nn0red 12533 |
. . . . 5
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) β β) |
35 | | 0re 11216 |
. . . . 5
β’ 0 β
β |
36 | | letri3 11299 |
. . . . 5
β’ (((πΊβπ₯) β β β§ 0 β β)
β ((πΊβπ₯) = 0 β ((πΊβπ₯) β€ 0 β§ 0 β€ (πΊβπ₯)))) |
37 | 34, 35, 36 | sylancl 587 |
. . . 4
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β ((πΊβπ₯) = 0 β ((πΊβπ₯) β€ 0 β§ 0 β€ (πΊβπ₯)))) |
38 | 30, 33, 37 | mpbir2and 712 |
. . 3
β’ (((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΊβπ₯) = 0) |
39 | 5, 38 | suppss 8179 |
. 2
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (πΊ supp 0) β (β‘πΉ β β)) |
40 | 7, 39 | eqsstrrd 4022 |
1
β’ ((πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ) β (β‘πΊ β β) β (β‘πΉ β β)) |