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 β€˜ ( 𝑋 Γ— π‘Œ ) ) )