Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . 5
β’ (((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β π β β+) |
2 | 1 | rpred 12965 |
. . . 4
β’ (((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β π β β) |
3 | | simplr 768 |
. . . . 5
β’ (((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β π β β+) |
4 | 3 | rpred 12965 |
. . . 4
β’ (((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β π β β) |
5 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π β β+) |
6 | 5 | rpred 12965 |
. . . . . . 7
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π β β) |
7 | | 0xr 11210 |
. . . . . . . . . 10
β’ 0 β
β* |
8 | 7 | a1i 11 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β 0 β
β*) |
9 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β β§ π β€ π) β π β β) |
10 | 9 | rexrd 11213 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β π β β*) |
11 | | 0le0 12262 |
. . . . . . . . . 10
β’ 0 β€
0 |
12 | 11 | a1i 11 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β 0 β€ 0) |
13 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β π β€ π) |
14 | | icossico 13343 |
. . . . . . . . 9
β’ (((0
β β* β§ π β β*) β§ (0 β€ 0
β§ π β€ π)) β (0[,)π) β (0[,)π)) |
15 | 8, 10, 12, 13, 14 | syl22anc 838 |
. . . . . . . 8
β’ ((π β β β§ π β€ π) β (0[,)π) β (0[,)π)) |
16 | | imass2 6058 |
. . . . . . . 8
β’
((0[,)π) β
(0[,)π) β (β‘π· β (0[,)π)) β (β‘π· β (0[,)π))) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ ((π β β β§ π β€ π) β (β‘π· β (0[,)π)) β (β‘π· β (0[,)π))) |
18 | 6, 17 | sylancom 589 |
. . . . . 6
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β (β‘π· β (0[,)π)) β (β‘π· β (0[,)π))) |
19 | | simplrl 776 |
. . . . . 6
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π΄ = (β‘π· β (0[,)π))) |
20 | | simplrr 777 |
. . . . . 6
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π΅ = (β‘π· β (0[,)π))) |
21 | 18, 19, 20 | 3sstr4d 3995 |
. . . . 5
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π΄ β π΅) |
22 | 21 | orcd 872 |
. . . 4
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β (π΄ β π΅ β¨ π΅ β π΄)) |
23 | | simplll 774 |
. . . . . . . 8
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π β β+) |
24 | 23 | rpred 12965 |
. . . . . . 7
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π β β) |
25 | 7 | a1i 11 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β 0 β
β*) |
26 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β β§ π β€ π) β π β β) |
27 | 26 | rexrd 11213 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β π β β*) |
28 | 11 | a1i 11 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β 0 β€ 0) |
29 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β β§ π β€ π) β π β€ π) |
30 | | icossico 13343 |
. . . . . . . . 9
β’ (((0
β β* β§ π β β*) β§ (0 β€ 0
β§ π β€ π)) β (0[,)π) β (0[,)π)) |
31 | 25, 27, 28, 29, 30 | syl22anc 838 |
. . . . . . . 8
β’ ((π β β β§ π β€ π) β (0[,)π) β (0[,)π)) |
32 | | imass2 6058 |
. . . . . . . 8
β’
((0[,)π) β
(0[,)π) β (β‘π· β (0[,)π)) β (β‘π· β (0[,)π))) |
33 | 31, 32 | syl 17 |
. . . . . . 7
β’ ((π β β β§ π β€ π) β (β‘π· β (0[,)π)) β (β‘π· β (0[,)π))) |
34 | 24, 33 | sylancom 589 |
. . . . . 6
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β (β‘π· β (0[,)π)) β (β‘π· β (0[,)π))) |
35 | | simplrr 777 |
. . . . . 6
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π΅ = (β‘π· β (0[,)π))) |
36 | | simplrl 776 |
. . . . . 6
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π΄ = (β‘π· β (0[,)π))) |
37 | 34, 35, 36 | 3sstr4d 3995 |
. . . . 5
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β π΅ β π΄) |
38 | 37 | olcd 873 |
. . . 4
β’ ((((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β§ π β€ π) β (π΄ β π΅ β¨ π΅ β π΄)) |
39 | 2, 4, 22, 38 | lecasei 11269 |
. . 3
β’ (((π β β+
β§ π β
β+) β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β (π΄ β π΅ β¨ π΅ β π΄)) |
40 | 39 | adantlll 717 |
. 2
β’
(((((π· β
(PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β§ π β β+) β§ π β β+)
β§ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) β (π΄ β π΅ β¨ π΅ β π΄)) |
41 | | metust.1 |
. . . . . 6
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
42 | 41 | metustel 23929 |
. . . . 5
β’ (π· β (PsMetβπ) β (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
43 | 42 | biimpa 478 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
44 | 43 | 3adant3 1133 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
45 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = π β (0[,)π) = (0[,)π)) |
46 | 45 | imaeq2d 6017 |
. . . . . . . . 9
β’ (π = π β (β‘π· β (0[,)π)) = (β‘π· β (0[,)π))) |
47 | 46 | cbvmptv 5222 |
. . . . . . . 8
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
48 | 47 | rneqi 5896 |
. . . . . . 7
β’ ran
(π β
β+ β¦ (β‘π· β (0[,)π))) = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
49 | 41, 48 | eqtri 2761 |
. . . . . 6
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
50 | 49 | metustel 23929 |
. . . . 5
β’ (π· β (PsMetβπ) β (π΅ β πΉ β βπ β β+ π΅ = (β‘π· β (0[,)π)))) |
51 | 50 | biimpa 478 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π΅ β πΉ) β βπ β β+ π΅ = (β‘π· β (0[,)π))) |
52 | 51 | 3adant2 1132 |
. . 3
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β βπ β β+ π΅ = (β‘π· β (0[,)π))) |
53 | | reeanv 3216 |
. . 3
β’
(βπ β
β+ βπ β β+ (π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π))) β (βπ β β+ π΄ = (β‘π· β (0[,)π)) β§ βπ β β+ π΅ = (β‘π· β (0[,)π)))) |
54 | 44, 52, 53 | sylanbrc 584 |
. 2
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β βπ β β+ βπ β β+
(π΄ = (β‘π· β (0[,)π)) β§ π΅ = (β‘π· β (0[,)π)))) |
55 | 40, 54 | r19.29vva 3204 |
1
β’ ((π· β (PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β (π΄ β π΅ β¨ π΅ β π΄)) |