Description: Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tmsxps.p | |
|
tmsxps.1 | |
||
tmsxps.2 | |
||
tmsxpsval.a | |
||
tmsxpsval.b | |
||
tmsxpsval.c | |
||
tmsxpsval.d | |
||
Assertion | tmsxpsval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tmsxps.p | |
|
2 | tmsxps.1 | |
|
3 | tmsxps.2 | |
|
4 | tmsxpsval.a | |
|
5 | tmsxpsval.b | |
|
6 | tmsxpsval.c | |
|
7 | tmsxpsval.d | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | 11 | tmsxms | |
13 | 2 12 | syl | |
14 | eqid | |
|
15 | 14 | tmsxms | |
16 | 3 15 | syl | |
17 | eqid | |
|
18 | eqid | |
|
19 | 11 | tmsds | |
20 | 2 19 | syl | |
21 | 11 | tmsbas | |
22 | 2 21 | syl | |
23 | 22 | fveq2d | |
24 | 2 20 23 | 3eltr3d | |
25 | ssid | |
|
26 | xmetres2 | |
|
27 | 24 25 26 | sylancl | |
28 | 14 | tmsds | |
29 | 3 28 | syl | |
30 | 14 | tmsbas | |
31 | 3 30 | syl | |
32 | 31 | fveq2d | |
33 | 3 29 32 | 3eltr3d | |
34 | ssid | |
|
35 | xmetres2 | |
|
36 | 33 34 35 | sylancl | |
37 | 4 22 | eleqtrd | |
38 | 5 31 | eleqtrd | |
39 | 6 22 | eleqtrd | |
40 | 7 31 | eleqtrd | |
41 | 8 9 10 13 16 1 17 18 27 36 37 38 39 40 | xpsdsval | |
42 | 37 39 | ovresd | |
43 | 20 | oveqd | |
44 | 42 43 | eqtr4d | |
45 | 38 40 | ovresd | |
46 | 29 | oveqd | |
47 | 45 46 | eqtr4d | |
48 | 44 47 | preq12d | |
49 | 48 | supeq1d | |
50 | 41 49 | eqtrd | |