Step | Hyp | Ref
| Expression |
1 | | prdsbl.y |
. . . . . . . . 9
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
2 | | prdsbl.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
3 | | prdsbl.s |
. . . . . . . . 9
β’ (π β π β π) |
4 | | prdsbl.i |
. . . . . . . . 9
β’ (π β πΌ β Fin) |
5 | | prdsbl.r |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΌ) β π
β π) |
6 | 5 | ralrimiva 3147 |
. . . . . . . . 9
β’ (π β βπ₯ β πΌ π
β π) |
7 | | prdsbl.v |
. . . . . . . . 9
β’ π = (Baseβπ
) |
8 | 1, 2, 3, 4, 6, 7 | prdsbas3 17427 |
. . . . . . . 8
β’ (π β π΅ = Xπ₯ β πΌ π) |
9 | 8 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π β π΅ β π β Xπ₯ β πΌ π)) |
10 | 9 | biimpa 478 |
. . . . . 6
β’ ((π β§ π β π΅) β π β Xπ₯ β πΌ π) |
11 | | ixpfn 8897 |
. . . . . 6
β’ (π β Xπ₯ β
πΌ π β π Fn πΌ) |
12 | | vex 3479 |
. . . . . . . 8
β’ π β V |
13 | 12 | elixp 8898 |
. . . . . . 7
β’ (π β Xπ₯ β
πΌ ((πβπ₯)(ballβπΈ)π΄) β (π Fn πΌ β§ βπ₯ β πΌ (πβπ₯) β ((πβπ₯)(ballβπΈ)π΄))) |
14 | 13 | baib 537 |
. . . . . 6
β’ (π Fn πΌ β (π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄) β βπ₯ β πΌ (πβπ₯) β ((πβπ₯)(ballβπΈ)π΄))) |
15 | 10, 11, 14 | 3syl 18 |
. . . . 5
β’ ((π β§ π β π΅) β (π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄) β βπ₯ β πΌ (πβπ₯) β ((πβπ₯)(ballβπΈ)π΄))) |
16 | | prdsbl.m |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
17 | 16 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
18 | | prdsbl.a |
. . . . . . . 8
β’ (π β π΄ β
β*) |
19 | 18 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β π΄ β
β*) |
20 | | prdsbl.p |
. . . . . . . . . 10
β’ (π β π β π΅) |
21 | 1, 2, 3, 4, 6, 7, 20 | prdsbascl 17429 |
. . . . . . . . 9
β’ (π β βπ₯ β πΌ (πβπ₯) β π) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΅) β βπ₯ β πΌ (πβπ₯) β π) |
23 | 22 | r19.21bi 3249 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β (πβπ₯) β π) |
24 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β π) |
25 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β πΌ β Fin) |
26 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β βπ₯ β πΌ π
β π) |
27 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β π΅) |
28 | 1, 2, 24, 25, 26, 7, 27 | prdsbascl 17429 |
. . . . . . . 8
β’ ((π β§ π β π΅) β βπ₯ β πΌ (πβπ₯) β π) |
29 | 28 | r19.21bi 3249 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β (πβπ₯) β π) |
30 | | elbl2 23896 |
. . . . . . 7
β’ (((πΈ β (βMetβπ) β§ π΄ β β*) β§ ((πβπ₯) β π β§ (πβπ₯) β π)) β ((πβπ₯) β ((πβπ₯)(ballβπΈ)π΄) β ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
31 | 17, 19, 23, 29, 30 | syl22anc 838 |
. . . . . 6
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯) β ((πβπ₯)(ballβπΈ)π΄) β ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
32 | 31 | ralbidva 3176 |
. . . . 5
β’ ((π β§ π β π΅) β (βπ₯ β πΌ (πβπ₯) β ((πβπ₯)(ballβπΈ)π΄) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
33 | | xmetcl 23837 |
. . . . . . . . . 10
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ (πβπ₯) β π) β ((πβπ₯)πΈ(πβπ₯)) β
β*) |
34 | 17, 23, 29, 33 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β
β*) |
35 | 34 | ralrimiva 3147 |
. . . . . . . 8
β’ ((π β§ π β π΅) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β
β*) |
36 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) = (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) |
37 | | breq1 5152 |
. . . . . . . . 9
β’ (π§ = ((πβπ₯)πΈ(πβπ₯)) β (π§ < π΄ β ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
38 | 36, 37 | ralrnmptw 7096 |
. . . . . . . 8
β’
(βπ₯ β
πΌ ((πβπ₯)πΈ(πβπ₯)) β β* β
(βπ§ β ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ < π΄ β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
39 | 35, 38 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π΅) β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ < π΄ β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
40 | | prdsbl.g |
. . . . . . . . . 10
β’ (π β 0 < π΄) |
41 | 40 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β 0 < π΄) |
42 | | c0ex 11208 |
. . . . . . . . . 10
β’ 0 β
V |
43 | | breq1 5152 |
. . . . . . . . . 10
β’ (π§ = 0 β (π§ < π΄ β 0 < π΄)) |
44 | 42, 43 | ralsn 4686 |
. . . . . . . . 9
β’
(βπ§ β
{0}π§ < π΄ β 0 < π΄) |
45 | 41, 44 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ π β π΅) β βπ§ β {0}π§ < π΄) |
46 | | ralunb 4192 |
. . . . . . . . 9
β’
(βπ§ β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ < π΄ β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ < π΄ β§ βπ§ β {0}π§ < π΄)) |
47 | 20 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β π β π΅) |
48 | | prdsbl.e |
. . . . . . . . . . . 12
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
49 | | prdsbl.d |
. . . . . . . . . . . 12
β’ π· = (distβπ) |
50 | 1, 2, 24, 25, 26, 47, 27, 7, 48, 49 | prdsdsval3 17431 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β (ππ·π) = sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
51 | | xrltso 13120 |
. . . . . . . . . . . . 13
β’ < Or
β* |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β < Or
β*) |
53 | 36 | rnmpt 5955 |
. . . . . . . . . . . . . . 15
β’ ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) = {π¦ β£ βπ₯ β πΌ π¦ = ((πβπ₯)πΈ(πβπ₯))} |
54 | | abrexfi 9352 |
. . . . . . . . . . . . . . 15
β’ (πΌ β Fin β {π¦ β£ βπ₯ β πΌ π¦ = ((πβπ₯)πΈ(πβπ₯))} β Fin) |
55 | 53, 54 | eqeltrid 2838 |
. . . . . . . . . . . . . 14
β’ (πΌ β Fin β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin) |
56 | 25, 55 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin) |
57 | | snfi 9044 |
. . . . . . . . . . . . 13
β’ {0}
β Fin |
58 | | unfi 9172 |
. . . . . . . . . . . . 13
β’ ((ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β Fin β§ {0} β Fin) β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β Fin) |
59 | 56, 57, 58 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β Fin) |
60 | | ssun2 4174 |
. . . . . . . . . . . . . 14
β’ {0}
β (ran (π₯ β
πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) |
61 | 42 | snss 4790 |
. . . . . . . . . . . . . 14
β’ (0 β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β {0} β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
62 | 60, 61 | mpbir 230 |
. . . . . . . . . . . . 13
β’ 0 β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) |
63 | | ne0i 4335 |
. . . . . . . . . . . . 13
β’ (0 β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β
) |
64 | 62, 63 | mp1i 13 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β
) |
65 | 34 | fmpttd 7115 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))):πΌβΆβ*) |
66 | 65 | frnd 6726 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β
β*) |
67 | | 0xr 11261 |
. . . . . . . . . . . . . . 15
β’ 0 β
β* |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β 0 β
β*) |
69 | 68 | snssd 4813 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β {0} β
β*) |
70 | 66, 69 | unssd 4187 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
71 | | fisupcl 9464 |
. . . . . . . . . . . 12
β’ (( <
Or β* β§ ((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β Fin β§ (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β
β§ (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β*))
β sup((ran (π₯ β
πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
72 | 52, 59, 64, 70, 71 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
73 | 50, 72 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (ππ·π) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
74 | | breq1 5152 |
. . . . . . . . . . 11
β’ (π§ = (ππ·π) β (π§ < π΄ β (ππ·π) < π΄)) |
75 | 74 | rspcv 3609 |
. . . . . . . . . 10
β’ ((ππ·π) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β (βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ < π΄ β (ππ·π) < π΄)) |
76 | 73, 75 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ < π΄ β (ππ·π) < π΄)) |
77 | 46, 76 | biimtrrid 242 |
. . . . . . . 8
β’ ((π β§ π β π΅) β ((βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ < π΄ β§ βπ§ β {0}π§ < π΄) β (ππ·π) < π΄)) |
78 | 45, 77 | mpan2d 693 |
. . . . . . 7
β’ ((π β§ π β π΅) β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ < π΄ β (ππ·π) < π΄)) |
79 | 39, 78 | sylbird 260 |
. . . . . 6
β’ ((π β§ π β π΅) β (βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) < π΄ β (ππ·π) < π΄)) |
80 | | ssun1 4173 |
. . . . . . . . . . 11
β’ ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) |
81 | | ovex 7442 |
. . . . . . . . . . . . . 14
β’ ((πβπ₯)πΈ(πβπ₯)) β V |
82 | 81 | elabrex 7242 |
. . . . . . . . . . . . 13
β’ (π₯ β πΌ β ((πβπ₯)πΈ(πβπ₯)) β {π¦ β£ βπ₯ β πΌ π¦ = ((πβπ₯)πΈ(πβπ₯))}) |
83 | 82 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β {π¦ β£ βπ₯ β πΌ π¦ = ((πβπ₯)πΈ(πβπ₯))}) |
84 | 83, 53 | eleqtrrdi 2845 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))) |
85 | 80, 84 | sselid 3981 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) |
86 | | supxrub 13303 |
. . . . . . . . . 10
β’ (((ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β*
β§ ((πβπ₯)πΈ(πβπ₯)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})) β ((πβπ₯)πΈ(πβπ₯)) β€ sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
87 | 70, 85, 86 | syl2an2r 684 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β€ sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
88 | 50 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β (ππ·π) = sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
89 | 87, 88 | breqtrrd 5177 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β€ (ππ·π)) |
90 | 1, 2, 7, 48, 49, 3, 4, 5, 16 | prdsxmet 23875 |
. . . . . . . . . . 11
β’ (π β π· β (βMetβπ΅)) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β π· β (βMetβπ΅)) |
92 | 20 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β π β π΅) |
93 | 27 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β π β π΅) |
94 | | xmetcl 23837 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π β π΅) β (ππ·π) β
β*) |
95 | 91, 92, 93, 94 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β (ππ·π) β
β*) |
96 | | xrlelttr 13135 |
. . . . . . . . 9
β’ ((((πβπ₯)πΈ(πβπ₯)) β β* β§ (ππ·π) β β* β§ π΄ β β*)
β ((((πβπ₯)πΈ(πβπ₯)) β€ (ππ·π) β§ (ππ·π) < π΄) β ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
97 | 34, 95, 19, 96 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((((πβπ₯)πΈ(πβπ₯)) β€ (ππ·π) β§ (ππ·π) < π΄) β ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
98 | 89, 97 | mpand 694 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π₯ β πΌ) β ((ππ·π) < π΄ β ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
99 | 98 | ralrimdva 3155 |
. . . . . 6
β’ ((π β§ π β π΅) β ((ππ·π) < π΄ β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) < π΄)) |
100 | 79, 99 | impbid 211 |
. . . . 5
β’ ((π β§ π β π΅) β (βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) < π΄ β (ππ·π) < π΄)) |
101 | 15, 32, 100 | 3bitrrd 306 |
. . . 4
β’ ((π β§ π β π΅) β ((ππ·π) < π΄ β π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄))) |
102 | 101 | pm5.32da 580 |
. . 3
β’ (π β ((π β π΅ β§ (ππ·π) < π΄) β (π β π΅ β§ π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄)))) |
103 | | elbl 23894 |
. . . 4
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π΄ β β*) β (π β (π(ballβπ·)π΄) β (π β π΅ β§ (ππ·π) < π΄))) |
104 | 90, 20, 18, 103 | syl3anc 1372 |
. . 3
β’ (π β (π β (π(ballβπ·)π΄) β (π β π΅ β§ (ππ·π) < π΄))) |
105 | 21 | r19.21bi 3249 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β π) |
106 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β π΄ β
β*) |
107 | | blssm 23924 |
. . . . . . . . 9
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ π΄ β β*) β ((πβπ₯)(ballβπΈ)π΄) β π) |
108 | 16, 105, 106, 107 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β ((πβπ₯)(ballβπΈ)π΄) β π) |
109 | 108 | ralrimiva 3147 |
. . . . . . 7
β’ (π β βπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄) β π) |
110 | | ss2ixp 8904 |
. . . . . . 7
β’
(βπ₯ β
πΌ ((πβπ₯)(ballβπΈ)π΄) β π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄) β Xπ₯ β πΌ π) |
111 | 109, 110 | syl 17 |
. . . . . 6
β’ (π β Xπ₯ β
πΌ ((πβπ₯)(ballβπΈ)π΄) β Xπ₯ β πΌ π) |
112 | 111, 8 | sseqtrrd 4024 |
. . . . 5
β’ (π β Xπ₯ β
πΌ ((πβπ₯)(ballβπΈ)π΄) β π΅) |
113 | 112 | sseld 3982 |
. . . 4
β’ (π β (π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄) β π β π΅)) |
114 | 113 | pm4.71rd 564 |
. . 3
β’ (π β (π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄) β (π β π΅ β§ π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄)))) |
115 | 102, 104,
114 | 3bitr4d 311 |
. 2
β’ (π β (π β (π(ballβπ·)π΄) β π β Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄))) |
116 | 115 | eqrdv 2731 |
1
β’ (π β (π(ballβπ·)π΄) = Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄)) |