Step | Hyp | Ref
| Expression |
1 | | rrxspheres.e |
. . . . . 6
β’ πΈ = (β^βπΌ) |
2 | 1 | fvexi 6852 |
. . . . 5
β’ πΈ β V |
3 | | rrxspheres.p |
. . . . . . . . . 10
β’ π = (β βm
πΌ) |
4 | | id 22 |
. . . . . . . . . . 11
β’ (πΌ β Fin β πΌ β Fin) |
5 | | eqid 2738 |
. . . . . . . . . . 11
β’
(BaseβπΈ) =
(BaseβπΈ) |
6 | 4, 1, 5 | rrxbasefi 24696 |
. . . . . . . . . 10
β’ (πΌ β Fin β
(BaseβπΈ) = (β
βm πΌ)) |
7 | 3, 6 | eqtr4id 2797 |
. . . . . . . . 9
β’ (πΌ β Fin β π = (BaseβπΈ)) |
8 | 7 | eleq2d 2824 |
. . . . . . . 8
β’ (πΌ β Fin β (π β π β π β (BaseβπΈ))) |
9 | 8 | biimpa 478 |
. . . . . . 7
β’ ((πΌ β Fin β§ π β π) β π β (BaseβπΈ)) |
10 | 9 | 3adant3 1133 |
. . . . . 6
β’ ((πΌ β Fin β§ π β π β§ π
β β) β π β (BaseβπΈ)) |
11 | 10 | adantl 483 |
. . . . 5
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β π β (BaseβπΈ)) |
12 | | rexr 11135 |
. . . . . . . . 9
β’ (π
β β β π
β
β*) |
13 | 12 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π β π β§ π
β β) β π
β
β*) |
14 | 13 | anim2i 618 |
. . . . . . 7
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β (0 β€ π
β§ π
β
β*)) |
15 | 14 | ancomd 463 |
. . . . . 6
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β (π
β β* β§ 0 β€
π
)) |
16 | | elxrge0 13303 |
. . . . . 6
β’ (π
β (0[,]+β) β
(π
β
β* β§ 0 β€ π
)) |
17 | 15, 16 | sylibr 233 |
. . . . 5
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β π
β (0[,]+β)) |
18 | | rrxspheres.s |
. . . . . 6
β’ π = (SphereβπΈ) |
19 | | rrxspheres.d |
. . . . . 6
β’ π· = (distβπΈ) |
20 | 5, 18, 19 | sphere 46533 |
. . . . 5
β’ ((πΈ β V β§ π β (BaseβπΈ) β§ π
β (0[,]+β)) β (πππ
) = {π β (BaseβπΈ) β£ (ππ·π) = π
}) |
21 | 2, 11, 17, 20 | mp3an2i 1467 |
. . . 4
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β (πππ
) = {π β (BaseβπΈ) β£ (ππ·π) = π
}) |
22 | | simp1 1137 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π β π β§ π
β β) β πΌ β Fin) |
23 | 22, 1, 5 | rrxbasefi 24696 |
. . . . . . 7
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (BaseβπΈ) = (β βm
πΌ)) |
24 | 23, 3 | eqtr4di 2796 |
. . . . . 6
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (BaseβπΈ) = π) |
25 | 24 | adantl 483 |
. . . . 5
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β (BaseβπΈ) = π) |
26 | 25 | rabeqdv 3421 |
. . . 4
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β {π β (BaseβπΈ) β£ (ππ·π) = π
} = {π β π β£ (ππ·π) = π
}) |
27 | 21, 26 | eqtrd 2778 |
. . 3
β’ ((0 β€
π
β§ (πΌ β Fin β§ π β π β§ π
β β)) β (πππ
) = {π β π β£ (ππ·π) = π
}) |
28 | 27 | ex 414 |
. 2
β’ (0 β€
π
β ((πΌ β Fin β§ π β π β§ π
β β) β (πππ
) = {π β π β£ (ππ·π) = π
})) |
29 | 5, 18, 19 | spheres 46532 |
. . . . . . 7
β’ (πΈ β V β π = (π₯ β (BaseβπΈ), π β (0[,]+β) β¦ {π β (BaseβπΈ) β£ (ππ·π₯) = π})) |
30 | 2, 29 | ax-mp 5 |
. . . . . 6
β’ π = (π₯ β (BaseβπΈ), π β (0[,]+β) β¦ {π β (BaseβπΈ) β£ (ππ·π₯) = π}) |
31 | | fvex 6851 |
. . . . . . 7
β’
(BaseβπΈ)
β V |
32 | 31 | rabex 5288 |
. . . . . 6
β’ {π β (BaseβπΈ) β£ (ππ·π₯) = π} β V |
33 | 30, 32 | dmmpo 7992 |
. . . . 5
β’ dom π = ((BaseβπΈ) Γ
(0[,]+β)) |
34 | | 0xr 11136 |
. . . . . . . . . . 11
β’ 0 β
β* |
35 | | pnfxr 11143 |
. . . . . . . . . . 11
β’ +β
β β* |
36 | 34, 35 | pm3.2i 472 |
. . . . . . . . . 10
β’ (0 β
β* β§ +β β β*) |
37 | | elicc1 13237 |
. . . . . . . . . 10
β’ ((0
β β* β§ +β β β*) β
(π
β (0[,]+β)
β (π
β
β* β§ 0 β€ π
β§ π
β€ +β))) |
38 | 36, 37 | mp1i 13 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (π
β (0[,]+β) β (π
β β*
β§ 0 β€ π
β§ π
β€
+β))) |
39 | | simp2 1138 |
. . . . . . . . 9
β’ ((π
β β*
β§ 0 β€ π
β§ π
β€ +β) β 0 β€
π
) |
40 | 38, 39 | syl6bi 253 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (π
β (0[,]+β) β 0 β€ π
)) |
41 | 40 | con3d 152 |
. . . . . . 7
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (Β¬ 0 β€ π
β Β¬ π
β (0[,]+β))) |
42 | 41 | imp 408 |
. . . . . 6
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β Β¬ π
β (0[,]+β)) |
43 | 42 | intnand 490 |
. . . . 5
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β Β¬ (π β (BaseβπΈ) β§ π
β (0[,]+β))) |
44 | | ndmovg 7530 |
. . . . 5
β’ ((dom
π = ((BaseβπΈ) Γ (0[,]+β)) β§
Β¬ (π β
(BaseβπΈ) β§ π
β (0[,]+β))) β
(πππ
) = β
) |
45 | 33, 43, 44 | sylancr 588 |
. . . 4
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β (πππ
) = β
) |
46 | 1 | fveq2i 6841 |
. . . . . . . . . . . . . . . 16
β’
(distβπΈ) =
(distβ(β^βπΌ)) |
47 | 19, 46 | eqtri 2766 |
. . . . . . . . . . . . . . 15
β’ π· =
(distβ(β^βπΌ)) |
48 | 47 | rrxmetfi 24698 |
. . . . . . . . . . . . . 14
β’ (πΌ β Fin β π· β (Metβ(β
βm πΌ))) |
49 | 48 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((πΌ β Fin β§ π β π β§ π
β β) β π· β (Metβ(β
βm πΌ))) |
50 | 49 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β π· β (Metβ(β
βm πΌ))) |
51 | 3 | fveq2i 6841 |
. . . . . . . . . . . 12
β’
(Metβπ) =
(Metβ(β βm πΌ)) |
52 | 50, 51 | eleqtrrdi 2850 |
. . . . . . . . . . 11
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β π· β (Metβπ)) |
53 | | simpr 486 |
. . . . . . . . . . 11
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β π β π) |
54 | | simp2 1138 |
. . . . . . . . . . . 12
β’ ((πΌ β Fin β§ π β π β§ π
β β) β π β π) |
55 | 54 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β π β π) |
56 | | metge0 23620 |
. . . . . . . . . . 11
β’ ((π· β (Metβπ) β§ π β π β§ π β π) β 0 β€ (ππ·π)) |
57 | 52, 53, 55, 56 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β 0 β€ (ππ·π)) |
58 | | breq2 5108 |
. . . . . . . . . 10
β’ ((ππ·π) = π
β (0 β€ (ππ·π) β 0 β€ π
)) |
59 | 57, 58 | syl5ibcom 245 |
. . . . . . . . 9
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β ((ππ·π) = π
β 0 β€ π
)) |
60 | 59 | con3d 152 |
. . . . . . . 8
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ π β π) β (Β¬ 0 β€ π
β Β¬ (ππ·π) = π
)) |
61 | 60 | impancom 453 |
. . . . . . 7
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β (π β π β Β¬ (ππ·π) = π
)) |
62 | 61 | imp 408 |
. . . . . 6
β’ ((((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β§ π β π) β Β¬ (ππ·π) = π
) |
63 | 62 | ralrimiva 3142 |
. . . . 5
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β βπ β π Β¬ (ππ·π) = π
) |
64 | | eqcom 2745 |
. . . . . 6
β’ (β
= {π β π β£ (ππ·π) = π
} β {π β π β£ (ππ·π) = π
} = β
) |
65 | | rabeq0 4343 |
. . . . . 6
β’ ({π β π β£ (ππ·π) = π
} = β
β βπ β π Β¬ (ππ·π) = π
) |
66 | 64, 65 | bitri 275 |
. . . . 5
β’ (β
= {π β π β£ (ππ·π) = π
} β βπ β π Β¬ (ππ·π) = π
) |
67 | 63, 66 | sylibr 233 |
. . . 4
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β β
= {π β π β£ (ππ·π) = π
}) |
68 | 45, 67 | eqtrd 2778 |
. . 3
β’ (((πΌ β Fin β§ π β π β§ π
β β) β§ Β¬ 0 β€ π
) β (πππ
) = {π β π β£ (ππ·π) = π
}) |
69 | 68 | expcom 415 |
. 2
β’ (Β¬ 0
β€ π
β ((πΌ β Fin β§ π β π β§ π
β β) β (πππ
) = {π β π β£ (ππ·π) = π
})) |
70 | 28, 69 | pm2.61i 182 |
1
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (πππ
) = {π β π β£ (ππ·π) = π
}) |