Step | Hyp | Ref
| Expression |
1 | | simp-4r 783 |
. . . 4
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π· β (PsMetβπ)) |
2 | | simplr 768 |
. . . . . 6
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β π β β+) |
3 | 2 | rphalfcld 12977 |
. . . . 5
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (π / 2) β
β+) |
4 | | eqidd 2734 |
. . . . 5
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β‘π· β (0[,)(π / 2))) = (β‘π· β (0[,)(π / 2)))) |
5 | | oveq2 7369 |
. . . . . . 7
β’ (π = (π / 2) β (0[,)π) = (0[,)(π / 2))) |
6 | 5 | imaeq2d 6017 |
. . . . . 6
β’ (π = (π / 2) β (β‘π· β (0[,)π)) = (β‘π· β (0[,)(π / 2)))) |
7 | 6 | rspceeqv 3599 |
. . . . 5
β’ (((π / 2) β β+
β§ (β‘π· β (0[,)(π / 2))) = (β‘π· β (0[,)(π / 2)))) β βπ β β+ (β‘π· β (0[,)(π / 2))) = (β‘π· β (0[,)π))) |
8 | 3, 4, 7 | syl2anc 585 |
. . . 4
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β βπ β β+ (β‘π· β (0[,)(π / 2))) = (β‘π· β (0[,)π))) |
9 | | metust.1 |
. . . . . . 7
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
10 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = π β (0[,)π) = (0[,)π)) |
11 | 10 | imaeq2d 6017 |
. . . . . . . . 9
β’ (π = π β (β‘π· β (0[,)π)) = (β‘π· β (0[,)π))) |
12 | 11 | cbvmptv 5222 |
. . . . . . . 8
β’ (π β β+
β¦ (β‘π· β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π))) |
13 | 12 | rneqi 5896 |
. . . . . . 7
β’ ran
(π β
β+ β¦ (β‘π· β (0[,)π))) = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
14 | 9, 13 | eqtri 2761 |
. . . . . 6
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
15 | 14 | metustel 23929 |
. . . . 5
β’ (π· β (PsMetβπ) β ((β‘π· β (0[,)(π / 2))) β πΉ β βπ β β+ (β‘π· β (0[,)(π / 2))) = (β‘π· β (0[,)π)))) |
16 | 15 | biimpar 479 |
. . . 4
β’ ((π· β (PsMetβπ) β§ βπ β β+
(β‘π· β (0[,)(π / 2))) = (β‘π· β (0[,)π))) β (β‘π· β (0[,)(π / 2))) β πΉ) |
17 | 1, 8, 16 | syl2anc 585 |
. . 3
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β‘π· β (0[,)(π / 2))) β πΉ) |
18 | | relco 6064 |
. . . . 5
β’ Rel
((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) |
19 | 18 | a1i 11 |
. . . 4
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β Rel ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) |
20 | | cossxp 6228 |
. . . . . . . . . 10
β’ ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β (dom (β‘π· β (0[,)(π / 2))) Γ ran (β‘π· β (0[,)(π / 2)))) |
21 | | cnvimass 6037 |
. . . . . . . . . . . . . 14
β’ (β‘π· β (0[,)(π / 2))) β dom π· |
22 | | psmetf 23682 |
. . . . . . . . . . . . . 14
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) |
23 | 21, 22 | fssdm 6692 |
. . . . . . . . . . . . 13
β’ (π· β (PsMetβπ) β (β‘π· β (0[,)(π / 2))) β (π Γ π)) |
24 | | dmss 5862 |
. . . . . . . . . . . . . 14
β’ ((β‘π· β (0[,)(π / 2))) β (π Γ π) β dom (β‘π· β (0[,)(π / 2))) β dom (π Γ π)) |
25 | | rnss 5898 |
. . . . . . . . . . . . . 14
β’ ((β‘π· β (0[,)(π / 2))) β (π Γ π) β ran (β‘π· β (0[,)(π / 2))) β ran (π Γ π)) |
26 | | xpss12 5652 |
. . . . . . . . . . . . . 14
β’ ((dom
(β‘π· β (0[,)(π / 2))) β dom (π Γ π) β§ ran (β‘π· β (0[,)(π / 2))) β ran (π Γ π)) β (dom (β‘π· β (0[,)(π / 2))) Γ ran (β‘π· β (0[,)(π / 2)))) β (dom (π Γ π) Γ ran (π Γ π))) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((β‘π· β (0[,)(π / 2))) β (π Γ π) β (dom (β‘π· β (0[,)(π / 2))) Γ ran (β‘π· β (0[,)(π / 2)))) β (dom (π Γ π) Γ ran (π Γ π))) |
28 | 23, 27 | syl 17 |
. . . . . . . . . . . 12
β’ (π· β (PsMetβπ) β (dom (β‘π· β (0[,)(π / 2))) Γ ran (β‘π· β (0[,)(π / 2)))) β (dom (π Γ π) Γ ran (π Γ π))) |
29 | 28 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β
β§ π· β (PsMetβπ)) β (dom (β‘π· β (0[,)(π / 2))) Γ ran (β‘π· β (0[,)(π / 2)))) β (dom (π Γ π) Γ ran (π Γ π))) |
30 | | dmxp 5888 |
. . . . . . . . . . . . 13
β’ (π β β
β dom (π Γ π) = π) |
31 | | rnxp 6126 |
. . . . . . . . . . . . 13
β’ (π β β
β ran (π Γ π) = π) |
32 | 30, 31 | xpeq12d 5668 |
. . . . . . . . . . . 12
β’ (π β β
β (dom (π Γ π) Γ ran (π Γ π)) = (π Γ π)) |
33 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β
β§ π· β (PsMetβπ)) β (dom (π Γ π) Γ ran (π Γ π)) = (π Γ π)) |
34 | 29, 33 | sseqtrd 3988 |
. . . . . . . . . 10
β’ ((π β β
β§ π· β (PsMetβπ)) β (dom (β‘π· β (0[,)(π / 2))) Γ ran (β‘π· β (0[,)(π / 2)))) β (π Γ π)) |
35 | 20, 34 | sstrid 3959 |
. . . . . . . . 9
β’ ((π β β
β§ π· β (PsMetβπ)) β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β (π Γ π)) |
36 | 35 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β (π Γ π)) |
37 | 36 | sselda 3948 |
. . . . . . 7
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β β¨π, πβ© β (π Γ π)) |
38 | | opelxp 5673 |
. . . . . . 7
β’
(β¨π, πβ© β (π Γ π) β (π β π β§ π β π)) |
39 | 37, 38 | sylib 217 |
. . . . . 6
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β (π β π β§ π β π)) |
40 | | simpll 766 |
. . . . . . 7
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ (π β π β§ π β π)) β ((((π β β
β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π)))) |
41 | | simprl 770 |
. . . . . . 7
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ (π β π β§ π β π)) β π β π) |
42 | | simprr 772 |
. . . . . . 7
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ (π β π β§ π β π)) β π β π) |
43 | | simplr 768 |
. . . . . . 7
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ (π β π β§ π β π)) β β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) |
44 | | simplll 774 |
. . . . . . . . . . . . . . 15
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (((((π β β
β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π)) |
45 | 44 | simp1d 1143 |
. . . . . . . . . . . . . 14
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((((π β β
β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π)))) |
46 | 45, 1 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π· β (PsMetβπ)) |
47 | 45, 2 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β β+) |
48 | 46, 47 | jca 513 |
. . . . . . . . . . . 12
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π· β (PsMetβπ) β§ π β
β+)) |
49 | 44 | simp2d 1144 |
. . . . . . . . . . . 12
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
50 | 44 | simp3d 1145 |
. . . . . . . . . . . 12
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
51 | 48, 49, 50 | 3jca 1129 |
. . . . . . . . . . 11
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((π· β (PsMetβπ) β§ π β β+) β§ π β π β§ π β π)) |
52 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
53 | | simprl 770 |
. . . . . . . . . . 11
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π(β‘π· β (0[,)(π / 2)))π) |
54 | | simprr 772 |
. . . . . . . . . . 11
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π(β‘π· β (0[,)(π / 2)))π) |
55 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((π· β (PsMetβπ) β§ π β β+) β§ π β π β§ π β π)) |
56 | 55 | simp1d 1143 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π· β (PsMetβπ) β§ π β
β+)) |
57 | 56 | simpld 496 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π· β (PsMetβπ)) |
58 | 22 | ffund 6676 |
. . . . . . . . . . . . 13
β’ (π· β (PsMetβπ) β Fun π·) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β Fun π·) |
60 | 55 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
61 | 55 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
62 | 60, 61 | opelxpd 5675 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β (π Γ π)) |
63 | 22 | fdmd 6683 |
. . . . . . . . . . . . . 14
β’ (π· β (PsMetβπ) β dom π· = (π Γ π)) |
64 | 57, 63 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β dom π· = (π Γ π)) |
65 | 62, 64 | eleqtrrd 2837 |
. . . . . . . . . . . 12
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β dom π·) |
66 | | 0xr 11210 |
. . . . . . . . . . . . . 14
β’ 0 β
β* |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β 0 β
β*) |
68 | 56 | simprd 497 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β β+) |
69 | 68 | rpxrd 12966 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β β*) |
70 | 57, 22 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π·:(π Γ π)βΆβ*) |
71 | 70, 62 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π·ββ¨π, πβ©) β
β*) |
72 | | psmetge0 23688 |
. . . . . . . . . . . . . . 15
β’ ((π· β (PsMetβπ) β§ π β π β§ π β π) β 0 β€ (ππ·π)) |
73 | 57, 60, 61, 72 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β 0 β€ (ππ·π)) |
74 | | df-ov 7364 |
. . . . . . . . . . . . . 14
β’ (ππ·π) = (π·ββ¨π, πβ©) |
75 | 73, 74 | breqtrdi 5150 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β 0 β€ (π·ββ¨π, πβ©)) |
76 | 74, 71 | eqeltrid 2838 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) β
β*) |
77 | | 0red 11166 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β 0 β β) |
78 | 68 | rpred 12965 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β β) |
79 | 78 | rehalfcld 12408 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π / 2) β β) |
80 | 79 | rexrd 11213 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π / 2) β
β*) |
81 | | df-ov 7364 |
. . . . . . . . . . . . . . . . . . . 20
β’ (ππ·π) = (π·ββ¨π, πβ©) |
82 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
83 | 60, 82 | opelxpd 5675 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β (π Γ π)) |
84 | 83, 64 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β dom π·) |
85 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π(β‘π· β (0[,)(π / 2)))π) |
86 | | df-br 5110 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π(β‘π· β (0[,)(π / 2)))π β β¨π, πβ© β (β‘π· β (0[,)(π / 2)))) |
87 | 85, 86 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β (β‘π· β (0[,)(π / 2)))) |
88 | | fvimacnv 7007 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)(π / 2)) β β¨π, πβ© β (β‘π· β (0[,)(π / 2))))) |
89 | 88 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((Fun
π· β§ β¨π, πβ© β dom π·) β§ β¨π, πβ© β (β‘π· β (0[,)(π / 2)))) β (π·ββ¨π, πβ©) β (0[,)(π / 2))) |
90 | 59, 84, 87, 89 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π·ββ¨π, πβ©) β (0[,)(π / 2))) |
91 | 81, 90 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) β (0[,)(π / 2))) |
92 | | elico2 13337 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((0
β β β§ (π /
2) β β*) β ((ππ·π) β (0[,)(π / 2)) β ((ππ·π) β β β§ 0 β€ (ππ·π) β§ (ππ·π) < (π / 2)))) |
93 | 92 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((0
β β β§ (π /
2) β β*) β§ (ππ·π) β (0[,)(π / 2))) β ((ππ·π) β β β§ 0 β€ (ππ·π) β§ (ππ·π) < (π / 2))) |
94 | 93 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
β’ (((0
β β β§ (π /
2) β β*) β§ (ππ·π) β (0[,)(π / 2))) β (ππ·π) β β) |
95 | 77, 80, 91, 94 | syl21anc 837 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) β β) |
96 | | df-ov 7364 |
. . . . . . . . . . . . . . . . . . . 20
β’ (ππ·π) = (π·ββ¨π, πβ©) |
97 | 82, 61 | opelxpd 5675 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β (π Γ π)) |
98 | 97, 64 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β dom π·) |
99 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π(β‘π· β (0[,)(π / 2)))π) |
100 | | df-br 5110 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π(β‘π· β (0[,)(π / 2)))π β β¨π, πβ© β (β‘π· β (0[,)(π / 2)))) |
101 | 99, 100 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β β¨π, πβ© β (β‘π· β (0[,)(π / 2)))) |
102 | | fvimacnv 7007 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)(π / 2)) β β¨π, πβ© β (β‘π· β (0[,)(π / 2))))) |
103 | 102 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((Fun
π· β§ β¨π, πβ© β dom π·) β§ β¨π, πβ© β (β‘π· β (0[,)(π / 2)))) β (π·ββ¨π, πβ©) β (0[,)(π / 2))) |
104 | 59, 98, 101, 103 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π·ββ¨π, πβ©) β (0[,)(π / 2))) |
105 | 96, 104 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) β (0[,)(π / 2))) |
106 | | elico2 13337 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((0
β β β§ (π /
2) β β*) β ((ππ·π) β (0[,)(π / 2)) β ((ππ·π) β β β§ 0 β€ (ππ·π) β§ (ππ·π) < (π / 2)))) |
107 | 106 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((0
β β β§ (π /
2) β β*) β§ (ππ·π) β (0[,)(π / 2))) β ((ππ·π) β β β§ 0 β€ (ππ·π) β§ (ππ·π) < (π / 2))) |
108 | 107 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
β’ (((0
β β β§ (π /
2) β β*) β§ (ππ·π) β (0[,)(π / 2))) β (ππ·π) β β) |
109 | 77, 80, 105, 108 | syl21anc 837 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) β β) |
110 | 95, 109 | rexaddd 13162 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((ππ·π) +π (ππ·π)) = ((ππ·π) + (ππ·π))) |
111 | 95, 109 | readdcld 11192 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((ππ·π) + (ππ·π)) β β) |
112 | 110, 111 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((ππ·π) +π (ππ·π)) β β) |
113 | 112 | rexrd 11213 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((ππ·π) +π (ππ·π)) β
β*) |
114 | | psmettri 23687 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (PsMetβπ) β§ (π β π β§ π β π β§ π β π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
115 | 57, 60, 61, 82, 114 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) β€ ((ππ·π) +π (ππ·π))) |
116 | 93 | simp3d 1145 |
. . . . . . . . . . . . . . . . . 18
β’ (((0
β β β§ (π /
2) β β*) β§ (ππ·π) β (0[,)(π / 2))) β (ππ·π) < (π / 2)) |
117 | 77, 80, 91, 116 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) < (π / 2)) |
118 | 107 | simp3d 1145 |
. . . . . . . . . . . . . . . . . 18
β’ (((0
β β β§ (π /
2) β β*) β§ (ππ·π) β (0[,)(π / 2))) β (ππ·π) < (π / 2)) |
119 | 77, 80, 105, 118 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) < (π / 2)) |
120 | 95, 109, 78, 117, 119 | lt2halvesd 12409 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((ππ·π) + (ππ·π)) < π) |
121 | 110, 120 | eqbrtrd 5131 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ((ππ·π) +π (ππ·π)) < π) |
122 | 76, 113, 69, 115, 121 | xrlelttrd 13088 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ·π) < π) |
123 | 74, 122 | eqbrtrrid 5145 |
. . . . . . . . . . . . 13
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π·ββ¨π, πβ©) < π) |
124 | 67, 69, 71, 75, 123 | elicod 13323 |
. . . . . . . . . . . 12
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (π·ββ¨π, πβ©) β (0[,)π)) |
125 | | fvimacnv 7007 |
. . . . . . . . . . . . . 14
β’ ((Fun
π· β§ β¨π, πβ© β dom π·) β ((π·ββ¨π, πβ©) β (0[,)π) β β¨π, πβ© β (β‘π· β (0[,)π)))) |
126 | 125 | biimpa 478 |
. . . . . . . . . . . . 13
β’ (((Fun
π· β§ β¨π, πβ© β dom π·) β§ (π·ββ¨π, πβ©) β (0[,)π)) β β¨π, πβ© β (β‘π· β (0[,)π))) |
127 | | df-br 5110 |
. . . . . . . . . . . . 13
β’ (π(β‘π· β (0[,)π))π β β¨π, πβ© β (β‘π· β (0[,)π))) |
128 | 126, 127 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((Fun
π· β§ β¨π, πβ© β dom π·) β§ (π·ββ¨π, πβ©) β (0[,)π)) β π(β‘π· β (0[,)π))π) |
129 | 59, 65, 124, 128 | syl21anc 837 |
. . . . . . . . . . 11
β’
(((((π· β
(PsMetβπ) β§ π β β+)
β§ π β π β§ π β π) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π(β‘π· β (0[,)π))π) |
130 | 51, 52, 53, 54, 129 | syl22anc 838 |
. . . . . . . . . 10
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π(β‘π· β (0[,)π))π) |
131 | 45 | simprd 497 |
. . . . . . . . . . 11
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π΄ = (β‘π· β (0[,)π))) |
132 | 131 | breqd 5120 |
. . . . . . . . . 10
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β (ππ΄π β π(β‘π· β (0[,)π))π)) |
133 | 130, 132 | mpbird 257 |
. . . . . . . . 9
β’
(((((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ π β π) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β ππ΄π) |
134 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) |
135 | | df-br 5110 |
. . . . . . . . . . . . 13
β’ (π((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))π β β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) |
136 | 134, 135 | sylibr 233 |
. . . . . . . . . . . 12
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β π((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))π) |
137 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π β V |
138 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π β V |
139 | 137, 138 | brco 5830 |
. . . . . . . . . . . 12
β’ (π((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))π β βπ(π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) |
140 | 136, 139 | sylib 217 |
. . . . . . . . . . 11
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β βπ(π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) |
141 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β
β§ π· β (PsMetβπ)) β (β‘π· β (0[,)(π / 2))) β (π Γ π)) |
142 | 141, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β
β§ π· β (PsMetβπ)) β ran (β‘π· β (0[,)(π / 2))) β ran (π Γ π)) |
143 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β
β§ π· β (PsMetβπ)) β ran (π Γ π) = π) |
144 | 142, 143 | sseqtrd 3988 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β
β§ π· β (PsMetβπ)) β ran (β‘π· β (0[,)(π / 2))) β π) |
145 | 144 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π(β‘π· β (0[,)(π / 2)))π) β ran (β‘π· β (0[,)(π / 2))) β π) |
146 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β V |
147 | 137, 146 | brelrn 5901 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(β‘π· β (0[,)(π / 2)))π β π β ran (β‘π· β (0[,)(π / 2)))) |
148 | 147 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π(β‘π· β (0[,)(π / 2)))π) β π β ran (β‘π· β (0[,)(π / 2)))) |
149 | 145, 148 | sseldd 3949 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π(β‘π· β (0[,)(π / 2)))π) β π β π) |
150 | 149 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β
β§ π· β (PsMetβπ)) β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) β π β π) |
151 | 150 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β π β π)) |
152 | 151 | ancrd 553 |
. . . . . . . . . . . . . . 15
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β (π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)))) |
153 | 152 | eximdv 1921 |
. . . . . . . . . . . . . 14
β’ ((π β β
β§ π· β (PsMetβπ)) β (βπ(π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β βπ(π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)))) |
154 | 153 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (βπ(π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β βπ(π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)))) |
155 | 154 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β (βπ(π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β βπ(π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)))) |
156 | 155 | adantr 482 |
. . . . . . . . . . 11
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β (βπ(π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β βπ(π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)))) |
157 | 140, 156 | mpd 15 |
. . . . . . . . . 10
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β βπ(π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π))) |
158 | | df-rex 3071 |
. . . . . . . . . 10
β’
(βπ β
π (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π) β βπ(π β π β§ (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π))) |
159 | 157, 158 | sylibr 233 |
. . . . . . . . 9
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β βπ β π (π(β‘π· β (0[,)(π / 2)))π β§ π(β‘π· β (0[,)(π / 2)))π)) |
160 | 133, 159 | r19.29a 3156 |
. . . . . . . 8
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β ππ΄π) |
161 | | df-br 5110 |
. . . . . . . 8
β’ (ππ΄π β β¨π, πβ© β π΄) |
162 | 160, 161 | sylib 217 |
. . . . . . 7
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ π β π β§ π β π) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β β¨π, πβ© β π΄) |
163 | 40, 41, 42, 43, 162 | syl31anc 1374 |
. . . . . 6
β’
(((((((π β
β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β§ (π β π β§ π β π)) β β¨π, πβ© β π΄) |
164 | 39, 163 | mpdan 686 |
. . . . 5
β’
((((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β§ β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) β β¨π, πβ© β π΄) |
165 | 164 | ex 414 |
. . . 4
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β (β¨π, πβ© β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β β¨π, πβ© β π΄)) |
166 | 19, 165 | relssdv 5748 |
. . 3
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β π΄) |
167 | | id 22 |
. . . . . 6
β’ (π£ = (β‘π· β (0[,)(π / 2))) β π£ = (β‘π· β (0[,)(π / 2)))) |
168 | 167, 167 | coeq12d 5824 |
. . . . 5
β’ (π£ = (β‘π· β (0[,)(π / 2))) β (π£ β π£) = ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2))))) |
169 | 168 | sseq1d 3979 |
. . . 4
β’ (π£ = (β‘π· β (0[,)(π / 2))) β ((π£ β π£) β π΄ β ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β π΄)) |
170 | 169 | rspcev 3583 |
. . 3
β’ (((β‘π· β (0[,)(π / 2))) β πΉ β§ ((β‘π· β (0[,)(π / 2))) β (β‘π· β (0[,)(π / 2)))) β π΄) β βπ£ β πΉ (π£ β π£) β π΄) |
171 | 17, 166, 170 | syl2anc 585 |
. 2
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π΄ β πΉ) β§ π β β+) β§ π΄ = (β‘π· β (0[,)π))) β βπ£ β πΉ (π£ β π£) β π΄) |
172 | 9 | metustel 23929 |
. . . 4
β’ (π· β (PsMetβπ) β (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
173 | 172 | adantl 483 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β (π΄ β πΉ β βπ β β+ π΄ = (β‘π· β (0[,)π)))) |
174 | 173 | biimpa 478 |
. 2
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β βπ β β+ π΄ = (β‘π· β (0[,)π))) |
175 | 171, 174 | r19.29a 3156 |
1
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β βπ£ β πΉ (π£ β π£) β π΄) |