Step | Hyp | Ref
| Expression |
1 | | xmetrel 13813 |
. . . 4
β’ Rel
βMet |
2 | | comet.1 |
. . . 4
β’ (π β π· β (βMetβπ)) |
3 | | relelfvdm 5547 |
. . . 4
β’ ((Rel
βMet β§ π· β
(βMetβπ))
β π β dom
βMet) |
4 | 1, 2, 3 | sylancr 414 |
. . 3
β’ (π β π β dom βMet) |
5 | 4 | elexd 2750 |
. 2
β’ (π β π β V) |
6 | | comet.2 |
. . 3
β’ (π β πΉ:(0[,]+β)βΆβ*) |
7 | | xmetf 13820 |
. . . . . 6
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
8 | 2, 7 | syl 14 |
. . . . 5
β’ (π β π·:(π Γ π)βΆβ*) |
9 | 8 | ffnd 5366 |
. . . 4
β’ (π β π· Fn (π Γ π)) |
10 | | xmetcl 13822 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β (ππ·π) β
β*) |
11 | | xmetge0 13835 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β 0 β€ (ππ·π)) |
12 | | elxrge0 9977 |
. . . . . . . 8
β’ ((ππ·π) β (0[,]+β) β ((ππ·π) β β* β§ 0 β€
(ππ·π))) |
13 | 10, 11, 12 | sylanbrc 417 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β (ππ·π) β (0[,]+β)) |
14 | 13 | 3expb 1204 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
15 | 2, 14 | sylan 283 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
16 | 15 | ralrimivva 2559 |
. . . 4
β’ (π β βπ β π βπ β π (ππ·π) β (0[,]+β)) |
17 | | ffnov 5978 |
. . . 4
β’ (π·:(π Γ π)βΆ(0[,]+β) β (π· Fn (π Γ π) β§ βπ β π βπ β π (ππ·π) β (0[,]+β))) |
18 | 9, 16, 17 | sylanbrc 417 |
. . 3
β’ (π β π·:(π Γ π)βΆ(0[,]+β)) |
19 | | fco 5381 |
. . 3
β’ ((πΉ:(0[,]+β)βΆβ*
β§ π·:(π Γ π)βΆ(0[,]+β)) β (πΉ β π·):(π Γ π)βΆβ*) |
20 | 6, 18, 19 | syl2anc 411 |
. 2
β’ (π β (πΉ β π·):(π Γ π)βΆβ*) |
21 | | opelxpi 4658 |
. . . . . 6
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
22 | | fvco3 5587 |
. . . . . 6
β’ ((π·:(π Γ π)βΆβ* β§
β¨π, πβ© β (π Γ π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
23 | 8, 21, 22 | syl2an 289 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
24 | | df-ov 5877 |
. . . . 5
β’ (π(πΉ β π·)π) = ((πΉ β π·)ββ¨π, πβ©) |
25 | | df-ov 5877 |
. . . . . 6
β’ (ππ·π) = (π·ββ¨π, πβ©) |
26 | 25 | fveq2i 5518 |
. . . . 5
β’ (πΉβ(ππ·π)) = (πΉβ(π·ββ¨π, πβ©)) |
27 | 23, 24, 26 | 3eqtr4g 2235 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
28 | 27 | eqeq1d 2186 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((π(πΉ β π·)π) = 0 β (πΉβ(ππ·π)) = 0)) |
29 | | fveq2 5515 |
. . . . . 6
β’ (π₯ = (ππ·π) β (πΉβπ₯) = (πΉβ(ππ·π))) |
30 | 29 | eqeq1d 2186 |
. . . . 5
β’ (π₯ = (ππ·π) β ((πΉβπ₯) = 0 β (πΉβ(ππ·π)) = 0)) |
31 | | eqeq1 2184 |
. . . . 5
β’ (π₯ = (ππ·π) β (π₯ = 0 β (ππ·π) = 0)) |
32 | 30, 31 | bibi12d 235 |
. . . 4
β’ (π₯ = (ππ·π) β (((πΉβπ₯) = 0 β π₯ = 0) β ((πΉβ(ππ·π)) = 0 β (ππ·π) = 0))) |
33 | | comet.3 |
. . . . . 6
β’ ((π β§ π₯ β (0[,]+β)) β ((πΉβπ₯) = 0 β π₯ = 0)) |
34 | 33 | ralrimiva 2550 |
. . . . 5
β’ (π β βπ₯ β (0[,]+β)((πΉβπ₯) = 0 β π₯ = 0)) |
35 | 34 | adantr 276 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β βπ₯ β (0[,]+β)((πΉβπ₯) = 0 β π₯ = 0)) |
36 | 32, 35, 15 | rspcdva 2846 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ(ππ·π)) = 0 β (ππ·π) = 0)) |
37 | | xmeteq0 13829 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β ((ππ·π) = 0 β π = π)) |
38 | 37 | 3expb 1204 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π)) β ((ππ·π) = 0 β π = π)) |
39 | 2, 38 | sylan 283 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((ππ·π) = 0 β π = π)) |
40 | 28, 36, 39 | 3bitrd 214 |
. 2
β’ ((π β§ (π β π β§ π β π)) β ((π(πΉ β π·)π) = 0 β π = π)) |
41 | 6 | adantr 276 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β πΉ:(0[,]+β)βΆβ*) |
42 | 15 | 3adantr3 1158 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
43 | 41, 42 | ffvelcdmd 5652 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β
β*) |
44 | 18 | adantr 276 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π·:(π Γ π)βΆ(0[,]+β)) |
45 | | simpr3 1005 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
46 | | simpr1 1003 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
47 | 44, 45, 46 | fovcdmd 6018 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
48 | | simpr2 1004 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
49 | 44, 45, 48 | fovcdmd 6018 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
50 | | ge0xaddcl 9982 |
. . . . . 6
β’ (((ππ·π) β (0[,]+β) β§ (ππ·π) β (0[,]+β)) β ((ππ·π) +π (ππ·π)) β (0[,]+β)) |
51 | 47, 49, 50 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((ππ·π) +π (ππ·π)) β (0[,]+β)) |
52 | 41, 51 | ffvelcdmd 5652 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ((ππ·π) +π (ππ·π))) β
β*) |
53 | 41, 47 | ffvelcdmd 5652 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β
β*) |
54 | 41, 49 | ffvelcdmd 5652 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β
β*) |
55 | 53, 54 | xaddcld 9883 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉβ(ππ·π)) +π (πΉβ(ππ·π))) β
β*) |
56 | | 3anrot 983 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β (π β π β§ π β π β§ π β π)) |
57 | | xmettri2 13831 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
58 | 56, 57 | sylan2br 288 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
59 | 2, 58 | sylan 283 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
60 | | comet.4 |
. . . . . . . 8
β’ ((π β§ (π₯ β (0[,]+β) β§ π¦ β (0[,]+β))) β
(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
61 | 60 | ralrimivva 2559 |
. . . . . . 7
β’ (π β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
62 | 61 | adantr 276 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
63 | | breq1 4006 |
. . . . . . . 8
β’ (π₯ = (ππ·π) β (π₯ β€ π¦ β (ππ·π) β€ π¦)) |
64 | 29 | breq1d 4013 |
. . . . . . . 8
β’ (π₯ = (ππ·π) β ((πΉβπ₯) β€ (πΉβπ¦) β (πΉβ(ππ·π)) β€ (πΉβπ¦))) |
65 | 63, 64 | imbi12d 234 |
. . . . . . 7
β’ (π₯ = (ππ·π) β ((π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)) β ((ππ·π) β€ π¦ β (πΉβ(ππ·π)) β€ (πΉβπ¦)))) |
66 | | breq2 4007 |
. . . . . . . 8
β’ (π¦ = ((ππ·π) +π (ππ·π)) β ((ππ·π) β€ π¦ β (ππ·π) β€ ((ππ·π) +π (ππ·π)))) |
67 | | fveq2 5515 |
. . . . . . . . 9
β’ (π¦ = ((ππ·π) +π (ππ·π)) β (πΉβπ¦) = (πΉβ((ππ·π) +π (ππ·π)))) |
68 | 67 | breq2d 4015 |
. . . . . . . 8
β’ (π¦ = ((ππ·π) +π (ππ·π)) β ((πΉβ(ππ·π)) β€ (πΉβπ¦) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π))))) |
69 | 66, 68 | imbi12d 234 |
. . . . . . 7
β’ (π¦ = ((ππ·π) +π (ππ·π)) β (((ππ·π) β€ π¦ β (πΉβ(ππ·π)) β€ (πΉβπ¦)) β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π)))))) |
70 | 65, 69 | rspc2va 2855 |
. . . . . 6
β’ ((((ππ·π) β (0[,]+β) β§ ((ππ·π) +π (ππ·π)) β (0[,]+β)) β§ βπ₯ β
(0[,]+β)βπ¦
β (0[,]+β)(π₯
β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π))))) |
71 | 42, 51, 62, 70 | syl21anc 1237 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π))))) |
72 | 59, 71 | mpd 13 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π)))) |
73 | | comet.5 |
. . . . . . 7
β’ ((π β§ (π₯ β (0[,]+β) β§ π¦ β (0[,]+β))) β
(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) |
74 | 73 | ralrimivva 2559 |
. . . . . 6
β’ (π β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) |
75 | 74 | adantr 276 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) |
76 | | fvoveq1 5897 |
. . . . . . 7
β’ (π₯ = (ππ·π) β (πΉβ(π₯ +π π¦)) = (πΉβ((ππ·π) +π π¦))) |
77 | | fveq2 5515 |
. . . . . . . 8
β’ (π₯ = (ππ·π) β (πΉβπ₯) = (πΉβ(ππ·π))) |
78 | 77 | oveq1d 5889 |
. . . . . . 7
β’ (π₯ = (ππ·π) β ((πΉβπ₯) +π (πΉβπ¦)) = ((πΉβ(ππ·π)) +π (πΉβπ¦))) |
79 | 76, 78 | breq12d 4016 |
. . . . . 6
β’ (π₯ = (ππ·π) β ((πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦)) β (πΉβ((ππ·π) +π π¦)) β€ ((πΉβ(ππ·π)) +π (πΉβπ¦)))) |
80 | | oveq2 5882 |
. . . . . . . 8
β’ (π¦ = (ππ·π) β ((ππ·π) +π π¦) = ((ππ·π) +π (ππ·π))) |
81 | 80 | fveq2d 5519 |
. . . . . . 7
β’ (π¦ = (ππ·π) β (πΉβ((ππ·π) +π π¦)) = (πΉβ((ππ·π) +π (ππ·π)))) |
82 | | fveq2 5515 |
. . . . . . . 8
β’ (π¦ = (ππ·π) β (πΉβπ¦) = (πΉβ(ππ·π))) |
83 | 82 | oveq2d 5890 |
. . . . . . 7
β’ (π¦ = (ππ·π) β ((πΉβ(ππ·π)) +π (πΉβπ¦)) = ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
84 | 81, 83 | breq12d 4016 |
. . . . . 6
β’ (π¦ = (ππ·π) β ((πΉβ((ππ·π) +π π¦)) β€ ((πΉβ(ππ·π)) +π (πΉβπ¦)) β (πΉβ((ππ·π) +π (ππ·π))) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π))))) |
85 | 79, 84 | rspc2va 2855 |
. . . . 5
β’ ((((ππ·π) β (0[,]+β) β§ (ππ·π) β (0[,]+β)) β§ βπ₯ β
(0[,]+β)βπ¦
β (0[,]+β)(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) β (πΉβ((ππ·π) +π (ππ·π))) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
86 | 47, 49, 75, 85 | syl21anc 1237 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ((ππ·π) +π (ππ·π))) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
87 | 43, 52, 55, 72, 86 | xrletrd 9811 |
. . 3
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
88 | 27 | 3adantr3 1158 |
. . 3
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
89 | 8 | adantr 276 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π·:(π Γ π)βΆβ*) |
90 | 45, 46 | opelxpd 4659 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β β¨π, πβ© β (π Γ π)) |
91 | | fvco3 5587 |
. . . . . 6
β’ ((π·:(π Γ π)βΆβ* β§
β¨π, πβ© β (π Γ π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
92 | 89, 90, 91 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
93 | | df-ov 5877 |
. . . . 5
β’ (π(πΉ β π·)π) = ((πΉ β π·)ββ¨π, πβ©) |
94 | | df-ov 5877 |
. . . . . 6
β’ (ππ·π) = (π·ββ¨π, πβ©) |
95 | 94 | fveq2i 5518 |
. . . . 5
β’ (πΉβ(ππ·π)) = (πΉβ(π·ββ¨π, πβ©)) |
96 | 92, 93, 95 | 3eqtr4g 2235 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
97 | 45, 48 | opelxpd 4659 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β β¨π, πβ© β (π Γ π)) |
98 | | fvco3 5587 |
. . . . . 6
β’ ((π·:(π Γ π)βΆβ* β§
β¨π, πβ© β (π Γ π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
99 | 89, 97, 98 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
100 | | df-ov 5877 |
. . . . 5
β’ (π(πΉ β π·)π) = ((πΉ β π·)ββ¨π, πβ©) |
101 | | df-ov 5877 |
. . . . . 6
β’ (ππ·π) = (π·ββ¨π, πβ©) |
102 | 101 | fveq2i 5518 |
. . . . 5
β’ (πΉβ(ππ·π)) = (πΉβ(π·ββ¨π, πβ©)) |
103 | 99, 100, 102 | 3eqtr4g 2235 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
104 | 96, 103 | oveq12d 5892 |
. . 3
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((π(πΉ β π·)π) +π (π(πΉ β π·)π)) = ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
105 | 87, 88, 104 | 3brtr4d 4035 |
. 2
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) β€ ((π(πΉ β π·)π) +π (π(πΉ β π·)π))) |
106 | 5, 20, 40, 105 | isxmetd 13817 |
1
β’ (π β (πΉ β π·) β (βMetβπ)) |