Metamath Proof Explorer


Theorem prdsvsca

Description: Scalar multiplication in a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015) (Revised 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 𝑅 = 𝐼 )
prdsvsca.k 𝐾 = ( Base ‘ 𝑆 )
prdsvsca.m · = ( ·𝑠𝑃 )
Assertion prdsvsca ( 𝜑· = ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p 𝑃 = ( 𝑆 Xs 𝑅 )
2 prdsbas.s ( 𝜑𝑆𝑉 )
3 prdsbas.r ( 𝜑𝑅𝑊 )
4 prdsbas.b 𝐵 = ( Base ‘ 𝑃 )
5 prdsbas.i ( 𝜑 → dom 𝑅 = 𝐼 )
6 prdsvsca.k 𝐾 = ( Base ‘ 𝑆 )
7 prdsvsca.m · = ( ·𝑠𝑃 )
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 eqidd ( 𝜑 → ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) = ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
14 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) )
15 eqidd ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
16 eqidd ( 𝜑 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ( le ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ( le ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) } )
17 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
18 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) = ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) )
19 eqidd ( 𝜑 → ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) )
20 1 6 5 8 10 12 13 14 15 16 17 18 19 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 ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ) )
21 vscaid ·𝑠 = Slot ( ·𝑠 ‘ ndx )
22 ovssunirn ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ⊆ ran ( ·𝑠 ‘ ( 𝑅𝑥 ) )
23 21 strfvss ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ( 𝑅𝑥 )
24 fvssunirn ( 𝑅𝑥 ) ⊆ ran 𝑅
25 rnss ( ( 𝑅𝑥 ) ⊆ ran 𝑅 → ran ( 𝑅𝑥 ) ⊆ ran ran 𝑅 )
26 uniss ( ran ( 𝑅𝑥 ) ⊆ ran ran 𝑅 ran ( 𝑅𝑥 ) ⊆ ran ran 𝑅 )
27 24 25 26 mp2b ran ( 𝑅𝑥 ) ⊆ ran ran 𝑅
28 23 27 sstri ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ran 𝑅
29 rnss ( ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ran 𝑅 → ran ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ran ran 𝑅 )
30 uniss ( ran ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ran ran 𝑅 ran ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ran ran 𝑅 )
31 28 29 30 mp2b ran ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ⊆ ran ran ran 𝑅
32 22 31 sstri ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ⊆ ran ran ran 𝑅
33 ovex ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ∈ V
34 33 elpw ( ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ∈ 𝒫 ran ran ran 𝑅 ↔ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ⊆ ran ran ran 𝑅 )
35 32 34 mpbir ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ∈ 𝒫 ran ran ran 𝑅
36 35 a1i ( ( 𝜑𝑥𝐼 ) → ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ∈ 𝒫 ran ran ran 𝑅 )
37 36 fmpttd ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) : 𝐼 ⟶ 𝒫 ran ran ran 𝑅 )
38 rnexg ( 𝑅𝑊 → ran 𝑅 ∈ V )
39 uniexg ( ran 𝑅 ∈ V → ran 𝑅 ∈ V )
40 3 38 39 3syl ( 𝜑 ran 𝑅 ∈ V )
41 rnexg ( ran 𝑅 ∈ V → ran ran 𝑅 ∈ V )
42 uniexg ( ran ran 𝑅 ∈ V → ran ran 𝑅 ∈ V )
43 40 41 42 3syl ( 𝜑 ran ran 𝑅 ∈ V )
44 rnexg ( ran ran 𝑅 ∈ V → ran ran ran 𝑅 ∈ V )
45 uniexg ( ran ran ran 𝑅 ∈ V → ran ran ran 𝑅 ∈ V )
46 pwexg ( ran ran ran 𝑅 ∈ V → 𝒫 ran ran ran 𝑅 ∈ V )
47 43 44 45 46 4syl ( 𝜑 → 𝒫 ran ran ran 𝑅 ∈ V )
48 3 dmexd ( 𝜑 → dom 𝑅 ∈ V )
49 5 48 eqeltrrd ( 𝜑𝐼 ∈ V )
50 47 49 elmapd ( 𝜑 → ( ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∈ ( 𝒫 ran ran ran 𝑅m 𝐼 ) ↔ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) : 𝐼 ⟶ 𝒫 ran ran ran 𝑅 ) )
51 37 50 mpbird ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∈ ( 𝒫 ran ran ran 𝑅m 𝐼 ) )
52 51 ralrimivw ( 𝜑 → ∀ 𝑔𝐵 ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∈ ( 𝒫 ran ran ran 𝑅m 𝐼 ) )
53 52 ralrimivw ( 𝜑 → ∀ 𝑓𝐾𝑔𝐵 ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∈ ( 𝒫 ran ran ran 𝑅m 𝐼 ) )
54 eqid ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) = ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) )
55 54 fmpo ( ∀ 𝑓𝐾𝑔𝐵 ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∈ ( 𝒫 ran ran ran 𝑅m 𝐼 ) ↔ ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ran ran ran 𝑅m 𝐼 ) )
56 53 55 sylib ( 𝜑 → ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ran ran ran 𝑅m 𝐼 ) )
57 6 fvexi 𝐾 ∈ V
58 4 fvexi 𝐵 ∈ V
59 57 58 xpex ( 𝐾 × 𝐵 ) ∈ V
60 ovex ( 𝒫 ran ran ran 𝑅m 𝐼 ) ∈ V
61 fex2 ( ( ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ran ran ran 𝑅m 𝐼 ) ∧ ( 𝐾 × 𝐵 ) ∈ V ∧ ( 𝒫 ran ran ran 𝑅m 𝐼 ) ∈ V ) → ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ∈ V )
62 59 60 61 mp3an23 ( ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ran ran ran 𝑅m 𝐼 ) → ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ∈ V )
63 56 62 syl ( 𝜑 → ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ∈ V )
64 snsstp2 { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ⊆ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ }
65 ssun2 { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } )
66 64 65 sstri { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } )
67 ssun1 ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ⊆ ( ( { ⟨ ( 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 ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
68 66 67 sstri { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ⊆ ( ( { ⟨ ( 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 ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
69 20 7 21 63 68 prdsbaslem ( 𝜑· = ( 𝑓𝐾 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )