Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β π) |
2 | | stoweidlem15.3 |
. . . . . 6
β’ (π β πΊ:(1...π)βΆπ) |
3 | 2 | ffvelcdmda 7086 |
. . . . 5
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ) β π) |
4 | | elrabi 3677 |
. . . . . 6
β’ ((πΊβπΌ) β {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} β (πΊβπΌ) β π΄) |
5 | | stoweidlem15.1 |
. . . . . 6
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
6 | 4, 5 | eleq2s 2851 |
. . . . 5
β’ ((πΊβπΌ) β π β (πΊβπΌ) β π΄) |
7 | 3, 6 | syl 17 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ) β π΄) |
8 | | eleq1 2821 |
. . . . . . . 8
β’ (π = (πΊβπΌ) β (π β π΄ β (πΊβπΌ) β π΄)) |
9 | 8 | anbi2d 629 |
. . . . . . 7
β’ (π = (πΊβπΌ) β ((π β§ π β π΄) β (π β§ (πΊβπΌ) β π΄))) |
10 | | feq1 6698 |
. . . . . . 7
β’ (π = (πΊβπΌ) β (π:πβΆβ β (πΊβπΌ):πβΆβ)) |
11 | 9, 10 | imbi12d 344 |
. . . . . 6
β’ (π = (πΊβπΌ) β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ (πΊβπΌ) β π΄) β (πΊβπΌ):πβΆβ))) |
12 | | stoweidlem15.4 |
. . . . . 6
β’ ((π β§ π β π΄) β π:πβΆβ) |
13 | 11, 12 | vtoclg 3556 |
. . . . 5
β’ ((πΊβπΌ) β π΄ β ((π β§ (πΊβπΌ) β π΄) β (πΊβπΌ):πβΆβ)) |
14 | 7, 13 | syl 17 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β ((π β§ (πΊβπΌ) β π΄) β (πΊβπΌ):πβΆβ)) |
15 | 1, 7, 14 | mp2and 697 |
. . 3
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ):πβΆβ) |
16 | 15 | ffvelcdmda 7086 |
. 2
β’ (((π β§ πΌ β (1...π)) β§ π β π) β ((πΊβπΌ)βπ) β β) |
17 | 3, 5 | eleqtrdi 2843 |
. . . . . . 7
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ) β {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))}) |
18 | | fveq1 6890 |
. . . . . . . . . 10
β’ (β = (πΊβπΌ) β (ββπ) = ((πΊβπΌ)βπ)) |
19 | 18 | eqeq1d 2734 |
. . . . . . . . 9
β’ (β = (πΊβπΌ) β ((ββπ) = 0 β ((πΊβπΌ)βπ) = 0)) |
20 | | fveq1 6890 |
. . . . . . . . . . . 12
β’ (β = (πΊβπΌ) β (ββπ‘) = ((πΊβπΌ)βπ‘)) |
21 | 20 | breq2d 5160 |
. . . . . . . . . . 11
β’ (β = (πΊβπΌ) β (0 β€ (ββπ‘) β 0 β€ ((πΊβπΌ)βπ‘))) |
22 | 20 | breq1d 5158 |
. . . . . . . . . . 11
β’ (β = (πΊβπΌ) β ((ββπ‘) β€ 1 β ((πΊβπΌ)βπ‘) β€ 1)) |
23 | 21, 22 | anbi12d 631 |
. . . . . . . . . 10
β’ (β = (πΊβπΌ) β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
24 | 23 | ralbidv 3177 |
. . . . . . . . 9
β’ (β = (πΊβπΌ) β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
25 | 19, 24 | anbi12d 631 |
. . . . . . . 8
β’ (β = (πΊβπΌ) β (((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)) β (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)))) |
26 | 25 | elrab 3683 |
. . . . . . 7
β’ ((πΊβπΌ) β {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} β ((πΊβπΌ) β π΄ β§ (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)))) |
27 | 17, 26 | sylib 217 |
. . . . . 6
β’ ((π β§ πΌ β (1...π)) β ((πΊβπΌ) β π΄ β§ (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)))) |
28 | 27 | simprd 496 |
. . . . 5
β’ ((π β§ πΌ β (1...π)) β (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
29 | 28 | simprd 496 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)) |
30 | | fveq2 6891 |
. . . . . . . 8
β’ (π = π‘ β ((πΊβπΌ)βπ ) = ((πΊβπΌ)βπ‘)) |
31 | 30 | breq2d 5160 |
. . . . . . 7
β’ (π = π‘ β (0 β€ ((πΊβπΌ)βπ ) β 0 β€ ((πΊβπΌ)βπ‘))) |
32 | 30 | breq1d 5158 |
. . . . . . 7
β’ (π = π‘ β (((πΊβπΌ)βπ ) β€ 1 β ((πΊβπΌ)βπ‘) β€ 1)) |
33 | 31, 32 | anbi12d 631 |
. . . . . 6
β’ (π = π‘ β ((0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
34 | 33 | cbvralvw 3234 |
. . . . 5
β’
(βπ β
π (0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)) |
35 | | fveq2 6891 |
. . . . . . . 8
β’ (π = π β ((πΊβπΌ)βπ ) = ((πΊβπΌ)βπ)) |
36 | 35 | breq2d 5160 |
. . . . . . 7
β’ (π = π β (0 β€ ((πΊβπΌ)βπ ) β 0 β€ ((πΊβπΌ)βπ))) |
37 | 35 | breq1d 5158 |
. . . . . . 7
β’ (π = π β (((πΊβπΌ)βπ ) β€ 1 β ((πΊβπΌ)βπ) β€ 1)) |
38 | 36, 37 | anbi12d 631 |
. . . . . 6
β’ (π = π β ((0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1))) |
39 | 38 | rspccva 3611 |
. . . . 5
β’
((βπ β
π (0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β§ π β π) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |
40 | 34, 39 | sylanbr 582 |
. . . 4
β’
((βπ‘ β
π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1) β§ π β π) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |
41 | 29, 40 | sylan 580 |
. . 3
β’ (((π β§ πΌ β (1...π)) β§ π β π) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |
42 | 41 | simpld 495 |
. 2
β’ (((π β§ πΌ β (1...π)) β§ π β π) β 0 β€ ((πΊβπΌ)βπ)) |
43 | 41 | simprd 496 |
. 2
β’ (((π β§ πΌ β (1...π)) β§ π β π) β ((πΊβπΌ)βπ) β€ 1) |
44 | 16, 42, 43 | 3jca 1128 |
1
β’ (((π β§ πΌ β (1...π)) β§ π β π) β (((πΊβπΌ)βπ) β β β§ 0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |