Theorem prdsbas

Description: Base set of a structure product. (Contributed by Stefan O'Rear, 3-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$$
	prdsbas.b	$$⊢B={\mathrm{Base}}_P$$
	prdsbas.i	$$⊢\phi \to \mathrm{dom}R=I$$
Assertion	prdsbas	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\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		prdsbas.b	$$⊢B={\mathrm{Base}}_P$$
5		prdsbas.i	$$⊢\phi \to \mathrm{dom}R=I$$
6		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
7		eqidd	$$⊢\phi \to \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$
8		eqidd	$$⊢\phi \to \left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)=\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)$$
9		eqidd	$$⊢\phi \to \left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)=\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)$$
10		eqidd	$$⊢\phi \to \left(f\in {\mathrm{Base}}_S,g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)=\left(f\in {\mathrm{Base}}_S,g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)$$
11		eqidd	$$⊢\phi \to \left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\sum }_S}\left(f\left(x\right){\cdot }_{𝑖}\left(R\left(x\right)\right)g\left(x\right)\right)\right)$$
12		eqidd	$$⊢\phi \to {\prod }_{𝑡}\left(\mathrm{TopOpen}\circ R\right)={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ R\right)$$
13		eqidd	$$⊢\phi \to \left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\wedge \forall x\in If\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\wedge \forall x\in If\left(x\right){\le }_{R\left(x\right)}g\left(x\right)\right)\right\}$$
14		eqidd	$$⊢\phi \to \left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼sup\left(\mathrm{ran}\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$$
15		eqidd	$$⊢\phi \to \left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(R\left(x\right)\right)g\left(x\right)\right)\right)$$
16		eqidd	$$⊢\phi \to \left(a\in \left(\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\times \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\right),c\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(d\in \left(c\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\times \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\right),c\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(d\in \left(c\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I⟼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)$$
17	1 6 5 7 8 9 10 11 12 13 14 15 16 2 3	prdsval	$$⊢\phi \to P=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\wedge \forall x\in If\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼sup\left(\mathrm{ran}\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\times \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\right),c\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(d\in \left(c\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I⟼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)$$
18		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
19	18	strfvss	$$⊢{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}R\left(x\right)$$
20		fvssunirn	$$⊢R\left(x\right)\subseteq \bigcup \mathrm{ran}R$$
21		rnss	$$⊢R\left(x\right)\subseteq \bigcup \mathrm{ran}R\to \mathrm{ran}R\left(x\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}R$$
22		uniss	$$⊢\mathrm{ran}R\left(x\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}R\to \bigcup \mathrm{ran}R\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R$$
23	20 21 22	mp2b	$$⊢\bigcup \mathrm{ran}R\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R$$
24	19 23	sstri	$$⊢{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R$$
25	24	rgenw	$$⊢\forall x\in I{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R$$
26		iunss	$$⊢\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R\leftrightarrow \forall x\in I{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R$$
27	25 26	mpbir	$$⊢\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R$$
28		rnexg	$$⊢R\in W\to \mathrm{ran}R\in \mathrm{V}$$
29		uniexg	$$⊢\mathrm{ran}R\in \mathrm{V}\to \bigcup \mathrm{ran}R\in \mathrm{V}$$
30	3 28 29	3syl	$$⊢\phi \to \bigcup \mathrm{ran}R\in \mathrm{V}$$
31		rnexg	$$⊢\bigcup \mathrm{ran}R\in \mathrm{V}\to \mathrm{ran}\bigcup \mathrm{ran}R\in \mathrm{V}$$
32		uniexg	$$⊢\mathrm{ran}\bigcup \mathrm{ran}R\in \mathrm{V}\to \bigcup \mathrm{ran}\bigcup \mathrm{ran}R\in \mathrm{V}$$
33	30 31 32	3syl	$$⊢\phi \to \bigcup \mathrm{ran}\bigcup \mathrm{ran}R\in \mathrm{V}$$
34		ssexg	$$⊢\left(\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}R\wedge \bigcup \mathrm{ran}\bigcup \mathrm{ran}R\in \mathrm{V}\right)\to \bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
35	27 33 34	sylancr	$$⊢\phi \to \bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
36		ixpssmap2g	$$⊢\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}\to \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\subseteq {\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}}^I$$
37		ovex	$$⊢{\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}}^I\in \mathrm{V}$$
38	37	ssex	$$⊢\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\subseteq {\bigcup _{x\in I}{\mathrm{Base}}_{R\left(x\right)}}^I\to \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
39	35 36 38	3syl	$$⊢\phi \to \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\in \mathrm{V}$$
40		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩\right\}$$
41		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\sum }_S}\left(f\left(x\right){\cdot }_{𝑖}\left(R\left(x\right)\right)g\left(x\right)\right)\right)⟩\right\}$$
42	40 41	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\sum }_S}\left(f\left(x\right){\cdot }_{𝑖}\left(R\left(x\right)\right)g\left(x\right)\right)\right)⟩\right\}$$
43		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\wedge \forall x\in If\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼sup\left(\mathrm{ran}\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\times \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\right),c\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(d\in \left(c\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I⟼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)$$
44	42 43	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f\left(x\right){+}_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(x\in I⟼f{\cdot }_{R\left(x\right)}g\left(x\right)\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{{\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\wedge \forall x\in If\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼sup\left(\mathrm{ran}\left(x\in I⟼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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\times \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}\right),c\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\left(d\in \left(c\left(f\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I}{⨉}{\mathrm{Base}}_{R\left(x\right)},g\in \underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}⟼\underset{x\in I}{⨉}\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 I⟼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)$$
45	17 4 18 39 44	prdsvallem	$$⊢\phi \to B=\underset{x\in I}{⨉}{\mathrm{Base}}_{R\left(x\right)}$$