Step | Hyp | Ref
| Expression |
1 | | relres 5970 |
. . 3
β’ Rel ( I
βΎ π) |
2 | 1 | a1i 11 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β Rel ( I βΎ π)) |
3 | | vex 3451 |
. . . . . . . . . . . . . . 15
β’ π β V |
4 | 3 | brresi 5950 |
. . . . . . . . . . . . . 14
β’ (π( I βΎ π)π β (π β π β§ π I π)) |
5 | | df-br 5110 |
. . . . . . . . . . . . . 14
β’ (π( I βΎ π)π β β¨π, πβ© β ( I βΎ π)) |
6 | 3 | ideq 5812 |
. . . . . . . . . . . . . . 15
β’ (π I π β π = π) |
7 | 6 | anbi2i 624 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π I π) β (π β π β§ π = π)) |
8 | 4, 5, 7 | 3bitr3i 301 |
. . . . . . . . . . . . 13
β’
(β¨π, πβ© β ( I βΎ π) β (π β π β§ π = π)) |
9 | 8 | biimpi 215 |
. . . . . . . . . . . 12
β’
(β¨π, πβ© β ( I βΎ π) β (π β π β§ π = π)) |
10 | 9 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β (π β π β§ π = π)) |
11 | 10 | simprd 497 |
. . . . . . . . . 10
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β π = π) |
12 | | df-ov 7364 |
. . . . . . . . . . 11
β’ (ππ·π) = (π·ββ¨π, πβ©) |
13 | | opeq2 4835 |
. . . . . . . . . . . 12
β’ (π = π β β¨π, πβ© = β¨π, πβ©) |
14 | 13 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π = π β (π·ββ¨π, πβ©) = (π·ββ¨π, πβ©)) |
15 | 12, 14 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π = π β (ππ·π) = (π·ββ¨π, πβ©)) |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β (ππ·π) = (π·ββ¨π, πβ©)) |
17 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β π· β (PsMetβπ)) |
18 | 10 | simpld 496 |
. . . . . . . . . 10
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β π β π) |
19 | | psmet0 23684 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π β π) β (ππ·π) = 0) |
20 | 17, 18, 19 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β (ππ·π) = 0) |
21 | 16, 20 | eqtr3d 2775 |
. . . . . . . 8
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β (π·ββ¨π, πβ©) = 0) |
22 | | 0xr 11210 |
. . . . . . . . . 10
β’ 0 β
β* |
23 | | rpxr 12932 |
. . . . . . . . . 10
β’ (π β β+
β π β
β*) |
24 | | rpgt0 12935 |
. . . . . . . . . 10
β’ (π β β+
β 0 < π) |
25 | | lbico1 13327 |
. . . . . . . . . 10
β’ ((0
β β* β§ π β β* β§ 0 <
π) β 0 β
(0[,)π)) |
26 | 22, 23, 24, 25 | mp3an2i 1467 |
. . . . . . . . 9
β’ (π β β+
β 0 β (0[,)π)) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β 0 β
(0[,)π)) |
28 | 21, 27 | eqeltrd 2834 |
. . . . . . 7
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β (π·ββ¨π, πβ©) β (0[,)π)) |
29 | | psmetf 23682 |
. . . . . . . . . 10
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
30 | 29 | ffund 6676 |
. . . . . . . . 9
β’ (π· β (PsMetβπ) β Fun π·) |
31 | 30 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β Fun π·) |
32 | 11, 18 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β π β π) |
33 | 18, 32 | opelxpd 5675 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β
β¨π, πβ© β (π Γ π)) |
34 | 29 | fdmd 6683 |
. . . . . . . . . 10
β’ (π· β (PsMetβπ) β dom π· = (π Γ π)) |
35 | 34 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β dom π· = (π Γ π)) |
36 | 33, 35 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β
β¨π, πβ© β dom π·) |
37 | | fvimacnv 7007 |
. . . . . . . 8
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
38 | 31, 36, 37 | syl2anc 585 |
. . . . . . 7
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
39 | 28, 38 | mpbid 231 |
. . . . . 6
β’ ((((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β
β¨π, πβ© β (β‘π· β (0[,)π))) |
40 | 39 | adantr 482 |
. . . . 5
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β (β‘π· β (0[,)π))) |
41 | | simpr 486 |
. . . . 5
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π΄ = (β‘π· β (0[,)π))) |
42 | 40, 41 | eleqtrrd 2837 |
. . . 4
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β β¨π, πβ© β π΄) |
43 | | simplr 768 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β π΄ β πΉ) |
44 | | metust.1 |
. . . . . . 7
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
45 | 44 | metustel 23929 |
. . . . . 6
β’ (π· β (PsMetβπ) β (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
46 | 45 | ad2antrr 725 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
47 | 43, 46 | mpbid 231 |
. . . 4
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
48 | 42, 47 | r19.29a 3156 |
. . 3
β’ (((π· β (PsMetβπ) β§ π΄ β πΉ) β§ β¨π, πβ© β ( I βΎ π)) β β¨π, πβ© β π΄) |
49 | 48 | ex 414 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β (β¨π, πβ© β ( I βΎ π) β β¨π, πβ© β π΄)) |
50 | 2, 49 | relssdv 5748 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β ( I βΎ π) β π΄) |