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	prdsvallem	⊢ ( 𝜑 → ( Scalar ‘ 𝑃 ) = 𝑆 )
25	24	eqcomd	⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑃 ) )