Metamath Proof Explorer

Theorem xpsmet

Description: The direct product of two metric spaces. Definition 14-1.5 of Gleason p. 225. (Contributed by NM, 20-Jun-2007) (Revised by Mario Carneiro, 20-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 ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
xpsmet.3 ⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
xpsmet.4 ⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑌 ) )
Assertion xpsmet ( 𝜑 → 𝑃 ∈ ( 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 xpsmet.3 ⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
10 xpsmet.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 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
22 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
23 eqid ⊢ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) )
24 eqid ⊢ ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
25 eqid ⊢ ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
26 fvexd ⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
27 2onn ⊢ 2o ∈ ω
28 nnfi ⊢ ( 2o ∈ ω → 2o ∈ Fin )
29 27 28 mp1i ⊢ ( 𝜑 → 2o ∈ Fin )
30 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ∈ V )
31 elpri ⊢ ( 𝑘 ∈ { ∅ , 1o } → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) )
32 df2o3 ⊢ 2o = { ∅ , 1o }
33 31 32 eleq2s ⊢ ( 𝑘 ∈ 2o → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) )
34 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
35 fveq2 ⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) )
36 fvpr0o ⊢ ( 𝑅 ∈ 𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
37 4 36 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
38 35 37 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑅 )
39 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑅 ) )
40 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑅 ) )
41 40 2 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑋 )
42 41 sqxpeqd ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑋 × 𝑋 ) )
43 39 42 reseq12d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) )
44 43 7 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑀 )
45 41 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( Met ‘ 𝑋 ) )
46 34 44 45 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
47 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → 𝑁 ∈ ( Met ‘ 𝑌 ) )
48 fveq2 ⊢ ( 𝑘 = 1o → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) )
49 fvpr1o ⊢ ( 𝑆 ∈ 𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
50 5 49 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
51 48 50 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑆 )
52 51 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑆 ) )
53 51 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑆 ) )
54 53 3 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑌 )
55 54 sqxpeqd ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑌 × 𝑌 ) )
56 52 55 reseq12d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) )
57 56 8 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑁 )
58 54 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( Met ‘ 𝑌 ) )
59 47 57 58 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
60 46 59 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑘 = ∅ ∨ 𝑘 = 1o ) ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
61 33 60 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
62 21 22 23 24 25 26 29 30 61 prdsmet ⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
63 fnpr2o ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
64 4 5 63 syl2anc ⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
65 dffn5 ⊢ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ↔ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
66 64 65 sylib ⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
67 66 oveq2d ⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
68 67 fveq2d ⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
69 67 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
70 15 69 eqtrd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
71 70 fveq2d ⊢ ( 𝜑 → ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) = ( Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
72 62 68 71 3eltr4d ⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
73 ssid ⊢ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
74 metres2 ⊢ ( ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ∧ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
75 72 73 74 sylancl ⊢ ( 𝜑 → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )
76 14 15 18 19 20 6 75 imasf1omet ⊢ ( 𝜑 → 𝑃 ∈ ( Met ‘ ( 𝑋 × 𝑌 ) ) )