# 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)

Ref Expression
Hypotheses prdsbas.p ${⊢}{P}={S}{⨉}_{𝑠}{R}$
prdsbas.s ${⊢}{\phi }\to {S}\in {V}$
prdsbas.r ${⊢}{\phi }\to {R}\in {W}$
Assertion prdssca ${⊢}{\phi }\to {S}=\mathrm{Scalar}\left({P}\right)$

### Proof

Step Hyp Ref Expression
1 prdsbas.p ${⊢}{P}={S}{⨉}_{𝑠}{R}$
2 prdsbas.s ${⊢}{\phi }\to {S}\in {V}$
3 prdsbas.r ${⊢}{\phi }\to {R}\in {W}$
4 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
5 eqidd ${⊢}{\phi }\to \mathrm{dom}{R}=\mathrm{dom}{R}$
6 eqidd ${⊢}{\phi }\to \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}=\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
7 eqidd ${⊢}{\phi }\to \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
8 eqidd ${⊢}{\phi }\to \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
9 eqidd ${⊢}{\phi }\to \left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
10 eqidd ${⊢}{\phi }\to \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)=\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
11 eqidd ${⊢}{\phi }\to {\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)$
12 eqidd ${⊢}{\phi }\to \left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\wedge \forall {x}\in \mathrm{dom}{R}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}=\left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\wedge \forall {x}\in \mathrm{dom}{R}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}$
13 eqidd ${⊢}{\phi }\to \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)=\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$
14 eqidd ${⊢}{\phi }\to \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)=\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
15 eqidd ${⊢}{\phi }\to \left({a}\in \left(\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}×\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\right),{c}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({d}\in \left({c}\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right){2}^{nd}\left({a}\right)\right),{e}\in \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)\left({a}\right)⟼\left({x}\in \mathrm{dom}{R}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)=\left({a}\in \left(\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}×\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\right),{c}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({d}\in \left({c}\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right){2}^{nd}\left({a}\right)\right),{e}\in \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)\left({a}\right)⟼\left({x}\in \mathrm{dom}{R}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)$
16 1 4 5 6 7 8 9 10 11 12 13 14 15 2 3 prdsval ${⊢}{\phi }\to {P}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟩,⟨{+}_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\wedge \forall {x}\in \mathrm{dom}{R}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left(\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}×\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\right),{c}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({d}\in \left({c}\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right){2}^{nd}\left({a}\right)\right),{e}\in \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)\left({a}\right)⟼\left({x}\in \mathrm{dom}{R}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)⟩\right\}\right)$
17 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
18 scaid ${⊢}\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$
19 2 elexd ${⊢}{\phi }\to {S}\in \mathrm{V}$
20 snsstp1 ${⊢}\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩\right\}\subseteq \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}$
21 ssun2 ${⊢}\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟩,⟨{+}_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}$
22 20 21 sstri ${⊢}\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟩,⟨{+}_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}$
23 ssun1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟩,⟨{+}_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟩,⟨{+}_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\wedge \forall {x}\in \mathrm{dom}{R}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left(\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}×\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\right),{c}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({d}\in \left({c}\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right){2}^{nd}\left({a}\right)\right),{e}\in \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)\left({a}\right)⟼\left({x}\in \mathrm{dom}{R}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)⟩\right\}\right)$
24 22 23 sstri ${⊢}\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟩,⟨{+}_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},\left({f}\in {\mathrm{Base}}_{{S}},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({x}\in \mathrm{dom}{R}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\wedge \forall {x}\in \mathrm{dom}{R}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{R}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left(\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}×\underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}\right),{c}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\left({d}\in \left({c}\left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right){2}^{nd}\left({a}\right)\right),{e}\in \left({f}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)},{g}\in \underset{{x}\in \mathrm{dom}{R}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}⟼\underset{{x}\in \mathrm{dom}{R}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)\left({a}\right)⟼\left({x}\in \mathrm{dom}{R}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)⟩\right\}\right)$
25 16 17 18 19 24 prdsvallem ${⊢}{\phi }\to \mathrm{Scalar}\left({P}\right)={S}$
26 25 eqcomd ${⊢}{\phi }\to {S}=\mathrm{Scalar}\left({P}\right)$