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 ⊢ 𝑃 = ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) )
tmsxps.1 ⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
tmsxps.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
Assertion tmsxps ( 𝜑 → 𝑃 ∈ ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 tmsxps.p ⊢ 𝑃 = ( dist ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) )
2 tmsxps.1 ⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
3 tmsxps.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
4 eqid ⊢ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) = ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) )
5 eqid ⊢ ( Base ‘ ( toMetSp ‘ 𝑀 ) ) = ( Base ‘ ( toMetSp ‘ 𝑀 ) )
6 eqid ⊢ ( Base ‘ ( toMetSp ‘ 𝑁 ) ) = ( Base ‘ ( toMetSp ‘ 𝑁 ) )
7 eqid ⊢ ( toMetSp ‘ 𝑀 ) = ( toMetSp ‘ 𝑀 )
8 7 tmsxms ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp )
9 2 8 syl ⊢ ( 𝜑 → ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp )
10 eqid ⊢ ( toMetSp ‘ 𝑁 ) = ( toMetSp ‘ 𝑁 )
11 10 tmsxms ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp )
12 3 11 syl ⊢ ( 𝜑 → ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp )
13 4 5 6 9 12 1 xpsdsfn2 ⊢ ( 𝜑 → 𝑃 Fn ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) )
14 fnresdm ⊢ ( 𝑃 Fn ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) → ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) = 𝑃 )
15 13 14 syl ⊢ ( 𝜑 → ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) = 𝑃 )
16 4 xpsxms ⊢ ( ( ( toMetSp ‘ 𝑀 ) ∈ ∞MetSp ∧ ( toMetSp ‘ 𝑁 ) ∈ ∞MetSp ) → ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ∈ ∞MetSp )
17 9 12 16 syl2anc ⊢ ( 𝜑 → ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ∈ ∞MetSp )
18 eqid ⊢ ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) = ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) )
19 18 1 xmsxmet2 ⊢ ( ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ∈ ∞MetSp → ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) )
20 17 19 syl ⊢ ( 𝜑 → ( 𝑃 ↾ ( ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) × ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) )
21 15 20 eqeltrrd ⊢ ( 𝜑 → 𝑃 ∈ ( ∞Met ‘ ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) )
22 7 tmsbas ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ ( toMetSp ‘ 𝑀 ) ) )
23 2 22 syl ⊢ ( 𝜑 → 𝑋 = ( Base ‘ ( toMetSp ‘ 𝑀 ) ) )
24 10 tmsbas ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝑌 = ( Base ‘ ( toMetSp ‘ 𝑁 ) ) )
25 3 24 syl ⊢ ( 𝜑 → 𝑌 = ( Base ‘ ( toMetSp ‘ 𝑁 ) ) )
26 23 25 xpeq12d ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) )
27 4 5 6 9 12 xpsbas ⊢ ( 𝜑 → ( ( Base ‘ ( toMetSp ‘ 𝑀 ) ) × ( Base ‘ ( toMetSp ‘ 𝑁 ) ) ) = ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) )
28 26 27 eqtrd ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) )
29 28 fveq2d ⊢ ( 𝜑 → ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) = ( ∞Met ‘ ( Base ‘ ( ( toMetSp ‘ 𝑀 ) ×s ( toMetSp ‘ 𝑁 ) ) ) ) )
30 21 29 eleqtrrd ⊢ ( 𝜑 → 𝑃 ∈ ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) )