Metamath Proof Explorer

Theorem xpsxms

Description: A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis xpsms.t ⊒ 𝑇 = ( 𝑅 Γ—s 𝑆 )
Assertion xpsxms ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ 𝑇 ∈ ∞MetSp )

Proof

Step Hyp Ref Expression
1 xpsms.t ⊒ 𝑇 = ( 𝑅 Γ—s 𝑆 )
2 eqid ⊒ ( Base β€˜ 𝑅 ) = ( Base β€˜ 𝑅 )
3 eqid ⊒ ( Base β€˜ 𝑆 ) = ( Base β€˜ 𝑆 )
4 simpl ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ 𝑅 ∈ ∞MetSp )
5 simpr ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ 𝑆 ∈ ∞MetSp )
6 eqid ⊒ ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } )
7 eqid ⊒ ( Scalar β€˜ 𝑅 ) = ( Scalar β€˜ 𝑅 )
8 eqid ⊒ ( ( Scalar β€˜ 𝑅 ) Xs { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar β€˜ 𝑅 ) Xs { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
9 1 2 3 4 5 6 7 8 xpsval ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ 𝑇 = ( β—‘ ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) β€œs ( ( Scalar β€˜ 𝑅 ) Xs { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
10 1 2 3 4 5 6 7 8 xpsrnbas ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ ran ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base β€˜ ( ( Scalar β€˜ 𝑅 ) Xs { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
11 6 xpsff1o2 ⊒ ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base β€˜ 𝑅 ) Γ— ( Base β€˜ 𝑆 ) ) –1-1-ontoβ†’ ran ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } )
12 f1ocnv ⊒ ( ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base β€˜ 𝑅 ) Γ— ( Base β€˜ 𝑆 ) ) –1-1-ontoβ†’ ran ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) β†’ β—‘ ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-ontoβ†’ ( ( Base β€˜ 𝑅 ) Γ— ( Base β€˜ 𝑆 ) ) )
13 11 12 mp1i ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ β—‘ ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( π‘₯ ∈ ( Base β€˜ 𝑅 ) , 𝑦 ∈ ( Base β€˜ 𝑆 ) ↦ { ⟨ βˆ… , π‘₯ ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-ontoβ†’ ( ( Base β€˜ 𝑅 ) Γ— ( Base β€˜ 𝑆 ) ) )
14 fvexd ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ ( Scalar β€˜ 𝑅 ) ∈ V )
15 2onn ⊒ 2o ∈ Ο‰
16 nnfi ⊒ ( 2o ∈ Ο‰ β†’ 2o ∈ Fin )
17 15 16 mp1i ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ 2o ∈ Fin )
18 xpscf ⊒ ( { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟢ ∞MetSp ↔ ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) )
19 18 biimpri ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟢ ∞MetSp )
20 8 prdsxms ⊒ ( ( ( Scalar β€˜ 𝑅 ) ∈ V ∧ 2o ∈ Fin ∧ { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } : 2o ⟢ ∞MetSp ) β†’ ( ( Scalar β€˜ 𝑅 ) Xs { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ ∞MetSp )
21 14 17 19 20 syl3anc ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ ( ( Scalar β€˜ 𝑅 ) Xs { ⟨ βˆ… , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ ∞MetSp )
22 9 10 13 21 imasf1oxms ⊒ ( ( 𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp ) β†’ 𝑇 ∈ ∞MetSp )