Metamath Proof Explorer


Theorem prdsds

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Hypotheses prdsbas.p 𝑃 = ( 𝑆 Xs 𝑅 )
prdsbas.s ( 𝜑𝑆𝑉 )
prdsbas.r ( 𝜑𝑅𝑊 )
prdsbas.b 𝐵 = ( Base ‘ 𝑃 )
prdsbas.i ( 𝜑 → dom 𝑅 = 𝐼 )
prdsds.l 𝐷 = ( dist ‘ 𝑃 )
Assertion prdsds ( 𝜑𝐷 = ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p 𝑃 = ( 𝑆 Xs 𝑅 )
2 prdsbas.s ( 𝜑𝑆𝑉 )
3 prdsbas.r ( 𝜑𝑅𝑊 )
4 prdsbas.b 𝐵 = ( Base ‘ 𝑃 )
5 prdsbas.i ( 𝜑 → dom 𝑅 = 𝐼 )
6 prdsds.l 𝐷 = ( dist ‘ 𝑃 )
7 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 1 2 3 4 5 prdsbas ( 𝜑𝐵 = X 𝑥𝐼 ( Base ‘ ( 𝑅𝑥 ) ) )
9 eqid ( +g𝑃 ) = ( +g𝑃 )
10 1 2 3 4 5 9 prdsplusg ( 𝜑 → ( +g𝑃 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
11 eqid ( .r𝑃 ) = ( .r𝑃 )
12 1 2 3 4 5 11 prdsmulr ( 𝜑 → ( .r𝑃 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
13 eqid ( ·𝑠𝑃 ) = ( ·𝑠𝑃 )
14 1 2 3 4 5 7 13 prdsvsca ( 𝜑 → ( ·𝑠𝑃 ) = ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
15 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) )
16 eqidd ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
17 eqid ( le ‘ 𝑃 ) = ( le ‘ 𝑃 )
18 1 2 3 4 5 17 prdsle ( 𝜑 → ( le ‘ 𝑃 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ( le ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) } )
19 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
20 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) = ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) )
21 eqidd ( 𝜑 → ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) )
22 1 7 5 8 10 12 14 15 16 18 19 20 21 2 3 prdsval ( 𝜑𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠𝑃 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ) )
23 dsid dist = Slot ( dist ‘ ndx )
24 4 fvexi 𝐵 ∈ V
25 xrex * ∈ V
26 25 uniex * ∈ V
27 26 pwex 𝒫 * ∈ V
28 df-sup sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) = { 𝑦 ∈ ℝ* ∣ ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ* ( 𝑧 < 𝑦 → ∃ 𝑤 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝑤 ) ) }
29 ssrab2 { 𝑦 ∈ ℝ* ∣ ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ* ( 𝑧 < 𝑦 → ∃ 𝑤 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝑤 ) ) } ⊆ ℝ*
30 29 unissi { 𝑦 ∈ ℝ* ∣ ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ* ( 𝑧 < 𝑦 → ∃ 𝑤 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝑤 ) ) } ⊆ *
31 26 30 elpwi2 { 𝑦 ∈ ℝ* ∣ ( ∀ 𝑧 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ* ( 𝑧 < 𝑦 → ∃ 𝑤 ∈ ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) 𝑧 < 𝑤 ) ) } ∈ 𝒫 *
32 28 31 eqeltri sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ 𝒫 *
33 32 rgen2w 𝑓𝐵𝑔𝐵 sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ 𝒫 *
34 24 24 27 33 mpoexw ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ∈ V
35 34 a1i ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ∈ V )
36 snsstp3 { ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ⊆ { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ }
37 ssun1 { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } )
38 36 37 sstri { ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } )
39 ssun2 ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠𝑃 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
40 38 39 sstri { ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠𝑃 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
41 22 6 23 35 40 prdsbaslem ( 𝜑𝐷 = ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )