This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdssca

Description: Scalar ring of 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 ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion prdssca ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2 prdsbas.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3 prdsbas.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 eqidd ⊢ ( 𝜑 → dom 𝑅 = dom 𝑅 )
6 eqidd ⊢ ( 𝜑 → X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
7 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
8 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
9 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
10 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
11 eqidd ⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
12 eqidd ⊢ ( 𝜑 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝑅 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝑅 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
13 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
15 eqidd ⊢ ( 𝜑 → ( 𝑎 ∈ ( X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
16 1 4 5 6 7 8 9 10 11 12 13 14 15 2 3 prdsval ⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝑅 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )
17 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
18 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
19 snsstp1 ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ } ⊆ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ }
20 ssun2 ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } )
21 19 20 sstri ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } )
22 ssun1 ⊢ ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝑅 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
23 21 22 sstri ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σg ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝑅 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ dom 𝑅 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ dom 𝑅 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑅 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
24 16 17 18 2 23 prdsbaslem ⊢ ( 𝜑 → ( Scalar ‘ 𝑃 ) = 𝑆 )
25 24 eqcomd ⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑃 ) )