Step | Hyp | Ref
| Expression |
1 | | metnrmlem.g |
. . . 4
β’ πΊ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
2 | | metdscn.j |
. . . 4
β’ π½ = (MetOpenβπ·) |
3 | | metnrmlem.1 |
. . . 4
β’ (π β π· β (βMetβπ)) |
4 | | metnrmlem.3 |
. . . 4
β’ (π β π β (Clsdβπ½)) |
5 | | metnrmlem.2 |
. . . 4
β’ (π β π β (Clsdβπ½)) |
6 | | incom 4166 |
. . . . 5
β’ (π β© π) = (π β© π) |
7 | | metnrmlem.4 |
. . . . 5
β’ (π β (π β© π) = β
) |
8 | 6, 7 | eqtrid 2789 |
. . . 4
β’ (π β (π β© π) = β
) |
9 | | metnrmlem.v |
. . . 4
β’ π = βͺ π β π (π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) |
10 | 1, 2, 3, 4, 5, 8, 9 | metnrmlem2 24239 |
. . 3
β’ (π β (π β π½ β§ π β π)) |
11 | 10 | simpld 496 |
. 2
β’ (π β π β π½) |
12 | | metdscn.f |
. . . 4
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
13 | | metnrmlem.u |
. . . 4
β’ π = βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) |
14 | 12, 2, 3, 5, 4, 7, 13 | metnrmlem2 24239 |
. . 3
β’ (π β (π β π½ β§ π β π)) |
15 | 14 | simpld 496 |
. 2
β’ (π β π β π½) |
16 | 10 | simprd 497 |
. 2
β’ (π β π β π) |
17 | 14 | simprd 497 |
. 2
β’ (π β π β π) |
18 | 9 | ineq1i 4173 |
. . . 4
β’ (π β© π) = (βͺ
π β π (π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) |
19 | | iunin1 5037 |
. . . 4
β’ βͺ π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) = (βͺ
π β π (π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) |
20 | 18, 19 | eqtr4i 2768 |
. . 3
β’ (π β© π) = βͺ
π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) |
21 | 13 | ineq2i 4174 |
. . . . . . . 8
β’ ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) = ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
22 | | iunin2 5036 |
. . . . . . . 8
β’ βͺ π‘ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) = ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
23 | 21, 22 | eqtr4i 2768 |
. . . . . . 7
β’ ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) = βͺ
π‘ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
24 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π‘ β π)) β π· β (βMetβπ)) |
25 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π½ =
βͺ π½ |
26 | 25 | cldss 22396 |
. . . . . . . . . . . . . . . 16
β’ (π β (Clsdβπ½) β π β βͺ π½) |
27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β βͺ π½) |
28 | 2 | mopnuni 23810 |
. . . . . . . . . . . . . . . 16
β’ (π· β (βMetβπ) β π = βͺ π½) |
29 | 3, 28 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π = βͺ π½) |
30 | 27, 29 | sseqtrrd 3990 |
. . . . . . . . . . . . . 14
β’ (π β π β π) |
31 | 30 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β π) |
32 | 31 | adantrr 716 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π‘ β π)) β π β π) |
33 | 25 | cldss 22396 |
. . . . . . . . . . . . . . . 16
β’ (π β (Clsdβπ½) β π β βͺ π½) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β βͺ π½) |
35 | 34, 29 | sseqtrrd 3990 |
. . . . . . . . . . . . . 14
β’ (π β π β π) |
36 | 35 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β π‘ β π) |
37 | 36 | adantrl 715 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π‘ β π)) β π‘ β π) |
38 | 1, 2, 3, 4, 5, 8 | metnrmlem1a 24237 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (0 < (πΊβπ ) β§ if(1 β€ (πΊβπ ), 1, (πΊβπ )) β
β+)) |
39 | 38 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β
β+) |
40 | 39 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β
β+) |
41 | 40 | rphalfcld 12976 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) β
β+) |
42 | 41 | rpxrd 12965 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) β
β*) |
43 | 12, 2, 3, 5, 4, 7 | metnrmlem1a 24237 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π‘ β π) β (0 < (πΉβπ‘) β§ if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β
β+)) |
44 | 43 | adantrl 715 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β (0 < (πΉβπ‘) β§ if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β
β+)) |
45 | 44 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β
β+) |
46 | 45 | rphalfcld 12976 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β
β+) |
47 | 46 | rpxrd 12965 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β
β*) |
48 | 40 | rpred 12964 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β β) |
49 | 48 | rehalfcld 12407 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) β β) |
50 | 45 | rpred 12964 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β β) |
51 | 50 | rehalfcld 12407 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β β) |
52 | 49, 51 | rexaddd 13160 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) +π (if(1 β€
(πΉβπ‘), 1, (πΉβπ‘)) / 2)) = ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) + (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
53 | 48 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β β) |
54 | 50 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β β) |
55 | | 2cnd 12238 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β 2 β β) |
56 | | 2ne0 12264 |
. . . . . . . . . . . . . . . 16
β’ 2 β
0 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β 2 β 0) |
58 | 53, 54, 55, 57 | divdird 11976 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) = ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) + (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
59 | 52, 58 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) +π (if(1 β€
(πΉβπ‘), 1, (πΉβπ‘)) / 2)) = ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) |
60 | 1, 2, 3, 4, 5, 8 | metnrmlem1 24238 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π‘ β π β§ π β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β€ (π‘π·π )) |
61 | 60 | ancom2s 649 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β€ (π‘π·π )) |
62 | | xmetsym 23716 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (βMetβπ) β§ π‘ β π β§ π β π) β (π‘π·π ) = (π π·π‘)) |
63 | 24, 37, 32, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β (π‘π·π ) = (π π·π‘)) |
64 | 61, 63 | breqtrd 5136 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β€ (π π·π‘)) |
65 | 12, 2, 3, 5, 4, 7 | metnrmlem1 24238 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β€ (π π·π‘)) |
66 | 40 | rpxrd 12965 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΊβπ ), 1, (πΊβπ )) β
β*) |
67 | 45 | rpxrd 12965 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β
β*) |
68 | | xmetcl 23700 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (βMetβπ) β§ π β π β§ π‘ β π) β (π π·π‘) β
β*) |
69 | 24, 32, 37, 68 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β (π π·π‘) β
β*) |
70 | | xle2add 13185 |
. . . . . . . . . . . . . . . . 17
β’ (((if(1
β€ (πΊβπ ), 1, (πΊβπ )) β β* β§ if(1 β€
(πΉβπ‘), 1, (πΉβπ‘)) β β*) β§ ((π π·π‘) β β* β§ (π π·π‘) β β*)) β ((if(1
β€ (πΊβπ ), 1, (πΊβπ )) β€ (π π·π‘) β§ if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β€ (π π·π‘)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) +π if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) β€ ((π π·π‘) +π (π π·π‘)))) |
71 | 66, 67, 69, 69, 70 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) β€ (π π·π‘) β§ if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β€ (π π·π‘)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) +π if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) β€ ((π π·π‘) +π (π π·π‘)))) |
72 | 64, 65, 71 | mp2and 698 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) +π if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) β€ ((π π·π‘) +π (π π·π‘))) |
73 | 48, 50 | readdcld 11191 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) β β) |
74 | 73 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) β β) |
75 | 74, 55, 57 | divcan2d 11940 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β (2 Β· ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) = (if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)))) |
76 | | 2re 12234 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
77 | 73 | rehalfcld 12407 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β β) |
78 | | rexmul 13197 |
. . . . . . . . . . . . . . . . 17
β’ ((2
β β β§ ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β β) β (2
Β·e ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) = (2 Β· ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2))) |
79 | 76, 77, 78 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β (2 Β·e ((if(1
β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) = (2 Β· ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2))) |
80 | 48, 50 | rexaddd 13160 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π‘ β π)) β (if(1 β€ (πΊβπ ), 1, (πΊβπ )) +π if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) = (if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)))) |
81 | 75, 79, 80 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β (2 Β·e ((if(1
β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) = (if(1 β€ (πΊβπ ), 1, (πΊβπ )) +π if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)))) |
82 | | x2times 13225 |
. . . . . . . . . . . . . . . 16
β’ ((π π·π‘) β β* β (2
Β·e (π π·π‘)) = ((π π·π‘) +π (π π·π‘))) |
83 | 69, 82 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β (2 Β·e (π π·π‘)) = ((π π·π‘) +π (π π·π‘))) |
84 | 72, 81, 83 | 3brtr4d 5142 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π‘ β π)) β (2 Β·e ((if(1
β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) β€ (2 Β·e (π π·π‘))) |
85 | 77 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β
β*) |
86 | | 2rp 12927 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β+ |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π‘ β π)) β 2 β
β+) |
88 | | xlemul2 13217 |
. . . . . . . . . . . . . . 15
β’ ((((if(1
β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β β* β§
(π π·π‘) β β* β§ 2 β
β+) β (((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β€ (π π·π‘) β (2 Β·e ((if(1 β€
(πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) β€ (2 Β·e (π π·π‘)))) |
89 | 85, 69, 87, 88 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π‘ β π)) β (((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β€ (π π·π‘) β (2 Β·e ((if(1 β€
(πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2)) β€ (2 Β·e (π π·π‘)))) |
90 | 84, 89 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) + if(1 β€ (πΉβπ‘), 1, (πΉβπ‘))) / 2) β€ (π π·π‘)) |
91 | 59, 90 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π‘ β π)) β ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) +π (if(1 β€
(πΉβπ‘), 1, (πΉβπ‘)) / 2)) β€ (π π·π‘)) |
92 | | bldisj 23767 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π β π β§ π‘ β π) β§ ((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) β β* β§
(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β β* β§
((if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2) +π (if(1 β€
(πΉβπ‘), 1, (πΉβπ‘)) / 2)) β€ (π π·π‘))) β ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) = β
) |
93 | 24, 32, 37, 42, 47, 91, 92 | syl33anc 1386 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π‘ β π)) β ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) = β
) |
94 | | eqimss 4005 |
. . . . . . . . . . 11
β’ (((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) = β
β ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
) |
95 | 93, 94 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π‘ β π)) β ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
) |
96 | 95 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π‘ β π) β ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
) |
97 | 96 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ π β π) β βπ‘ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
) |
98 | | iunss 5010 |
. . . . . . . 8
β’ (βͺ π‘ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
β
βπ‘ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
) |
99 | 97, 98 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β π) β βͺ
π‘ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) β β
) |
100 | 23, 99 | eqsstrid 3997 |
. . . . . 6
β’ ((π β§ π β π) β ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) β β
) |
101 | 100 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) β β
) |
102 | | iunss 5010 |
. . . . 5
β’ (βͺ π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) β β
β βπ β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) β β
) |
103 | 101, 102 | sylibr 233 |
. . . 4
β’ (π β βͺ π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) β β
) |
104 | | ss0 4363 |
. . . 4
β’ (βͺ π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) β β
β βͺ π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) = β
) |
105 | 103, 104 | syl 17 |
. . 3
β’ (π β βͺ π β π ((π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β© π) = β
) |
106 | 20, 105 | eqtrid 2789 |
. 2
β’ (π β (π β© π) = β
) |
107 | | sseq2 3975 |
. . . 4
β’ (π§ = π β (π β π§ β π β π)) |
108 | | ineq1 4170 |
. . . . 5
β’ (π§ = π β (π§ β© π€) = (π β© π€)) |
109 | 108 | eqeq1d 2739 |
. . . 4
β’ (π§ = π β ((π§ β© π€) = β
β (π β© π€) = β
)) |
110 | 107, 109 | 3anbi13d 1439 |
. . 3
β’ (π§ = π β ((π β π§ β§ π β π€ β§ (π§ β© π€) = β
) β (π β π β§ π β π€ β§ (π β© π€) = β
))) |
111 | | sseq2 3975 |
. . . 4
β’ (π€ = π β (π β π€ β π β π)) |
112 | | ineq2 4171 |
. . . . 5
β’ (π€ = π β (π β© π€) = (π β© π)) |
113 | 112 | eqeq1d 2739 |
. . . 4
β’ (π€ = π β ((π β© π€) = β
β (π β© π) = β
)) |
114 | 111, 113 | 3anbi23d 1440 |
. . 3
β’ (π€ = π β ((π β π β§ π β π€ β§ (π β© π€) = β
) β (π β π β§ π β π β§ (π β© π) = β
))) |
115 | 110, 114 | rspc2ev 3595 |
. 2
β’ ((π β π½ β§ π β π½ β§ (π β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π½ βπ€ β π½ (π β π§ β§ π β π€ β§ (π§ β© π€) = β
)) |
116 | 11, 15, 16, 17, 106, 115 | syl113anc 1383 |
1
β’ (π β βπ§ β π½ βπ€ β π½ (π β π§ β§ π β π€ β§ (π§ β© π€) = β
)) |