Metamath Proof Explorer

Theorem xpsxmetlem

Description: Lemma for xpsxmet . (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 xpsxmetlem ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )

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 ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
12 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
13 eqid ⊢ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) )
14 eqid ⊢ ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
15 eqid ⊢ ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
16 fvexd ⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
17 2on ⊢ 2o ∈ On
18 17 a1i ⊢ ( 𝜑 → 2o ∈ On )
19 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ∈ V )
20 elpri ⊢ ( 𝑘 ∈ { ∅ , 1o } → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) )
21 df2o3 ⊢ 2o = { ∅ , 1o }
22 20 21 eleq2s ⊢ ( 𝑘 ∈ 2o → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) )
23 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
24 fveq2 ⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) )
25 fvpr0o ⊢ ( 𝑅 ∈ 𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
26 4 25 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
27 24 26 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑅 )
28 27 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑅 ) )
29 27 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑅 ) )
30 29 2 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑋 )
31 30 sqxpeqd ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑋 × 𝑋 ) )
32 28 31 reseq12d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) )
33 32 7 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑀 )
34 30 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ∞Met ‘ 𝑋 ) )
35 23 33 34 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
36 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
37 fveq2 ⊢ ( 𝑘 = 1o → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) )
38 fvpr1o ⊢ ( 𝑆 ∈ 𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
39 5 38 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
40 37 39 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑆 )
41 40 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑆 ) )
42 40 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑆 ) )
43 42 3 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑌 )
44 43 sqxpeqd ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑌 × 𝑌 ) )
45 41 44 reseq12d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) )
46 45 8 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑁 )
47 43 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ∞Met ‘ 𝑌 ) )
48 36 46 47 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑘 = 1o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
49 35 48 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑘 = ∅ ∨ 𝑘 = 1o ) ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
50 22 49 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
51 11 12 13 14 15 16 18 19 50 prdsxmet ⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
52 fnpr2o ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
53 4 5 52 syl2anc ⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
54 dffn5 ⊢ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o ↔ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
55 53 54 sylib ⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } = ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
56 55 oveq2d ⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
57 56 fveq2d ⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
58 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
59 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
60 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
61 1 2 3 4 5 58 59 60 xpsrnbas ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
62 56 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
63 61 62 eqtrd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
64 63 fveq2d ⊢ ( 𝜑 → ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) = ( ∞Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝑘 ∈ 2o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
65 51 57 64 3eltr4d ⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) )