Step | Hyp | Ref
| Expression |
1 | | totbndbnd 36277 |
. 2
β’ (πΆ β (TotBndβπ΄) β πΆ β (Bndβπ΄)) |
2 | | bndmet 36269 |
. . . . 5
β’ (πΆ β (Bndβπ΄) β πΆ β (Metβπ΄)) |
3 | | 0totbnd 36261 |
. . . . 5
β’ (π΄ = β
β (πΆ β (TotBndβπ΄) β πΆ β (Metβπ΄))) |
4 | 2, 3 | syl5ibr 246 |
. . . 4
β’ (π΄ = β
β (πΆ β (Bndβπ΄) β πΆ β (TotBndβπ΄))) |
5 | 4 | a1i 11 |
. . 3
β’ (π β (π΄ = β
β (πΆ β (Bndβπ΄) β πΆ β (TotBndβπ΄)))) |
6 | | n0 4311 |
. . . 4
β’ (π΄ β β
β
βπ π β π΄) |
7 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β πΆ β (Bndβπ΄)) |
8 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (πXs(π₯ β πΌ β¦ (π
βπ₯))) = (πXs(π₯ β πΌ β¦ (π
βπ₯))) |
9 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
10 | | prdsbnd.v |
. . . . . . . . . . . 12
β’ π = (Baseβ(π
βπ₯)) |
11 | | prdsbnd.e |
. . . . . . . . . . . 12
β’ πΈ = ((distβ(π
βπ₯)) βΎ (π Γ π)) |
12 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(distβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) = (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
13 | | prdsbnd.s |
. . . . . . . . . . . 12
β’ (π β π β π) |
14 | | prdsbnd.i |
. . . . . . . . . . . 12
β’ (π β πΌ β Fin) |
15 | | fvexd 6862 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΌ) β (π
βπ₯) β V) |
16 | | prdsbnd2.e |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΌ) β πΈ β (Metβπ)) |
17 | 8, 9, 10, 11, 12, 13, 14, 15, 16 | prdsmet 23739 |
. . . . . . . . . . 11
β’ (π β (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) β (Metβ(Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))))) |
18 | | prdsbnd.d |
. . . . . . . . . . . 12
β’ π· = (distβπ) |
19 | | prdsbnd.y |
. . . . . . . . . . . . . 14
β’ π = (πXsπ
) |
20 | | prdsbnd.r |
. . . . . . . . . . . . . . . 16
β’ (π β π
Fn πΌ) |
21 | | dffn5 6906 |
. . . . . . . . . . . . . . . 16
β’ (π
Fn πΌ β π
= (π₯ β πΌ β¦ (π
βπ₯))) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β π
= (π₯ β πΌ β¦ (π
βπ₯))) |
23 | 22 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π β (πXsπ
) = (πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
24 | 19, 23 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ (π β π = (πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
25 | 24 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π β (distβπ) = (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
26 | 18, 25 | eqtrid 2789 |
. . . . . . . . . . 11
β’ (π β π· = (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
27 | | prdsbnd.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
28 | 24 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
29 | 27, 28 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ (π β π΅ = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
30 | 29 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π β (Metβπ΅) =
(Metβ(Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))))) |
31 | 17, 26, 30 | 3eltr4d 2853 |
. . . . . . . . . 10
β’ (π β π· β (Metβπ΅)) |
32 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β π· β (Metβπ΅)) |
33 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ πΆ β (Bndβπ΄)) β πΆ β (Bndβπ΄)) |
34 | | prdsbnd2.c |
. . . . . . . . . . . 12
β’ πΆ = (π· βΎ (π΄ Γ π΄)) |
35 | 34 | bnd2lem 36279 |
. . . . . . . . . . 11
β’ ((π· β (Metβπ΅) β§ πΆ β (Bndβπ΄)) β π΄ β π΅) |
36 | 31, 33, 35 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β π΄ β π΅) |
37 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β π β π΄) |
38 | 36, 37 | sseldd 3950 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β π β π΅) |
39 | 34 | ssbnd 36276 |
. . . . . . . . 9
β’ ((π· β (Metβπ΅) β§ π β π΅) β (πΆ β (Bndβπ΄) β βπ β β π΄ β (π(ballβπ·)π))) |
40 | 32, 38, 39 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β (πΆ β (Bndβπ΄) β βπ β β π΄ β (π(ballβπ·)π))) |
41 | 7, 40 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β βπ β β π΄ β (π(ballβπ·)π)) |
42 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π΄ β (π(ballβπ·)π)) |
43 | | xpss12 5653 |
. . . . . . . . . . 11
β’ ((π΄ β (π(ballβπ·)π) β§ π΄ β (π(ballβπ·)π)) β (π΄ Γ π΄) β ((π(ballβπ·)π) Γ (π(ballβπ·)π))) |
44 | 42, 42, 43 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β (π΄ Γ π΄) β ((π(ballβπ·)π) Γ (π(ballβπ·)π))) |
45 | 44 | resabs1d 5973 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β ((π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) βΎ (π΄ Γ π΄)) = (π· βΎ (π΄ Γ π΄))) |
46 | 45, 34 | eqtr4di 2795 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β ((π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) βΎ (π΄ Γ π΄)) = πΆ) |
47 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π) |
48 | 38 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π β π΅) |
49 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π β β) |
50 | 37 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π β π΄) |
51 | 42, 50 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π β (π(ballβπ·)π)) |
52 | 51 | ne0d 4300 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β (π(ballβπ·)π) β β
) |
53 | 31 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π· β (Metβπ΅)) |
54 | | metxmet 23703 |
. . . . . . . . . . . . . 14
β’ (π· β (Metβπ΅) β π· β (βMetβπ΅)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π· β (βMetβπ΅)) |
56 | 49 | rexrd 11212 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π β β*) |
57 | | xbln0 23783 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π β β*) β ((π(ballβπ·)π) β β
β 0 < π)) |
58 | 55, 48, 56, 57 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β ((π(ballβπ·)π) β β
β 0 < π)) |
59 | 52, 58 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β 0 < π) |
60 | 49, 59 | elrpd 12961 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β π β β+) |
61 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))) = (πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))) |
62 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (Baseβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) |
63 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβ((π¦
β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) = (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) |
64 | | eqid 2737 |
. . . . . . . . . . . 12
β’
((distβ((π¦
β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) βΎ ((Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) Γ (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)))) = ((distβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) βΎ ((Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) Γ (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)))) |
65 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(distβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (distβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) |
66 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β β+)) β π β π) |
67 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β β+)) β πΌ β Fin) |
68 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)) β V |
69 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (π
βπ¦) = (π
βπ₯)) |
70 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π₯ β (distβ(π
βπ¦)) = (distβ(π
βπ₯))) |
71 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π₯ β (Baseβ(π
βπ¦)) = (Baseβ(π
βπ₯))) |
72 | 71, 10 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π₯ β (Baseβ(π
βπ¦)) = π) |
73 | 72 | sqxpeqd 5670 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π₯ β ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦))) = (π Γ π)) |
74 | 70, 73 | reseq12d 5943 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π₯ β ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))) = ((distβ(π
βπ₯)) βΎ (π Γ π))) |
75 | 74, 11 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π₯ β ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))) = πΈ) |
76 | 75 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦))))) = (ballβπΈ)) |
77 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (πβπ¦) = (πβπ₯)) |
78 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β π = π) |
79 | 76, 77, 78 | oveq123d 7383 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π) = ((πβπ₯)(ballβπΈ)π)) |
80 | 69, 79 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)) = ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) |
81 | 80 | cbvmptv 5223 |
. . . . . . . . . . . . . 14
β’ (π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))) = (π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) |
82 | 68, 81 | fnmpti 6649 |
. . . . . . . . . . . . 13
β’ (π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))) Fn πΌ |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β β+)) β (π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))) Fn πΌ) |
84 | 16 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β πΈ β (Metβπ)) |
85 | | metxmet 23703 |
. . . . . . . . . . . . . . . 16
β’ (πΈ β (Metβπ) β πΈ β (βMetβπ)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
87 | 15 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ₯ β πΌ (π
βπ₯) β V) |
88 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β+)) β
βπ₯ β πΌ (π
βπ₯) β V) |
89 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β β+)) β π β π΅) |
90 | 29 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β β+)) β π΅ = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
91 | 89, 90 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β+)) β π β (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
92 | 8, 9, 66, 67, 88, 10, 91 | prdsbascl 17372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β+)) β
βπ₯ β πΌ (πβπ₯) β π) |
93 | 92 | r19.21bi 3237 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (πβπ₯) β π) |
94 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β π β β+) |
95 | 94 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β π β β) |
96 | | blbnd 36275 |
. . . . . . . . . . . . . . 15
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ π β β) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π))) |
97 | 86, 93, 95, 96 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π))) |
98 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ₯)(ballβπΈ)π) β V |
99 | | xpeq12 5663 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ = ((πβπ₯)(ballβπΈ)π) β§ π¦ = ((πβπ₯)(ballβπΈ)π)) β (π¦ Γ π¦) = (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) |
100 | 99 | anidms 568 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β (π¦ Γ π¦) = (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) |
101 | 100 | reseq2d 5942 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β (πΈ βΎ (π¦ Γ π¦)) = (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)))) |
102 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β (TotBndβπ¦) = (TotBndβ((πβπ₯)(ballβπΈ)π))) |
103 | 101, 102 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β ((πΈ βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (TotBndβ((πβπ₯)(ballβπΈ)π)))) |
104 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β (Bndβπ¦) = (Bndβ((πβπ₯)(ballβπΈ)π))) |
105 | 101, 104 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β ((πΈ βΎ (π¦ Γ π¦)) β (Bndβπ¦) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π)))) |
106 | 103, 105 | bibi12d 346 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β (((πΈ βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (πΈ βΎ (π¦ Γ π¦)) β (Bndβπ¦)) β ((πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (TotBndβ((πβπ₯)(ballβπΈ)π)) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π))))) |
107 | 106 | imbi2d 341 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = ((πβπ₯)(ballβπΈ)π) β (((π β§ π₯ β πΌ) β ((πΈ βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (πΈ βΎ (π¦ Γ π¦)) β (Bndβπ¦))) β ((π β§ π₯ β πΌ) β ((πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (TotBndβ((πβπ₯)(ballβπΈ)π)) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π)))))) |
108 | | prdsbnd2.m |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β πΌ) β ((πΈ βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (πΈ βΎ (π¦ Γ π¦)) β (Bndβπ¦))) |
109 | 98, 107, 108 | vtocl 3521 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΌ) β ((πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (TotBndβ((πβπ₯)(ballβπΈ)π)) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π)))) |
110 | 109 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (TotBndβ((πβπ₯)(ballβπΈ)π)) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (Bndβ((πβπ₯)(ballβπΈ)π)))) |
111 | 97, 110 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) β (TotBndβ((πβπ₯)(ballβπΈ)π))) |
112 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))) = (π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))) |
113 | 80, 112, 68 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β πΌ β ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯) = ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) |
114 | 113 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯) = ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) |
115 | 114 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (distβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) = (distβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)) = ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)) |
117 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(distβ(π
βπ₯)) = (distβ(π
βπ₯)) |
118 | 116, 117 | ressds 17298 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ₯)(ballβπΈ)π) β V β (distβ(π
βπ₯)) = (distβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
119 | 98, 118 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(distβ(π
βπ₯)) = (distβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) |
120 | 115, 119 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (distβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) = (distβ(π
βπ₯))) |
121 | 114 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) = (Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
122 | | rpxr 12931 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β+
β π β
β*) |
123 | 122 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β π΅ β§ π β β+)) β π β
β*) |
124 | 123 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β π β β*) |
125 | | blssm 23787 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ π β β*) β ((πβπ₯)(ballβπΈ)π) β π) |
126 | 86, 93, 124, 125 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((πβπ₯)(ballβπΈ)π) β π) |
127 | 116, 10 | ressbas2 17127 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ₯)(ballβπΈ)π) β π β ((πβπ₯)(ballβπΈ)π) = (Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((πβπ₯)(ballβπΈ)π) = (Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
129 | 121, 128 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) = ((πβπ₯)(ballβπΈ)π)) |
130 | 129 | sqxpeqd 5670 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) Γ (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯))) = (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) |
131 | 120, 130 | reseq12d 5943 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((distβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) βΎ ((Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) Γ (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)))) = ((distβ(π
βπ₯)) βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)))) |
132 | 11 | reseq1i 5938 |
. . . . . . . . . . . . . . 15
β’ (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) = (((distβ(π
βπ₯)) βΎ (π Γ π)) βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) |
133 | | xpss12 5653 |
. . . . . . . . . . . . . . . . 17
β’ ((((πβπ₯)(ballβπΈ)π) β π β§ ((πβπ₯)(ballβπΈ)π) β π) β (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)) β (π Γ π)) |
134 | 126, 126,
133 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)) β (π Γ π)) |
135 | 134 | resabs1d 5973 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (((distβ(π
βπ₯)) βΎ (π Γ π)) βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) = ((distβ(π
βπ₯)) βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)))) |
136 | 132, 135 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π))) = ((distβ(π
βπ₯)) βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)))) |
137 | 131, 136 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((distβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) βΎ ((Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) Γ (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)))) = (πΈ βΎ (((πβπ₯)(ballβπΈ)π) Γ ((πβπ₯)(ballβπΈ)π)))) |
138 | 129 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (TotBndβ(Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯))) = (TotBndβ((πβπ₯)(ballβπΈ)π))) |
139 | 111, 137,
138 | 3eltr4d 2853 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((distβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) βΎ ((Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)) Γ (Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)))) β (TotBndβ(Baseβ((π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))βπ₯)))) |
140 | 61, 62, 63, 64, 65, 66, 67, 83, 139 | prdstotbnd 36282 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β β+)) β
(distβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) β (TotBndβ(Baseβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))))) |
141 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β β+)) β π = (πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
142 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β β+)) β (πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) = (πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) |
143 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) = (Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) |
144 | 81 | oveq2i 7373 |
. . . . . . . . . . . . . 14
β’ (πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))) = (πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
145 | 144 | fveq2i 6850 |
. . . . . . . . . . . . 13
β’
(distβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (distβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) |
146 | | fvexd 6862 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β (π
βπ₯) β V) |
147 | 98 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((πβπ₯)(ballβπΈ)π) β V) |
148 | 141, 142,
143, 18, 145, 66, 66, 67, 146, 147 | ressprdsds 23740 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β β+)) β
(distβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (π· βΎ ((Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) Γ (Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))))))) |
149 | 128 | ixpeq2dva 8857 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β β+)) β Xπ₯ β
πΌ ((πβπ₯)(ballβπΈ)π) = Xπ₯ β πΌ (Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
150 | 69 | cbvmptv 5223 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β πΌ β¦ (π
βπ¦)) = (π₯ β πΌ β¦ (π
βπ₯)) |
151 | 150 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πXs(π¦ β πΌ β¦ (π
βπ¦))) = (πXs(π₯ β πΌ β¦ (π
βπ₯))) |
152 | 24, 151 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π = (πXs(π¦ β πΌ β¦ (π
βπ¦)))) |
153 | 152 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (distβπ) = (distβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
154 | 18, 153 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π· = (distβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
155 | 154 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π β (ballβπ·) =
(ballβ(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))))) |
156 | 155 | oveqdr 7390 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β+)) β (π(ballβπ·)π) = (π(ballβ(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))))π)) |
157 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) |
158 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) = (distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) |
159 | 152 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Baseβπ) = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
160 | 27, 159 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
161 | 160 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β β+)) β π΅ = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
162 | 89, 161 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β+)) β π β (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
163 | | rpgt0 12934 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β 0 < π) |
164 | 163 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β+)) β 0 <
π) |
165 | 151, 157,
10, 11, 158, 66, 67, 146, 86, 162, 123, 164 | prdsbl 23863 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β+)) β (π(ballβ(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))))π) = Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π)) |
166 | 156, 165 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β β+)) β (π(ballβπ·)π) = Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π)) |
167 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) = (πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
168 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β β+)) β§ π₯ β πΌ) β ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)) β V) |
169 | 168 | ralrimiva 3144 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β+)) β
βπ₯ β πΌ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)) β V) |
170 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) = (Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))) |
171 | 167, 143,
66, 67, 169, 170 | prdsbas3 17370 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β β+)) β
(Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) = Xπ₯ β πΌ (Baseβ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))) |
172 | 149, 166,
171 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β β+)) β
(Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) = (π(ballβπ·)π)) |
173 | 172 | sqxpeqd 5670 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β β+)) β
((Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) Γ (Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π)))))) = ((π(ballβπ·)π) Γ (π(ballβπ·)π))) |
174 | 173 | reseq2d 5942 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β β+)) β (π· βΎ ((Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) Γ (Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))))) = (π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π)))) |
175 | 148, 174 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β β+)) β
(distβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π)))) |
176 | 144 | fveq2i 6850 |
. . . . . . . . . . . . 13
β’
(Baseβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (Baseβ(πXs(π₯ β πΌ β¦ ((π
βπ₯) βΎs ((πβπ₯)(ballβπΈ)π))))) |
177 | 176, 172 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β β+)) β
(Baseβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π))))) = (π(ballβπ·)π)) |
178 | 177 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β β+)) β
(TotBndβ(Baseβ(πXs(π¦ β πΌ β¦ ((π
βπ¦) βΎs ((πβπ¦)(ballβ((distβ(π
βπ¦)) βΎ ((Baseβ(π
βπ¦)) Γ (Baseβ(π
βπ¦)))))π)))))) = (TotBndβ(π(ballβπ·)π))) |
179 | 140, 175,
178 | 3eltr3d 2852 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β β+)) β (π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) β (TotBndβ(π(ballβπ·)π))) |
180 | 47, 48, 60, 179 | syl12anc 836 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β (π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) β (TotBndβ(π(ballβπ·)π))) |
181 | | totbndss 36265 |
. . . . . . . . 9
β’ (((π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) β (TotBndβ(π(ballβπ·)π)) β§ π΄ β (π(ballβπ·)π)) β ((π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) βΎ (π΄ Γ π΄)) β (TotBndβπ΄)) |
182 | 180, 42, 181 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β ((π· βΎ ((π(ballβπ·)π) Γ (π(ballβπ·)π))) βΎ (π΄ Γ π΄)) β (TotBndβπ΄)) |
183 | 46, 182 | eqeltrrd 2839 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β§ (π β β β§ π΄ β (π(ballβπ·)π))) β πΆ β (TotBndβπ΄)) |
184 | 41, 183 | rexlimddv 3159 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ πΆ β (Bndβπ΄))) β πΆ β (TotBndβπ΄)) |
185 | 184 | exp32 422 |
. . . . 5
β’ (π β (π β π΄ β (πΆ β (Bndβπ΄) β πΆ β (TotBndβπ΄)))) |
186 | 185 | exlimdv 1937 |
. . . 4
β’ (π β (βπ π β π΄ β (πΆ β (Bndβπ΄) β πΆ β (TotBndβπ΄)))) |
187 | 6, 186 | biimtrid 241 |
. . 3
β’ (π β (π΄ β β
β (πΆ β (Bndβπ΄) β πΆ β (TotBndβπ΄)))) |
188 | 5, 187 | pm2.61dne 3032 |
. 2
β’ (π β (πΆ β (Bndβπ΄) β πΆ β (TotBndβπ΄))) |
189 | 1, 188 | impbid2 225 |
1
β’ (π β (πΆ β (TotBndβπ΄) β πΆ β (Bndβπ΄))) |