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 ⊢ Base toMetSp ⁡ M = Base toMetSp ⁡ M
6 eqid ⊢ Base toMetSp ⁡ N = Base toMetSp ⁡ 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 ⊢ φ → P Fn Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
14 fnresdm ⊢ P Fn Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N → P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = P
15 13 14 syl ⊢ φ → P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ 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 ⊢ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N = Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
19 18 1 xmsxmet2 ⊢ toMetSp ⁡ M × 𝑠 toMetSp ⁡ N ∈ ∞MetSp → P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N ∈ ∞Met ⁡ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
20 17 19 syl ⊢ φ → P ↾ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N × Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N ∈ ∞Met ⁡ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
21 15 20 eqeltrrd ⊢ φ → P ∈ ∞Met ⁡ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
22 7 tmsbas ⊢ M ∈ ∞Met ⁡ X → X = Base toMetSp ⁡ M
23 2 22 syl ⊢ φ → X = Base toMetSp ⁡ M
24 10 tmsbas ⊢ N ∈ ∞Met ⁡ Y → Y = Base toMetSp ⁡ N
25 3 24 syl ⊢ φ → Y = Base toMetSp ⁡ N
26 23 25 xpeq12d ⊢ φ → X × Y = Base toMetSp ⁡ M × Base toMetSp ⁡ N
27 4 5 6 9 12 xpsbas ⊢ φ → Base toMetSp ⁡ M × Base toMetSp ⁡ N = Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
28 26 27 eqtrd ⊢ φ → X × Y = Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
29 28 fveq2d ⊢ φ → ∞Met ⁡ X × Y = ∞Met ⁡ Base toMetSp ⁡ M × 𝑠 toMetSp ⁡ N
30 21 29 eleqtrrd ⊢ φ → P ∈ ∞Met ⁡ X × Y