Step | Hyp | Ref
| Expression |
1 | | prdsdsf.b |
. . . 4
β’ π΅ = (Baseβπ) |
2 | 1 | fvexi 6852 |
. . 3
β’ π΅ β V |
3 | 2 | a1i 11 |
. 2
β’ (π β π΅ β V) |
4 | | prdsdsf.y |
. . . 4
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
5 | | prdsdsf.v |
. . . 4
β’ π = (Baseβπ
) |
6 | | prdsdsf.e |
. . . 4
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
7 | | prdsdsf.d |
. . . 4
β’ π· = (distβπ) |
8 | | prdsdsf.s |
. . . 4
β’ (π β π β π) |
9 | | prdsdsf.i |
. . . 4
β’ (π β πΌ β π) |
10 | | prdsdsf.r |
. . . 4
β’ ((π β§ π₯ β πΌ) β π
β π) |
11 | | prdsdsf.m |
. . . 4
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
12 | 4, 1, 5, 6, 7, 8, 9, 10, 11 | prdsdsf 23642 |
. . 3
β’ (π β π·:(π΅ Γ π΅)βΆ(0[,]+β)) |
13 | | iccssxr 13276 |
. . 3
β’
(0[,]+β) β β* |
14 | | fss 6681 |
. . 3
β’ ((π·:(π΅ Γ π΅)βΆ(0[,]+β) β§ (0[,]+β)
β β*) β π·:(π΅ Γ π΅)βΆβ*) |
15 | 12, 13, 14 | sylancl 587 |
. 2
β’ (π β π·:(π΅ Γ π΅)βΆβ*) |
16 | 12 | fovcdmda 7518 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππ·π) β (0[,]+β)) |
17 | | elxrge0 13303 |
. . . 4
β’ ((ππ·π) β (0[,]+β) β ((ππ·π) β β* β§ 0 β€
(ππ·π))) |
18 | 17 | simprbi 498 |
. . 3
β’ ((ππ·π) β (0[,]+β) β 0 β€ (ππ·π)) |
19 | 16, 18 | syl 17 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β 0 β€ (ππ·π)) |
20 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
21 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β πΌ β π) |
22 | 10 | ralrimiva 3142 |
. . . . . 6
β’ (π β βπ₯ β πΌ π
β π) |
23 | 22 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ π
β π) |
24 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
25 | | simprr 772 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
26 | 4, 1, 20, 21, 23, 24, 25, 5, 6, 7 | prdsdsval3 17302 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππ·π) = sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
27 | 26 | breq1d 5114 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((ππ·π) β€ 0 β sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β€ 0)) |
28 | 11 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
29 | 4, 1, 20, 21, 23, 5, 24 | prdsbascl 17300 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
30 | 29 | r19.21bi 3233 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (πβπ₯) β π) |
31 | 4, 1, 20, 21, 23, 5, 25 | prdsbascl 17300 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
32 | 31 | r19.21bi 3233 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (πβπ₯) β π) |
33 | | xmetcl 23606 |
. . . . . . . 8
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ (πβπ₯) β π) β ((πβπ₯)πΈ(πβπ₯)) β
β*) |
34 | 28, 30, 32, 33 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β
β*) |
35 | 34 | fmpttd 7058 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))):πΌβΆβ*) |
36 | 35 | frnd 6672 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) β
β*) |
37 | | 0xr 11136 |
. . . . . . 7
β’ 0 β
β* |
38 | 37 | a1i 11 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β 0 β
β*) |
39 | 38 | snssd 4768 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β {0} β
β*) |
40 | 36, 39 | unssd 4145 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
41 | | supxrleub 13174 |
. . . 4
β’ (((ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β*
β§ 0 β β*) β (sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β€ 0 β βπ§
β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ 0)) |
42 | 40, 37, 41 | sylancl 587 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β€ 0 β βπ§
β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ 0)) |
43 | | 0le0 12188 |
. . . . . . 7
β’ 0 β€
0 |
44 | | c0ex 11083 |
. . . . . . . 8
β’ 0 β
V |
45 | | breq1 5107 |
. . . . . . . 8
β’ (π§ = 0 β (π§ β€ 0 β 0 β€ 0)) |
46 | 44, 45 | ralsn 4641 |
. . . . . . 7
β’
(βπ§ β
{0}π§ β€ 0 β 0 β€
0) |
47 | 43, 46 | mpbir 230 |
. . . . . 6
β’
βπ§ β
{0}π§ β€
0 |
48 | | ralunb 4150 |
. . . . . 6
β’
(βπ§ β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ 0 β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ 0 β§ βπ§ β {0}π§ β€ 0)) |
49 | 47, 48 | mpbiran2 709 |
. . . . 5
β’
(βπ§ β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ 0 β βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ 0) |
50 | | ovex 7383 |
. . . . . . 7
β’ ((πβπ₯)πΈ(πβπ₯)) β V |
51 | 50 | rgenw 3067 |
. . . . . 6
β’
βπ₯ β
πΌ ((πβπ₯)πΈ(πβπ₯)) β V |
52 | | eqid 2738 |
. . . . . . 7
β’ (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) = (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) |
53 | | breq1 5107 |
. . . . . . 7
β’ (π§ = ((πβπ₯)πΈ(πβπ₯)) β (π§ β€ 0 β ((πβπ₯)πΈ(πβπ₯)) β€ 0)) |
54 | 52, 53 | ralrnmptw 7039 |
. . . . . 6
β’
(βπ₯ β
πΌ ((πβπ₯)πΈ(πβπ₯)) β V β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ 0 β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ 0)) |
55 | 51, 54 | ax-mp 5 |
. . . . 5
β’
(βπ§ β
ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ 0 β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ 0) |
56 | 49, 55 | bitri 275 |
. . . 4
β’
(βπ§ β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ 0 β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ 0) |
57 | | xmetge0 23619 |
. . . . . . . . 9
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ (πβπ₯) β π) β 0 β€ ((πβπ₯)πΈ(πβπ₯))) |
58 | 28, 30, 32, 57 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β 0 β€ ((πβπ₯)πΈ(πβπ₯))) |
59 | 58 | biantrud 533 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (((πβπ₯)πΈ(πβπ₯)) β€ 0 β (((πβπ₯)πΈ(πβπ₯)) β€ 0 β§ 0 β€ ((πβπ₯)πΈ(πβπ₯))))) |
60 | | xrletri3 13002 |
. . . . . . . 8
β’ ((((πβπ₯)πΈ(πβπ₯)) β β* β§ 0 β
β*) β (((πβπ₯)πΈ(πβπ₯)) = 0 β (((πβπ₯)πΈ(πβπ₯)) β€ 0 β§ 0 β€ ((πβπ₯)πΈ(πβπ₯))))) |
61 | 34, 37, 60 | sylancl 587 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (((πβπ₯)πΈ(πβπ₯)) = 0 β (((πβπ₯)πΈ(πβπ₯)) β€ 0 β§ 0 β€ ((πβπ₯)πΈ(πβπ₯))))) |
62 | | xmeteq0 23613 |
. . . . . . . 8
β’ ((πΈ β (βMetβπ) β§ (πβπ₯) β π β§ (πβπ₯) β π) β (((πβπ₯)πΈ(πβπ₯)) = 0 β (πβπ₯) = (πβπ₯))) |
63 | 28, 30, 32, 62 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (((πβπ₯)πΈ(πβπ₯)) = 0 β (πβπ₯) = (πβπ₯))) |
64 | 59, 61, 63 | 3bitr2d 307 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π₯ β πΌ) β (((πβπ₯)πΈ(πβπ₯)) β€ 0 β (πβπ₯) = (πβπ₯))) |
65 | 64 | ralbidva 3171 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ 0 β βπ₯ β πΌ (πβπ₯) = (πβπ₯))) |
66 | | eqid 2738 |
. . . . . . . . . 10
β’ (π₯ β πΌ β¦ π
) = (π₯ β πΌ β¦ π
) |
67 | 66 | fnmpt 6637 |
. . . . . . . . 9
β’
(βπ₯ β
πΌ π
β π β (π₯ β πΌ β¦ π
) Fn πΌ) |
68 | 22, 67 | syl 17 |
. . . . . . . 8
β’ (π β (π₯ β πΌ β¦ π
) Fn πΌ) |
69 | 68 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π₯ β πΌ β¦ π
) Fn πΌ) |
70 | 4, 1, 20, 21, 69, 24 | prdsbasfn 17288 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π Fn πΌ) |
71 | 4, 1, 20, 21, 69, 25 | prdsbasfn 17288 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β π Fn πΌ) |
72 | | eqfnfv 6978 |
. . . . . 6
β’ ((π Fn πΌ β§ π Fn πΌ) β (π = π β βπ₯ β πΌ (πβπ₯) = (πβπ₯))) |
73 | 70, 71, 72 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π = π β βπ₯ β πΌ (πβπ₯) = (πβπ₯))) |
74 | 65, 73 | bitr4d 282 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ 0 β π = π)) |
75 | 56, 74 | bitrid 283 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅)) β (βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ 0 β π = π)) |
76 | 27, 42, 75 | 3bitrd 305 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β ((ππ·π) β€ 0 β π = π)) |
77 | 26 | 3adantr3 1172 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅)) β (ππ·π) = sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
78 | 77 | 3adant3 1133 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (ππ·π) = sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
79 | 11 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
80 | 29 | 3adantr3 1172 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
81 | 80 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ₯ β πΌ (πβπ₯) β π) |
82 | 81 | r19.21bi 3233 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (πβπ₯) β π) |
83 | 31 | 3adantr3 1172 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
84 | 83 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ₯ β πΌ (πβπ₯) β π) |
85 | 84 | r19.21bi 3233 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (πβπ₯) β π) |
86 | 79, 82, 85, 33 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β
β*) |
87 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β π β π) |
88 | 9 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β πΌ β π) |
89 | 22 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ₯ β πΌ π
β π) |
90 | | simp23 1209 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β β β π΅) |
91 | 4, 1, 87, 88, 89, 5, 90 | prdsbascl 17300 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ₯ β πΌ (ββπ₯) β π) |
92 | 91 | r19.21bi 3233 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (ββπ₯) β π) |
93 | | xmetcl 23606 |
. . . . . . . . . . . 12
β’ ((πΈ β (βMetβπ) β§ (ββπ₯) β π β§ (πβπ₯) β π) β ((ββπ₯)πΈ(πβπ₯)) β
β*) |
94 | 79, 92, 82, 93 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β
β*) |
95 | | simp3l 1202 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ·π) β β) |
96 | 95 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (βπ·π) β β) |
97 | | xmetge0 23619 |
. . . . . . . . . . . 12
β’ ((πΈ β (βMetβπ) β§ (ββπ₯) β π β§ (πβπ₯) β π) β 0 β€ ((ββπ₯)πΈ(πβπ₯))) |
98 | 79, 92, 82, 97 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β 0 β€ ((ββπ₯)πΈ(πβπ₯))) |
99 | 94 | fmpttd 7058 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))):πΌβΆβ*) |
100 | 99 | frnd 6672 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) β
β*) |
101 | 37 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β 0 β
β*) |
102 | 101 | snssd 4768 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β {0} β
β*) |
103 | 100, 102 | unssd 4145 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
104 | | ssun1 4131 |
. . . . . . . . . . . . . 14
β’ ran
(π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}) |
105 | | ovex 7383 |
. . . . . . . . . . . . . . . . 17
β’ ((ββπ₯)πΈ(πβπ₯)) β V |
106 | 105 | elabrex 7185 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β πΌ β ((ββπ₯)πΈ(πβπ₯)) β {π§ β£ βπ₯ β πΌ π§ = ((ββπ₯)πΈ(πβπ₯))}) |
107 | 106 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β {π§ β£ βπ₯ β πΌ π§ = ((ββπ₯)πΈ(πβπ₯))}) |
108 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) = (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) |
109 | 108 | rnmpt 5907 |
. . . . . . . . . . . . . . 15
β’ ran
(π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) = {π§ β£ βπ₯ β πΌ π§ = ((ββπ₯)πΈ(πβπ₯))} |
110 | 107, 109 | eleqtrrdi 2850 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯)))) |
111 | 104, 110 | sselid 3941 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0})) |
112 | | supxrub 13172 |
. . . . . . . . . . . . 13
β’ (((ran
(π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}) β β*
β§ ((ββπ₯)πΈ(πβπ₯)) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0})) β ((ββπ₯)πΈ(πβπ₯)) β€ sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
113 | 103, 111,
112 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β€ sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
114 | | simp21 1207 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β π β π΅) |
115 | 4, 1, 87, 88, 89, 90, 114, 5, 6, 7 | prdsdsval3 17302 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ·π) = sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
116 | 115 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (βπ·π) = sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
117 | 113, 116 | breqtrrd 5132 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β€ (βπ·π)) |
118 | | xrrege0 13022 |
. . . . . . . . . . 11
β’
(((((ββπ₯)πΈ(πβπ₯)) β β* β§ (βπ·π) β β) β§ (0 β€ ((ββπ₯)πΈ(πβπ₯)) β§ ((ββπ₯)πΈ(πβπ₯)) β€ (βπ·π))) β ((ββπ₯)πΈ(πβπ₯)) β β) |
119 | 94, 96, 98, 117, 118 | syl22anc 838 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β β) |
120 | | xmetcl 23606 |
. . . . . . . . . . . 12
β’ ((πΈ β (βMetβπ) β§ (ββπ₯) β π β§ (πβπ₯) β π) β ((ββπ₯)πΈ(πβπ₯)) β
β*) |
121 | 79, 92, 85, 120 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β
β*) |
122 | | simp3r 1203 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ·π) β β) |
123 | 122 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (βπ·π) β β) |
124 | | xmetge0 23619 |
. . . . . . . . . . . 12
β’ ((πΈ β (βMetβπ) β§ (ββπ₯) β π β§ (πβπ₯) β π) β 0 β€ ((ββπ₯)πΈ(πβπ₯))) |
125 | 79, 92, 85, 124 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β 0 β€ ((ββπ₯)πΈ(πβπ₯))) |
126 | 121 | fmpttd 7058 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))):πΌβΆβ*) |
127 | 126 | frnd 6672 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) β
β*) |
128 | 127, 102 | unssd 4145 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
129 | | ssun1 4131 |
. . . . . . . . . . . . . 14
β’ ran
(π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}) |
130 | | ovex 7383 |
. . . . . . . . . . . . . . . . 17
β’ ((ββπ₯)πΈ(πβπ₯)) β V |
131 | 130 | elabrex 7185 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β πΌ β ((ββπ₯)πΈ(πβπ₯)) β {π§ β£ βπ₯ β πΌ π§ = ((ββπ₯)πΈ(πβπ₯))}) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β {π§ β£ βπ₯ β πΌ π§ = ((ββπ₯)πΈ(πβπ₯))}) |
133 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) = (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) |
134 | 133 | rnmpt 5907 |
. . . . . . . . . . . . . . 15
β’ ran
(π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) = {π§ β£ βπ₯ β πΌ π§ = ((ββπ₯)πΈ(πβπ₯))} |
135 | 132, 134 | eleqtrrdi 2850 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯)))) |
136 | 129, 135 | sselid 3941 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0})) |
137 | | supxrub 13172 |
. . . . . . . . . . . . 13
β’ (((ran
(π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}) β β*
β§ ((ββπ₯)πΈ(πβπ₯)) β (ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0})) β ((ββπ₯)πΈ(πβπ₯)) β€ sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
138 | 128, 136,
137 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β€ sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
139 | | simp22 1208 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β π β π΅) |
140 | 4, 1, 87, 88, 89, 90, 139, 5, 6, 7 | prdsdsval3 17302 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ·π) = sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
141 | 140 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (βπ·π) = sup((ran (π₯ β πΌ β¦ ((ββπ₯)πΈ(πβπ₯))) βͺ {0}), β*, <
)) |
142 | 138, 141 | breqtrrd 5132 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β€ (βπ·π)) |
143 | | xrrege0 13022 |
. . . . . . . . . . 11
β’
(((((ββπ₯)πΈ(πβπ₯)) β β* β§ (βπ·π) β β) β§ (0 β€ ((ββπ₯)πΈ(πβπ₯)) β§ ((ββπ₯)πΈ(πβπ₯)) β€ (βπ·π))) β ((ββπ₯)πΈ(πβπ₯)) β β) |
144 | 121, 123,
125, 142, 143 | syl22anc 838 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((ββπ₯)πΈ(πβπ₯)) β β) |
145 | 119, 144 | readdcld 11118 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (((ββπ₯)πΈ(πβπ₯)) + ((ββπ₯)πΈ(πβπ₯))) β β) |
146 | 79, 82, 85, 57 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β 0 β€ ((πβπ₯)πΈ(πβπ₯))) |
147 | | xmettri2 23615 |
. . . . . . . . . . 11
β’ ((πΈ β (βMetβπ) β§ ((ββπ₯) β π β§ (πβπ₯) β π β§ (πβπ₯) β π)) β ((πβπ₯)πΈ(πβπ₯)) β€ (((ββπ₯)πΈ(πβπ₯)) +π ((ββπ₯)πΈ(πβπ₯)))) |
148 | 79, 92, 82, 85, 147 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β€ (((ββπ₯)πΈ(πβπ₯)) +π ((ββπ₯)πΈ(πβπ₯)))) |
149 | 119, 144 | rexaddd 13082 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (((ββπ₯)πΈ(πβπ₯)) +π ((ββπ₯)πΈ(πβπ₯))) = (((ββπ₯)πΈ(πβπ₯)) + ((ββπ₯)πΈ(πβπ₯)))) |
150 | 148, 149 | breqtrd 5130 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β€ (((ββπ₯)πΈ(πβπ₯)) + ((ββπ₯)πΈ(πβπ₯)))) |
151 | | xrrege0 13022 |
. . . . . . . . 9
β’
(((((πβπ₯)πΈ(πβπ₯)) β β* β§ (((ββπ₯)πΈ(πβπ₯)) + ((ββπ₯)πΈ(πβπ₯))) β β) β§ (0 β€ ((πβπ₯)πΈ(πβπ₯)) β§ ((πβπ₯)πΈ(πβπ₯)) β€ (((ββπ₯)πΈ(πβπ₯)) + ((ββπ₯)πΈ(πβπ₯))))) β ((πβπ₯)πΈ(πβπ₯)) β β) |
152 | 86, 145, 146, 150, 151 | syl22anc 838 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β β) |
153 | | readdcl 11068 |
. . . . . . . . . 10
β’ (((βπ·π) β β β§ (βπ·π) β β) β ((βπ·π) + (βπ·π)) β β) |
154 | 153 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β ((βπ·π) + (βπ·π)) β β) |
155 | 154 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((βπ·π) + (βπ·π)) β β) |
156 | 119, 144,
96, 123, 117, 142 | le2addd 11708 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β (((ββπ₯)πΈ(πβπ₯)) + ((ββπ₯)πΈ(πβπ₯))) β€ ((βπ·π) + (βπ·π))) |
157 | 152, 145,
155, 150, 156 | letrd 11246 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β§ π₯ β πΌ) β ((πβπ₯)πΈ(πβπ₯)) β€ ((βπ·π) + (βπ·π))) |
158 | 157 | ralrimiva 3142 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ ((βπ·π) + (βπ·π))) |
159 | 86 | ralrimiva 3142 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β
β*) |
160 | | breq1 5107 |
. . . . . . . 8
β’ (π§ = ((πβπ₯)πΈ(πβπ₯)) β (π§ β€ ((βπ·π) + (βπ·π)) β ((πβπ₯)πΈ(πβπ₯)) β€ ((βπ·π) + (βπ·π)))) |
161 | 52, 160 | ralrnmptw 7039 |
. . . . . . 7
β’
(βπ₯ β
πΌ ((πβπ₯)πΈ(πβπ₯)) β β* β
(βπ§ β ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ ((βπ·π) + (βπ·π)) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ ((βπ·π) + (βπ·π)))) |
162 | 159, 161 | syl 17 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ ((βπ·π) + (βπ·π)) β βπ₯ β πΌ ((πβπ₯)πΈ(πβπ₯)) β€ ((βπ·π) + (βπ·π)))) |
163 | 158, 162 | mpbird 257 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ ((βπ·π) + (βπ·π))) |
164 | 12 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β π·:(π΅ Γ π΅)βΆ(0[,]+β)) |
165 | 164, 90, 114 | fovcdmd 7519 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ·π) β (0[,]+β)) |
166 | | elxrge0 13303 |
. . . . . . . . 9
β’ ((βπ·π) β (0[,]+β) β ((βπ·π) β β* β§ 0 β€
(βπ·π))) |
167 | 166 | simprbi 498 |
. . . . . . . 8
β’ ((βπ·π) β (0[,]+β) β 0 β€ (βπ·π)) |
168 | 165, 167 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β 0 β€ (βπ·π)) |
169 | 164, 90, 139 | fovcdmd 7519 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (βπ·π) β (0[,]+β)) |
170 | | elxrge0 13303 |
. . . . . . . . 9
β’ ((βπ·π) β (0[,]+β) β ((βπ·π) β β* β§ 0 β€
(βπ·π))) |
171 | 170 | simprbi 498 |
. . . . . . . 8
β’ ((βπ·π) β (0[,]+β) β 0 β€ (βπ·π)) |
172 | 169, 171 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β 0 β€ (βπ·π)) |
173 | 95, 122, 168, 172 | addge0d 11665 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β 0 β€ ((βπ·π) + (βπ·π))) |
174 | | breq1 5107 |
. . . . . . 7
β’ (π§ = 0 β (π§ β€ ((βπ·π) + (βπ·π)) β 0 β€ ((βπ·π) + (βπ·π)))) |
175 | 44, 174 | ralsn 4641 |
. . . . . 6
β’
(βπ§ β
{0}π§ β€ ((βπ·π) + (βπ·π)) β 0 β€ ((βπ·π) + (βπ·π))) |
176 | 173, 175 | sylibr 233 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ§ β {0}π§ β€ ((βπ·π) + (βπ·π))) |
177 | | ralunb 4150 |
. . . . 5
β’
(βπ§ β
(ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ ((βπ·π) + (βπ·π)) β (βπ§ β ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯)))π§ β€ ((βπ·π) + (βπ·π)) β§ βπ§ β {0}π§ β€ ((βπ·π) + (βπ·π)))) |
178 | 163, 176,
177 | sylanbrc 584 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ ((βπ·π) + (βπ·π))) |
179 | 40 | 3adantr3 1172 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
180 | 179 | 3adant3 1133 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β
β*) |
181 | 154 | rexrd 11139 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β ((βπ·π) + (βπ·π)) β
β*) |
182 | | supxrleub 13174 |
. . . . 5
β’ (((ran
(π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}) β β*
β§ ((βπ·π) + (βπ·π)) β β*) β
(sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β€ ((βπ·π) + (βπ·π)) β βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ ((βπ·π) + (βπ·π)))) |
183 | 180, 181,
182 | syl2anc 585 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β€ ((βπ·π) + (βπ·π)) β βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0})π§ β€ ((βπ·π) + (βπ·π)))) |
184 | 178, 183 | mpbird 257 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β sup((ran (π₯ β πΌ β¦ ((πβπ₯)πΈ(πβπ₯))) βͺ {0}), β*, < )
β€ ((βπ·π) + (βπ·π))) |
185 | 78, 184 | eqbrtrd 5126 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅ β§ β β π΅) β§ ((βπ·π) β β β§ (βπ·π) β β)) β (ππ·π) β€ ((βπ·π) + (βπ·π))) |
186 | 3, 15, 19, 76, 185 | isxmet2d 23602 |
1
β’ (π β π· β (βMetβπ΅)) |