This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )