| Step | Hyp | Ref
| Expression |
|---|
| 1 | | blssps 24240 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·) β§ π β π₯) β βπ β β+ (π(ballβπ·)π) β π₯) |
| 2 | | sstr 3982 |
. . . . . . . . 9
β’ (((π(ballβπ·)π) β π₯ β§ π₯ β π΄) β (π(ballβπ·)π) β π΄) |
| 3 | 2 | expcom 413 |
. . . . . . . 8
β’ (π₯ β π΄ β ((π(ballβπ·)π) β π₯ β (π(ballβπ·)π) β π΄)) |
| 4 | 3 | reximdv 3162 |
. . . . . . 7
β’ (π₯ β π΄ β (βπ β β+ (π(ballβπ·)π) β π₯ β βπ β β+ (π(ballβπ·)π) β π΄)) |
| 5 | 1, 4 | syl5com 31 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·) β§ π β π₯) β (π₯ β π΄ β βπ β β+ (π(ballβπ·)π) β π΄)) |
| 6 | 5 | 3expa 1115 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·)) β§ π β π₯) β (π₯ β π΄ β βπ β β+ (π(ballβπ·)π) β π΄)) |
| 7 | 6 | expimpd 453 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·)) β ((π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
| 8 | 7 | adantlr 712 |
. . 3
β’ (((π· β (PsMetβπ) β§ π β π) β§ π₯ β ran (ballβπ·)) β ((π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
| 9 | 8 | rexlimdva 3147 |
. 2
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
| 10 | | simpll 764 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π· β (PsMetβπ)) |
| 11 | | simplr 766 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β π) |
| 12 | | rpxr 12979 |
. . . . . 6
β’ (π β β+
β π β
β*) |
| 13 | 12 | ad2antrl 725 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β β*) |
| 14 | | blelrnps 24232 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β ran (ballβπ·)) |
| 15 | 10, 11, 13, 14 | syl3anc 1368 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β (π(ballβπ·)π) β ran (ballβπ·)) |
| 16 | | simprl 768 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β β+) |
| 17 | | blcntrps 24228 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π)) |
| 18 | 10, 11, 16, 17 | syl3anc 1368 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β (π(ballβπ·)π)) |
| 19 | | simprr 770 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β (π(ballβπ·)π) β π΄) |
| 20 | | eleq2 2814 |
. . . . . 6
β’ (π₯ = (π(ballβπ·)π) β (π β π₯ β π β (π(ballβπ·)π))) |
| 21 | | sseq1 3999 |
. . . . . 6
β’ (π₯ = (π(ballβπ·)π) β (π₯ β π΄ β (π(ballβπ·)π) β π΄)) |
| 22 | 20, 21 | anbi12d 630 |
. . . . 5
β’ (π₯ = (π(ballβπ·)π) β ((π β π₯ β§ π₯ β π΄) β (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π΄))) |
| 23 | 22 | rspcev 3604 |
. . . 4
β’ (((π(ballβπ·)π) β ran (ballβπ·) β§ (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π΄)) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) |
| 24 | 15, 18, 19, 23 | syl12anc 834 |
. . 3
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) |
| 25 | 24 | rexlimdvaa 3148 |
. 2
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ β β+ (π(ballβπ·)π) β π΄ β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄))) |
| 26 | 9, 25 | impbid 211 |
1
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
