Metamath Proof Explorer


Theorem imasds

Description: The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 11-Jul-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasbas.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasbas.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasbas.r ( 𝜑𝑅𝑍 )
imasds.e 𝐸 = ( dist ‘ 𝑅 )
imasds.d 𝐷 = ( dist ‘ 𝑈 )
Assertion imasds ( 𝜑𝐷 = ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) )

Proof

Step Hyp Ref Expression
1 imasbas.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
2 imasbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 imasbas.f ( 𝜑𝐹 : 𝑉onto𝐵 )
4 imasbas.r ( 𝜑𝑅𝑍 )
5 imasds.e 𝐸 = ( dist ‘ 𝑅 )
6 imasds.d 𝐷 = ( dist ‘ 𝑈 )
7 eqid ( +g𝑅 ) = ( +g𝑅 )
8 eqid ( .r𝑅 ) = ( .r𝑅 )
9 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
10 eqid ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
11 eqid ( ·𝑠𝑅 ) = ( ·𝑠𝑅 )
12 eqid ( ·𝑖𝑅 ) = ( ·𝑖𝑅 )
13 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
14 eqid ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
15 eqidd ( 𝜑 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } )
16 eqidd ( 𝜑 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } )
17 eqidd ( 𝜑 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) = 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) )
18 eqidd ( 𝜑 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } )
19 eqidd ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
20 eqidd ( 𝜑 → ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) )
21 eqidd ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) )
22 1 2 7 8 9 10 11 12 13 5 14 15 16 17 18 19 20 21 3 4 imasval ( 𝜑𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) )
23 eqid ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } )
24 23 imasvalstr ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) Struct ⟨ 1 , 1 2 ⟩
25 dsid dist = Slot ( dist ‘ ndx )
26 snsstp3 { ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ⊆ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ }
27 ssun2 { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } )
28 26 27 sstri { ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , 𝑞𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝑝 ( ·𝑖𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ⟩ } )
29 fvex ( Base ‘ 𝑅 ) ∈ V
30 2 29 eqeltrdi ( 𝜑𝑉 ∈ V )
31 fornex ( 𝑉 ∈ V → ( 𝐹 : 𝑉onto𝐵𝐵 ∈ V ) )
32 30 3 31 sylc ( 𝜑𝐵 ∈ V )
33 mpoexga ( ( 𝐵 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ∈ V )
34 32 32 33 syl2anc ( 𝜑 → ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) ∈ V )
35 22 24 25 28 34 6 strfv3 ( 𝜑𝐷 = ( 𝑥𝐵 , 𝑦𝐵 ↦ inf ( 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( 𝐸𝑔 ) ) ) , ℝ* , < ) ) )