Step | Hyp | Ref
| Expression |
1 | | metidss 32860 |
. . . 4
β’ (π· β (PsMetβπ) β
(~Metβπ·)
β (π Γ π)) |
2 | | xpss 5692 |
. . . 4
β’ (π Γ π) β (V Γ V) |
3 | 1, 2 | sstrdi 3994 |
. . 3
β’ (π· β (PsMetβπ) β
(~Metβπ·)
β (V Γ V)) |
4 | | df-rel 5683 |
. . 3
β’ (Rel
(~Metβπ·)
β (~Metβπ·) β (V Γ V)) |
5 | 3, 4 | sylibr 233 |
. 2
β’ (π· β (PsMetβπ) β Rel
(~Metβπ·)) |
6 | 1 | ssbrd 5191 |
. . . . 5
β’ (π· β (PsMetβπ) β (π₯(~Metβπ·)π¦ β π₯(π Γ π)π¦)) |
7 | 6 | imp 408 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π¦) β π₯(π Γ π)π¦) |
8 | | brxp 5724 |
. . . 4
β’ (π₯(π Γ π)π¦ β (π₯ β π β§ π¦ β π)) |
9 | 7, 8 | sylib 217 |
. . 3
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π¦) β (π₯ β π β§ π¦ β π)) |
10 | | psmetsym 23808 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯π·π¦) = (π¦π·π₯)) |
11 | 10 | 3expb 1121 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) = (π¦π·π₯)) |
12 | 11 | eqeq1d 2735 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β (π¦π·π₯) = 0)) |
13 | | metidv 32861 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯(~Metβπ·)π¦ β (π₯π·π¦) = 0)) |
14 | | metidv 32861 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π¦ β π β§ π₯ β π)) β (π¦(~Metβπ·)π₯ β (π¦π·π₯) = 0)) |
15 | 14 | ancom2s 649 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π¦(~Metβπ·)π₯ β (π¦π·π₯) = 0)) |
16 | 12, 13, 15 | 3bitr4d 311 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯(~Metβπ·)π¦ β π¦(~Metβπ·)π₯)) |
17 | 16 | biimpd 228 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯(~Metβπ·)π¦ β π¦(~Metβπ·)π₯)) |
18 | 17 | impancom 453 |
. . 3
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π¦) β ((π₯ β π β§ π¦ β π) β π¦(~Metβπ·)π₯)) |
19 | 9, 18 | mpd 15 |
. 2
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π¦) β π¦(~Metβπ·)π₯) |
20 | | simpl 484 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π· β (PsMetβπ)) |
21 | | simprr 772 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π¦(~Metβπ·)π§) |
22 | 1 | ssbrd 5191 |
. . . . . . . . . 10
β’ (π· β (PsMetβπ) β (π¦(~Metβπ·)π§ β π¦(π Γ π)π§)) |
23 | 22 | imp 408 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π¦(~Metβπ·)π§) β π¦(π Γ π)π§) |
24 | | brxp 5724 |
. . . . . . . . 9
β’ (π¦(π Γ π)π§ β (π¦ β π β§ π§ β π)) |
25 | 23, 24 | sylib 217 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π¦(~Metβπ·)π§) β (π¦ β π β§ π§ β π)) |
26 | 21, 25 | syldan 592 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π¦ β π β§ π§ β π)) |
27 | 26 | simpld 496 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π¦ β π) |
28 | | simprl 770 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π₯(~Metβπ·)π¦) |
29 | 28, 9 | syldan 592 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯ β π β§ π¦ β π)) |
30 | 29 | simpld 496 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π₯ β π) |
31 | 26 | simprd 497 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π§ β π) |
32 | | psmettri2 23807 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π¦ β π β§ π₯ β π β§ π§ β π)) β (π₯π·π§) β€ ((π¦π·π₯) +π (π¦π·π§))) |
33 | 20, 27, 30, 31, 32 | syl13anc 1373 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯π·π§) β€ ((π¦π·π₯) +π (π¦π·π§))) |
34 | 29, 11 | syldan 592 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯π·π¦) = (π¦π·π₯)) |
35 | 29, 13 | syldan 592 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯(~Metβπ·)π¦ β (π₯π·π¦) = 0)) |
36 | 28, 35 | mpbid 231 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯π·π¦) = 0) |
37 | 34, 36 | eqtr3d 2775 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π¦π·π₯) = 0) |
38 | | metidv 32861 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ (π¦ β π β§ π§ β π)) β (π¦(~Metβπ·)π§ β (π¦π·π§) = 0)) |
39 | 26, 38 | syldan 592 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π¦(~Metβπ·)π§ β (π¦π·π§) = 0)) |
40 | 21, 39 | mpbid 231 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π¦π·π§) = 0) |
41 | 37, 40 | oveq12d 7424 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β ((π¦π·π₯) +π (π¦π·π§)) = (0 +π
0)) |
42 | | 0xr 11258 |
. . . . . . 7
β’ 0 β
β* |
43 | | xaddrid 13217 |
. . . . . . 7
β’ (0 β
β* β (0 +π 0) = 0) |
44 | 42, 43 | ax-mp 5 |
. . . . . 6
β’ (0
+π 0) = 0 |
45 | 41, 44 | eqtrdi 2789 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β ((π¦π·π₯) +π (π¦π·π§)) = 0) |
46 | 33, 45 | breqtrd 5174 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯π·π§) β€ 0) |
47 | | psmetge0 23810 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π₯ β π β§ π§ β π) β 0 β€ (π₯π·π§)) |
48 | 20, 30, 31, 47 | syl3anc 1372 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β 0 β€ (π₯π·π§)) |
49 | | psmetcl 23805 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π₯ β π β§ π§ β π) β (π₯π·π§) β
β*) |
50 | 20, 30, 31, 49 | syl3anc 1372 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯π·π§) β
β*) |
51 | | xrletri3 13130 |
. . . . 5
β’ (((π₯π·π§) β β* β§ 0 β
β*) β ((π₯π·π§) = 0 β ((π₯π·π§) β€ 0 β§ 0 β€ (π₯π·π§)))) |
52 | 50, 42, 51 | sylancl 587 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β ((π₯π·π§) = 0 β ((π₯π·π§) β€ 0 β§ 0 β€ (π₯π·π§)))) |
53 | 46, 48, 52 | mpbir2and 712 |
. . 3
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯π·π§) = 0) |
54 | | metidv 32861 |
. . . 4
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π§ β π)) β (π₯(~Metβπ·)π§ β (π₯π·π§) = 0)) |
55 | 20, 30, 31, 54 | syl12anc 836 |
. . 3
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β (π₯(~Metβπ·)π§ β (π₯π·π§) = 0)) |
56 | 53, 55 | mpbird 257 |
. 2
β’ ((π· β (PsMetβπ) β§ (π₯(~Metβπ·)π¦ β§ π¦(~Metβπ·)π§)) β π₯(~Metβπ·)π§) |
57 | | psmet0 23806 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π₯ β π) β (π₯π·π₯) = 0) |
58 | | metidv 32861 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ (π₯ β π β§ π₯ β π)) β (π₯(~Metβπ·)π₯ β (π₯π·π₯) = 0)) |
59 | 58 | anabsan2 673 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π₯ β π) β (π₯(~Metβπ·)π₯ β (π₯π·π₯) = 0)) |
60 | 57, 59 | mpbird 257 |
. . 3
β’ ((π· β (PsMetβπ) β§ π₯ β π) β π₯(~Metβπ·)π₯) |
61 | 1 | ssbrd 5191 |
. . . . . 6
β’ (π· β (PsMetβπ) β (π₯(~Metβπ·)π₯ β π₯(π Γ π)π₯)) |
62 | 61 | imp 408 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π₯) β π₯(π Γ π)π₯) |
63 | | brxp 5724 |
. . . . 5
β’ (π₯(π Γ π)π₯ β (π₯ β π β§ π₯ β π)) |
64 | 62, 63 | sylib 217 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π₯) β (π₯ β π β§ π₯ β π)) |
65 | 64 | simpld 496 |
. . 3
β’ ((π· β (PsMetβπ) β§ π₯(~Metβπ·)π₯) β π₯ β π) |
66 | 60, 65 | impbida 800 |
. 2
β’ (π· β (PsMetβπ) β (π₯ β π β π₯(~Metβπ·)π₯)) |
67 | 5, 19, 56, 66 | iserd 8726 |
1
β’ (π· β (PsMetβπ) β
(~Metβπ·)
Er π) |