Theorem xpsms

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	xpsms	⊢ ( ( 𝑅 ∈ 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	prdsms	⊢ ( ( ( 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	imasf1oms	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝑆 ∈ MetSp ) → 𝑇 ∈ MetSp )