Metamath Proof Explorer


Theorem tmsxpsval

Description: Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsxps.p P=disttoMetSpM×𝑠toMetSpN
tmsxps.1 φM∞MetX
tmsxps.2 φN∞MetY
tmsxpsval.a φAX
tmsxpsval.b φBY
tmsxpsval.c φCX
tmsxpsval.d φDY
Assertion tmsxpsval φABPCD=supAMCBND*<

Proof

Step Hyp Ref Expression
1 tmsxps.p P=disttoMetSpM×𝑠toMetSpN
2 tmsxps.1 φM∞MetX
3 tmsxps.2 φN∞MetY
4 tmsxpsval.a φAX
5 tmsxpsval.b φBY
6 tmsxpsval.c φCX
7 tmsxpsval.d φDY
8 eqid toMetSpM×𝑠toMetSpN=toMetSpM×𝑠toMetSpN
9 eqid BasetoMetSpM=BasetoMetSpM
10 eqid BasetoMetSpN=BasetoMetSpN
11 eqid toMetSpM=toMetSpM
12 11 tmsxms M∞MetXtoMetSpM∞MetSp
13 2 12 syl φtoMetSpM∞MetSp
14 eqid toMetSpN=toMetSpN
15 14 tmsxms N∞MetYtoMetSpN∞MetSp
16 3 15 syl φtoMetSpN∞MetSp
17 eqid disttoMetSpMBasetoMetSpM×BasetoMetSpM=disttoMetSpMBasetoMetSpM×BasetoMetSpM
18 eqid disttoMetSpNBasetoMetSpN×BasetoMetSpN=disttoMetSpNBasetoMetSpN×BasetoMetSpN
19 11 tmsds M∞MetXM=disttoMetSpM
20 2 19 syl φM=disttoMetSpM
21 11 tmsbas M∞MetXX=BasetoMetSpM
22 2 21 syl φX=BasetoMetSpM
23 22 fveq2d φ∞MetX=∞MetBasetoMetSpM
24 2 20 23 3eltr3d φdisttoMetSpM∞MetBasetoMetSpM
25 ssid BasetoMetSpMBasetoMetSpM
26 xmetres2 disttoMetSpM∞MetBasetoMetSpMBasetoMetSpMBasetoMetSpMdisttoMetSpMBasetoMetSpM×BasetoMetSpM∞MetBasetoMetSpM
27 24 25 26 sylancl φdisttoMetSpMBasetoMetSpM×BasetoMetSpM∞MetBasetoMetSpM
28 14 tmsds N∞MetYN=disttoMetSpN
29 3 28 syl φN=disttoMetSpN
30 14 tmsbas N∞MetYY=BasetoMetSpN
31 3 30 syl φY=BasetoMetSpN
32 31 fveq2d φ∞MetY=∞MetBasetoMetSpN
33 3 29 32 3eltr3d φdisttoMetSpN∞MetBasetoMetSpN
34 ssid BasetoMetSpNBasetoMetSpN
35 xmetres2 disttoMetSpN∞MetBasetoMetSpNBasetoMetSpNBasetoMetSpNdisttoMetSpNBasetoMetSpN×BasetoMetSpN∞MetBasetoMetSpN
36 33 34 35 sylancl φdisttoMetSpNBasetoMetSpN×BasetoMetSpN∞MetBasetoMetSpN
37 4 22 eleqtrd φABasetoMetSpM
38 5 31 eleqtrd φBBasetoMetSpN
39 6 22 eleqtrd φCBasetoMetSpM
40 7 31 eleqtrd φDBasetoMetSpN
41 8 9 10 13 16 1 17 18 27 36 37 38 39 40 xpsdsval φABPCD=supAdisttoMetSpMBasetoMetSpM×BasetoMetSpMCBdisttoMetSpNBasetoMetSpN×BasetoMetSpND*<
42 37 39 ovresd φAdisttoMetSpMBasetoMetSpM×BasetoMetSpMC=AdisttoMetSpMC
43 20 oveqd φAMC=AdisttoMetSpMC
44 42 43 eqtr4d φAdisttoMetSpMBasetoMetSpM×BasetoMetSpMC=AMC
45 38 40 ovresd φBdisttoMetSpNBasetoMetSpN×BasetoMetSpND=BdisttoMetSpND
46 29 oveqd φBND=BdisttoMetSpND
47 45 46 eqtr4d φBdisttoMetSpNBasetoMetSpN×BasetoMetSpND=BND
48 44 47 preq12d φAdisttoMetSpMBasetoMetSpM×BasetoMetSpMCBdisttoMetSpNBasetoMetSpN×BasetoMetSpND=AMCBND
49 48 supeq1d φsupAdisttoMetSpMBasetoMetSpM×BasetoMetSpMCBdisttoMetSpNBasetoMetSpN×BasetoMetSpND*<=supAMCBND*<
50 41 49 eqtrd φABPCD=supAMCBND*<