Theorem xpsxmet

Description: A product metric of extended metrics is an extended metric. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	xpsds.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
	xpsds.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	xpsds.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
	xpsds.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	xpsds.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	xpsds.p	⊢ 𝑃 = ( dist ‘ 𝑇 )
	xpsds.m	⊢ 𝑀 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) )
	xpsds.n	⊢ 𝑁 = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
	xpsds.3	⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
	xpsds.4	⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
Assertion	xpsxmet	⊢ ( 𝜑 → 𝑃 ∈ ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpsds.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2		xpsds.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
3		xpsds.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
4		xpsds.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5		xpsds.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
6		xpsds.p	⊢ 𝑃 = ( dist ‘ 𝑇 )
7		xpsds.m	⊢ 𝑀 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) )
8		xpsds.n	⊢ 𝑁 = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
9		xpsds.3	⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
10		xpsds.4	⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
11		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
12		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
13		eqid	⊢ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
14	1 2 3 4 5 11 12 13	xpsval	⊢ ( 𝜑 → 𝑇 = ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
15	1 2 3 4 5 11 12 13	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
16	11	xpsff1o2	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
17		f1ocnv	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
18	16 17	mp1i	⊢ ( 𝜑 → ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
19		ovexd	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
20		eqid	⊢ ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) = ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
21	1 2 3 4 5 6 7 8 9 10	xpsxmetlem	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
22		ssid	⊢ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
23		xmetres2	⊢ ( ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ∧ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
24	21 22 23	sylancl	⊢ ( 𝜑 → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
25	14 15 18 19 20 6 24	imasf1oxmet	⊢ ( 𝜑 → 𝑃 ∈ ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) )