Step | Hyp | Ref
| Expression |
1 | | comet.1 |
. . 3
β’ (π β π· β (βMetβπ)) |
2 | 1 | elfvexd 6877 |
. 2
β’ (π β π β V) |
3 | | comet.2 |
. . 3
β’ (π β πΉ:(0[,]+β)βΆβ*) |
4 | | xmetf 23604 |
. . . . . 6
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β π·:(π Γ π)βΆβ*) |
6 | 5 | ffnd 6665 |
. . . 4
β’ (π β π· Fn (π Γ π)) |
7 | | xmetcl 23606 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β (ππ·π) β
β*) |
8 | | xmetge0 23619 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β 0 β€ (ππ·π)) |
9 | | elxrge0 13303 |
. . . . . . . 8
β’ ((ππ·π) β (0[,]+β) β ((ππ·π) β β* β§ 0 β€
(ππ·π))) |
10 | 7, 8, 9 | sylanbrc 584 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β (ππ·π) β (0[,]+β)) |
11 | 10 | 3expb 1121 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
12 | 1, 11 | sylan 581 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
13 | 12 | ralrimivva 3196 |
. . . 4
β’ (π β βπ β π βπ β π (ππ·π) β (0[,]+β)) |
14 | | ffnov 7476 |
. . . 4
β’ (π·:(π Γ π)βΆ(0[,]+β) β (π· Fn (π Γ π) β§ βπ β π βπ β π (ππ·π) β (0[,]+β))) |
15 | 6, 13, 14 | sylanbrc 584 |
. . 3
β’ (π β π·:(π Γ π)βΆ(0[,]+β)) |
16 | 3, 15 | fcod 6690 |
. 2
β’ (π β (πΉ β π·):(π Γ π)βΆβ*) |
17 | | opelxpi 5668 |
. . . . . 6
β’ ((π β π β§ π β π) β β¨π, πβ© β (π Γ π)) |
18 | | fvco3 6936 |
. . . . . 6
β’ ((π·:(π Γ π)βΆβ* β§
β¨π, πβ© β (π Γ π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
19 | 5, 17, 18 | syl2an 597 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
20 | | df-ov 7353 |
. . . . 5
β’ (π(πΉ β π·)π) = ((πΉ β π·)ββ¨π, πβ©) |
21 | | df-ov 7353 |
. . . . . 6
β’ (ππ·π) = (π·ββ¨π, πβ©) |
22 | 21 | fveq2i 6841 |
. . . . 5
β’ (πΉβ(ππ·π)) = (πΉβ(π·ββ¨π, πβ©)) |
23 | 19, 20, 22 | 3eqtr4g 2803 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
24 | 23 | eqeq1d 2740 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((π(πΉ β π·)π) = 0 β (πΉβ(ππ·π)) = 0)) |
25 | | fveq2 6838 |
. . . . . 6
β’ (π₯ = (ππ·π) β (πΉβπ₯) = (πΉβ(ππ·π))) |
26 | 25 | eqeq1d 2740 |
. . . . 5
β’ (π₯ = (ππ·π) β ((πΉβπ₯) = 0 β (πΉβ(ππ·π)) = 0)) |
27 | | eqeq1 2742 |
. . . . 5
β’ (π₯ = (ππ·π) β (π₯ = 0 β (ππ·π) = 0)) |
28 | 26, 27 | bibi12d 346 |
. . . 4
β’ (π₯ = (ππ·π) β (((πΉβπ₯) = 0 β π₯ = 0) β ((πΉβ(ππ·π)) = 0 β (ππ·π) = 0))) |
29 | | comet.3 |
. . . . . 6
β’ ((π β§ π₯ β (0[,]+β)) β ((πΉβπ₯) = 0 β π₯ = 0)) |
30 | 29 | ralrimiva 3142 |
. . . . 5
β’ (π β βπ₯ β (0[,]+β)((πΉβπ₯) = 0 β π₯ = 0)) |
31 | 30 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β βπ₯ β (0[,]+β)((πΉβπ₯) = 0 β π₯ = 0)) |
32 | 28, 31, 12 | rspcdva 3581 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ(ππ·π)) = 0 β (ππ·π) = 0)) |
33 | | xmeteq0 23613 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β ((ππ·π) = 0 β π = π)) |
34 | 33 | 3expb 1121 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π)) β ((ππ·π) = 0 β π = π)) |
35 | 1, 34 | sylan 581 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((ππ·π) = 0 β π = π)) |
36 | 24, 32, 35 | 3bitrd 305 |
. 2
β’ ((π β§ (π β π β§ π β π)) β ((π(πΉ β π·)π) = 0 β π = π)) |
37 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β πΉ:(0[,]+β)βΆβ*) |
38 | 12 | 3adantr3 1172 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
39 | 37, 38 | ffvelcdmd 7031 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β
β*) |
40 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π·:(π Γ π)βΆ(0[,]+β)) |
41 | | simpr3 1197 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
42 | | simpr1 1195 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
43 | 40, 41, 42 | fovcdmd 7519 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
44 | | simpr2 1196 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π β π) |
45 | 40, 41, 44 | fovcdmd 7519 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β (0[,]+β)) |
46 | | ge0xaddcl 13308 |
. . . . . 6
β’ (((ππ·π) β (0[,]+β) β§ (ππ·π) β (0[,]+β)) β ((ππ·π) +π (ππ·π)) β (0[,]+β)) |
47 | 43, 45, 46 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((ππ·π) +π (ππ·π)) β (0[,]+β)) |
48 | 37, 47 | ffvelcdmd 7031 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ((ππ·π) +π (ππ·π))) β
β*) |
49 | 37, 43 | ffvelcdmd 7031 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β
β*) |
50 | 37, 45 | ffvelcdmd 7031 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β
β*) |
51 | 49, 50 | xaddcld 13149 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉβ(ππ·π)) +π (πΉβ(ππ·π))) β
β*) |
52 | | 3anrot 1101 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β (π β π β§ π β π β§ π β π)) |
53 | | xmettri2 23615 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
54 | 52, 53 | sylan2br 596 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
55 | 1, 54 | sylan 581 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
56 | | comet.4 |
. . . . . . . 8
β’ ((π β§ (π₯ β (0[,]+β) β§ π¦ β (0[,]+β))) β
(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
57 | 56 | ralrimivva 3196 |
. . . . . . 7
β’ (π β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
58 | 57 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
59 | | breq1 5107 |
. . . . . . . 8
β’ (π₯ = (ππ·π) β (π₯ β€ π¦ β (ππ·π) β€ π¦)) |
60 | 25 | breq1d 5114 |
. . . . . . . 8
β’ (π₯ = (ππ·π) β ((πΉβπ₯) β€ (πΉβπ¦) β (πΉβ(ππ·π)) β€ (πΉβπ¦))) |
61 | 59, 60 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = (ππ·π) β ((π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)) β ((ππ·π) β€ π¦ β (πΉβ(ππ·π)) β€ (πΉβπ¦)))) |
62 | | breq2 5108 |
. . . . . . . 8
β’ (π¦ = ((ππ·π) +π (ππ·π)) β ((ππ·π) β€ π¦ β (ππ·π) β€ ((ππ·π) +π (ππ·π)))) |
63 | | fveq2 6838 |
. . . . . . . . 9
β’ (π¦ = ((ππ·π) +π (ππ·π)) β (πΉβπ¦) = (πΉβ((ππ·π) +π (ππ·π)))) |
64 | 63 | breq2d 5116 |
. . . . . . . 8
β’ (π¦ = ((ππ·π) +π (ππ·π)) β ((πΉβ(ππ·π)) β€ (πΉβπ¦) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π))))) |
65 | 62, 64 | imbi12d 345 |
. . . . . . 7
β’ (π¦ = ((ππ·π) +π (ππ·π)) β (((ππ·π) β€ π¦ β (πΉβ(ππ·π)) β€ (πΉβπ¦)) β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π)))))) |
66 | 61, 65 | rspc2va 3590 |
. . . . . 6
β’ ((((ππ·π) β (0[,]+β) β§ ((ππ·π) +π (ππ·π)) β (0[,]+β)) β§ βπ₯ β
(0[,]+β)βπ¦
β (0[,]+β)(π₯
β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π))))) |
67 | 38, 47, 58, 66 | syl21anc 837 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((ππ·π) β€ ((ππ·π) +π (ππ·π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π))))) |
68 | 55, 67 | mpd 15 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β€ (πΉβ((ππ·π) +π (ππ·π)))) |
69 | | comet.5 |
. . . . . . 7
β’ ((π β§ (π₯ β (0[,]+β) β§ π¦ β (0[,]+β))) β
(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) |
70 | 69 | ralrimivva 3196 |
. . . . . 6
β’ (π β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) |
71 | 70 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β βπ₯ β (0[,]+β)βπ¦ β (0[,]+β)(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) |
72 | | fvoveq1 7373 |
. . . . . . 7
β’ (π₯ = (ππ·π) β (πΉβ(π₯ +π π¦)) = (πΉβ((ππ·π) +π π¦))) |
73 | | fveq2 6838 |
. . . . . . . 8
β’ (π₯ = (ππ·π) β (πΉβπ₯) = (πΉβ(ππ·π))) |
74 | 73 | oveq1d 7365 |
. . . . . . 7
β’ (π₯ = (ππ·π) β ((πΉβπ₯) +π (πΉβπ¦)) = ((πΉβ(ππ·π)) +π (πΉβπ¦))) |
75 | 72, 74 | breq12d 5117 |
. . . . . 6
β’ (π₯ = (ππ·π) β ((πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦)) β (πΉβ((ππ·π) +π π¦)) β€ ((πΉβ(ππ·π)) +π (πΉβπ¦)))) |
76 | | oveq2 7358 |
. . . . . . . 8
β’ (π¦ = (ππ·π) β ((ππ·π) +π π¦) = ((ππ·π) +π (ππ·π))) |
77 | 76 | fveq2d 6842 |
. . . . . . 7
β’ (π¦ = (ππ·π) β (πΉβ((ππ·π) +π π¦)) = (πΉβ((ππ·π) +π (ππ·π)))) |
78 | | fveq2 6838 |
. . . . . . . 8
β’ (π¦ = (ππ·π) β (πΉβπ¦) = (πΉβ(ππ·π))) |
79 | 78 | oveq2d 7366 |
. . . . . . 7
β’ (π¦ = (ππ·π) β ((πΉβ(ππ·π)) +π (πΉβπ¦)) = ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
80 | 77, 79 | breq12d 5117 |
. . . . . 6
β’ (π¦ = (ππ·π) β ((πΉβ((ππ·π) +π π¦)) β€ ((πΉβ(ππ·π)) +π (πΉβπ¦)) β (πΉβ((ππ·π) +π (ππ·π))) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π))))) |
81 | 75, 80 | rspc2va 3590 |
. . . . 5
β’ ((((ππ·π) β (0[,]+β) β§ (ππ·π) β (0[,]+β)) β§ βπ₯ β
(0[,]+β)βπ¦
β (0[,]+β)(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) β (πΉβ((ππ·π) +π (ππ·π))) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
82 | 43, 45, 71, 81 | syl21anc 837 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ((ππ·π) +π (ππ·π))) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
83 | 39, 48, 51, 68, 82 | xrletrd 13010 |
. . 3
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (πΉβ(ππ·π)) β€ ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
84 | 23 | 3adantr3 1172 |
. . 3
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
85 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β π·:(π Γ π)βΆβ*) |
86 | 41, 42 | opelxpd 5669 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β β¨π, πβ© β (π Γ π)) |
87 | 85, 86 | fvco3d 6937 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
88 | | df-ov 7353 |
. . . . 5
β’ (π(πΉ β π·)π) = ((πΉ β π·)ββ¨π, πβ©) |
89 | | df-ov 7353 |
. . . . . 6
β’ (ππ·π) = (π·ββ¨π, πβ©) |
90 | 89 | fveq2i 6841 |
. . . . 5
β’ (πΉβ(ππ·π)) = (πΉβ(π·ββ¨π, πβ©)) |
91 | 87, 88, 90 | 3eqtr4g 2803 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
92 | 41, 44 | opelxpd 5669 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π β§ π β π)) β β¨π, πβ© β (π Γ π)) |
93 | 85, 92 | fvco3d 6937 |
. . . . 5
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉ β π·)ββ¨π, πβ©) = (πΉβ(π·ββ¨π, πβ©))) |
94 | | df-ov 7353 |
. . . . 5
β’ (π(πΉ β π·)π) = ((πΉ β π·)ββ¨π, πβ©) |
95 | | df-ov 7353 |
. . . . . 6
β’ (ππ·π) = (π·ββ¨π, πβ©) |
96 | 95 | fveq2i 6841 |
. . . . 5
β’ (πΉβ(ππ·π)) = (πΉβ(π·ββ¨π, πβ©)) |
97 | 93, 94, 96 | 3eqtr4g 2803 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) = (πΉβ(ππ·π))) |
98 | 91, 97 | oveq12d 7368 |
. . 3
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((π(πΉ β π·)π) +π (π(πΉ β π·)π)) = ((πΉβ(ππ·π)) +π (πΉβ(ππ·π)))) |
99 | 83, 84, 98 | 3brtr4d 5136 |
. 2
β’ ((π β§ (π β π β§ π β π β§ π β π)) β (π(πΉ β π·)π) β€ ((π(πΉ β π·)π) +π (π(πΉ β π·)π))) |
100 | 2, 16, 36, 99 | isxmetd 23601 |
1
β’ (π β (πΉ β π·) β (βMetβπ)) |