Step | Hyp | Ref
| Expression |
1 | | spheres.l |
. . 3
β’ π = (Sphereβπ) |
2 | 1 | a1i 11 |
. 2
β’ (π β π β π = (Sphereβπ)) |
3 | | df-sph 46717 |
. . 3
β’ Sphere =
(π€ β V β¦ (π₯ β (Baseβπ€), π β (0[,]+β) β¦ {π β (Baseβπ€) β£ (π(distβπ€)π₯) = π})) |
4 | | fveq2 6839 |
. . . . 5
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
5 | | spheres.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
6 | 5 | eqcomi 2746 |
. . . . . 6
β’
(Baseβπ) =
π΅ |
7 | 6 | a1i 11 |
. . . . 5
β’ (π€ = π β (Baseβπ) = π΅) |
8 | 4, 7 | eqtrd 2777 |
. . . 4
β’ (π€ = π β (Baseβπ€) = π΅) |
9 | | eqidd 2738 |
. . . 4
β’ (π€ = π β (0[,]+β) =
(0[,]+β)) |
10 | | fveq2 6839 |
. . . . . . . 8
β’ (π€ = π β (distβπ€) = (distβπ)) |
11 | | spheres.d |
. . . . . . . . . 10
β’ π· = (distβπ) |
12 | 11 | eqcomi 2746 |
. . . . . . . . 9
β’
(distβπ) =
π· |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ (π€ = π β (distβπ) = π·) |
14 | 10, 13 | eqtrd 2777 |
. . . . . . 7
β’ (π€ = π β (distβπ€) = π·) |
15 | 14 | oveqd 7368 |
. . . . . 6
β’ (π€ = π β (π(distβπ€)π₯) = (ππ·π₯)) |
16 | 15 | eqeq1d 2739 |
. . . . 5
β’ (π€ = π β ((π(distβπ€)π₯) = π β (ππ·π₯) = π)) |
17 | 8, 16 | rabeqbidv 3422 |
. . . 4
β’ (π€ = π β {π β (Baseβπ€) β£ (π(distβπ€)π₯) = π} = {π β π΅ β£ (ππ·π₯) = π}) |
18 | 8, 9, 17 | mpoeq123dv 7426 |
. . 3
β’ (π€ = π β (π₯ β (Baseβπ€), π β (0[,]+β) β¦ {π β (Baseβπ€) β£ (π(distβπ€)π₯) = π}) = (π₯ β π΅, π β (0[,]+β) β¦ {π β π΅ β£ (ππ·π₯) = π})) |
19 | | elex 3461 |
. . 3
β’ (π β π β π β V) |
20 | | fvex 6852 |
. . . . . 6
β’
(Baseβπ)
β V |
21 | 5, 20 | eqeltri 2834 |
. . . . 5
β’ π΅ β V |
22 | | ovex 7384 |
. . . . 5
β’
(0[,]+β) β V |
23 | 21, 22 | mpoex 8004 |
. . . 4
β’ (π₯ β π΅, π β (0[,]+β) β¦ {π β π΅ β£ (ππ·π₯) = π}) β V |
24 | 23 | a1i 11 |
. . 3
β’ (π β π β (π₯ β π΅, π β (0[,]+β) β¦ {π β π΅ β£ (ππ·π₯) = π}) β V) |
25 | 3, 18, 19, 24 | fvmptd3 6968 |
. 2
β’ (π β π β (Sphereβπ) = (π₯ β π΅, π β (0[,]+β) β¦ {π β π΅ β£ (ππ·π₯) = π})) |
26 | 2, 25 | eqtrd 2777 |
1
β’ (π β π β π = (π₯ β π΅, π β (0[,]+β) β¦ {π β π΅ β£ (ππ·π₯) = π})) |