Metamath Proof Explorer

Theorem tmsxps

Description: Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsxps.p ⊢P=dist⁡toMetSp⁡M×𝑠toMetSp⁡N
tmsxps.1 ⊢φ→M∈∞Met⁡X
tmsxps.2 ⊢φ→N∈∞Met⁡Y
Assertion tmsxps ⊢φ→P∈∞Met⁡X×Y

Proof

Step Hyp Ref Expression
1 tmsxps.p ⊢P=dist⁡toMetSp⁡M×𝑠toMetSp⁡N
2 tmsxps.1 ⊢φ→M∈∞Met⁡X
3 tmsxps.2 ⊢φ→N∈∞Met⁡Y
4 eqid ⊢toMetSp⁡M×𝑠toMetSp⁡N=toMetSp⁡M×𝑠toMetSp⁡N
5 eqid ⊢BasetoMetSp⁡M=BasetoMetSp⁡M
6 eqid ⊢BasetoMetSp⁡N=BasetoMetSp⁡N
7 eqid ⊢toMetSp⁡M=toMetSp⁡M
8 7 tmsxms ⊢M∈∞Met⁡X→toMetSp⁡M∈∞MetSp
9 2 8 syl ⊢φ→toMetSp⁡M∈∞MetSp
10 eqid ⊢toMetSp⁡N=toMetSp⁡N
11 10 tmsxms ⊢N∈∞Met⁡Y→toMetSp⁡N∈∞MetSp
12 3 11 syl ⊢φ→toMetSp⁡N∈∞MetSp
13 4 5 6 9 12 1 xpsdsfn2 ⊢φ→PFnBasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N
14 fnresdm ⊢PFnBasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N→P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N=P
15 13 14 syl ⊢φ→P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N=P
16 4 xpsxms ⊢toMetSp⁡M∈∞MetSp∧toMetSp⁡N∈∞MetSp→toMetSp⁡M×𝑠toMetSp⁡N∈∞MetSp
17 9 12 16 syl2anc ⊢φ→toMetSp⁡M×𝑠toMetSp⁡N∈∞MetSp
18 eqid ⊢BasetoMetSp⁡M×𝑠toMetSp⁡N=BasetoMetSp⁡M×𝑠toMetSp⁡N
19 18 1 xmsxmet2 ⊢toMetSp⁡M×𝑠toMetSp⁡N∈∞MetSp→P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N∈∞Met⁡BasetoMetSp⁡M×𝑠toMetSp⁡N
20 17 19 syl ⊢φ→P↾BasetoMetSp⁡M×𝑠toMetSp⁡N×BasetoMetSp⁡M×𝑠toMetSp⁡N∈∞Met⁡BasetoMetSp⁡M×𝑠toMetSp⁡N
21 15 20 eqeltrrd ⊢φ→P∈∞Met⁡BasetoMetSp⁡M×𝑠toMetSp⁡N
22 7 tmsbas ⊢M∈∞Met⁡X→X=BasetoMetSp⁡M
23 2 22 syl ⊢φ→X=BasetoMetSp⁡M
24 10 tmsbas ⊢N∈∞Met⁡Y→Y=BasetoMetSp⁡N
25 3 24 syl ⊢φ→Y=BasetoMetSp⁡N
26 23 25 xpeq12d ⊢φ→X×Y=BasetoMetSp⁡M×BasetoMetSp⁡N
27 4 5 6 9 12 xpsbas ⊢φ→BasetoMetSp⁡M×BasetoMetSp⁡N=BasetoMetSp⁡M×𝑠toMetSp⁡N
28 26 27 eqtrd ⊢φ→X×Y=BasetoMetSp⁡M×𝑠toMetSp⁡N
29 28 fveq2d ⊢φ→∞Met⁡X×Y=∞Met⁡BasetoMetSp⁡M×𝑠toMetSp⁡N
30 21 29 eleqtrrd ⊢φ→P∈∞Met⁡X×Y