Step | Hyp | Ref
| Expression |
1 | | blssps 23622 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·) β§ π β π₯) β βπ β β+ (π(ballβπ·)π) β π₯) |
2 | | sstr 3934 |
. . . . . . . . 9
β’ (((π(ballβπ·)π) β π₯ β§ π₯ β π΄) β (π(ballβπ·)π) β π΄) |
3 | 2 | expcom 415 |
. . . . . . . 8
β’ (π₯ β π΄ β ((π(ballβπ·)π) β π₯ β (π(ballβπ·)π) β π΄)) |
4 | 3 | reximdv 3164 |
. . . . . . 7
β’ (π₯ β π΄ β (βπ β β+ (π(ballβπ·)π) β π₯ β βπ β β+ (π(ballβπ·)π) β π΄)) |
5 | 1, 4 | syl5com 31 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·) β§ π β π₯) β (π₯ β π΄ β βπ β β+ (π(ballβπ·)π) β π΄)) |
6 | 5 | 3expa 1118 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·)) β§ π β π₯) β (π₯ β π΄ β βπ β β+ (π(ballβπ·)π) β π΄)) |
7 | 6 | expimpd 455 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π₯ β ran (ballβπ·)) β ((π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
8 | 7 | adantlr 713 |
. . 3
β’ (((π· β (PsMetβπ) β§ π β π) β§ π₯ β ran (ballβπ·)) β ((π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
9 | 8 | rexlimdva 3149 |
. 2
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
10 | | simpll 765 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π· β (PsMetβπ)) |
11 | | simplr 767 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β π) |
12 | | rpxr 12785 |
. . . . . 6
β’ (π β β+
β π β
β*) |
13 | 12 | ad2antrl 726 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β β*) |
14 | | blelrnps 23614 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β ran (ballβπ·)) |
15 | 10, 11, 13, 14 | syl3anc 1371 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β (π(ballβπ·)π) β ran (ballβπ·)) |
16 | | simprl 769 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β β+) |
17 | | blcntrps 23610 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π)) |
18 | 10, 11, 16, 17 | syl3anc 1371 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β (π(ballβπ·)π)) |
19 | | simprr 771 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β (π(ballβπ·)π) β π΄) |
20 | | eleq2 2825 |
. . . . . 6
β’ (π₯ = (π(ballβπ·)π) β (π β π₯ β π β (π(ballβπ·)π))) |
21 | | sseq1 3951 |
. . . . . 6
β’ (π₯ = (π(ballβπ·)π) β (π₯ β π΄ β (π(ballβπ·)π) β π΄)) |
22 | 20, 21 | anbi12d 632 |
. . . . 5
β’ (π₯ = (π(ballβπ·)π) β ((π β π₯ β§ π₯ β π΄) β (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π΄))) |
23 | 22 | rspcev 3566 |
. . . 4
β’ (((π(ballβπ·)π) β ran (ballβπ·) β§ (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π΄)) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) |
24 | 15, 18, 19, 23 | syl12anc 835 |
. . 3
β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) |
25 | 24 | rexlimdvaa 3150 |
. 2
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ β β+ (π(ballβπ·)π) β π΄ β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄))) |
26 | 9, 25 | impbid 211 |
1
β’ ((π· β (PsMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |