Theorem rlocbas

Description: The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocbas.b	$$⊢B={\mathrm{Base}}_R$$
	rlocbas.1	$$⊢\underset{\dot{}}{0}=0_R$$
	rlocbas.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rlocbas.3	$$⊢\underset{\dot{}}{-}={-}_R$$
	rlocbas.w	$$⊢W=B\times S$$
	rlocbas.l	No typesetting found for |- L = ( R RLocal S ) with typecode |-
	rlocbas.4	No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
	rlocbas.r	$$⊢\phi \to R\in V$$
	rlocbas.s	$$⊢\phi \to S\subseteq B$$
Assertion	rlocbas	$$⊢\phi \to W/\underset{\dot{}}{\sim }={\mathrm{Base}}_L$$

Proof

Step	Hyp	Ref	Expression
1		rlocbas.b	$$⊢B={\mathrm{Base}}_R$$
2		rlocbas.1	$$⊢\underset{\dot{}}{0}=0_R$$
3		rlocbas.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		rlocbas.3	$$⊢\underset{\dot{}}{-}={-}_R$$
5		rlocbas.w	$$⊢W=B\times S$$
6		rlocbas.l	Could not format L = ( R RLocal S ) : No typesetting found for |- L = ( R RLocal S ) with typecode |-
7		rlocbas.4	Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
8		rlocbas.r	$$⊢\phi \to R\in V$$
9		rlocbas.s	$$⊢\phi \to S\subseteq B$$
10		eqid	$$⊢{+}_R={+}_R$$
11		eqid	$$⊢{\le }_R={\le }_R$$
12		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
13		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
14		eqid	$$⊢{\cdot }_R={\cdot }_R$$
15		eqid	$$⊢\mathrm{TopSet}\left(R\right)=\mathrm{TopSet}\left(R\right)$$
16		eqid	$$⊢\mathrm{dist}\left(R\right)=\mathrm{dist}\left(R\right)$$
17		eqid	$$⊢\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)=\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)$$
18		eqid	$$⊢\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)=\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)$$
19		eqid	$$⊢\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)=\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)$$
20		eqid	$$⊢\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}=\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}$$
21		eqid	$$⊢\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)$$
22	1 2 3 4 10 11 12 13 14 5 7 15 16 17 18 19 20 21 8 9	rlocval	Could not format ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , ( a e. W , b e. W |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( +g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. W , b e. W |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` R ) ) , a e. W |-> <. ( k ( .s ` R ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` R ) tX ( ( TopSet ` R ) |`t S ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( le ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. W , b e. W |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( dist ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) >. } ) /s .~ ) ) : No typesetting found for |- ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , ( a e. W , b e. W |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( +g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. W , b e. W |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` R ) ) , a e. W |-> <. ( k ( .s ` R ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` R ) tX ( ( TopSet ` R ) |`t S ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( le ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. W , b e. W |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( dist ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) >. } ) /s .~ ) ) with typecode |-
23	6 22	eqtrid	$$⊢\phi \to L=\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
24		eqidd	$$⊢\phi \to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}$$
25		eqid	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}$$
26	25	imasvalstr	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right)\mathrm{Struct}⟨1,12⟩$$
27		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
28		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}$$
29		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}$$
30		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}$$
31	29 30	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}$$
32	28 31	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}$$
33	1	fvexi	$$⊢B\in \mathrm{V}$$
34	33	a1i	$$⊢\phi \to B\in \mathrm{V}$$
35	34 9	ssexd	$$⊢\phi \to S\in \mathrm{V}$$
36	34 35	xpexd	$$⊢\phi \to B\times S\in \mathrm{V}$$
37	5 36	eqeltrid	$$⊢\phi \to W\in \mathrm{V}$$
38		eqid	$$⊢{\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right)}={\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right)}$$
39	24 26 27 32 37 38	strfv3	$$⊢\phi \to {\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right)}=W$$
40	39	eqcomd	$$⊢\phi \to W={\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right)}$$
41	7	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
42	41	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
43		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\in \mathrm{V}$$
44		tpex	$$⊢\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\in \mathrm{V}$$
45	43 44	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\in \mathrm{V}$$
46		tpex	$$⊢\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\in \mathrm{V}$$
47	45 46	unex	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\in \mathrm{V}$$
48	47	a1i	$$⊢\phi \to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){+}_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in W⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(R\right){\times }_t\left(\mathrm{TopSet}\left(R\right){\upharpoonright }_{𝑡}S\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right){\le }_R\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(R\right)\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)⟩\right\}\in \mathrm{V}$$
49	23 40 42 48	qusbas	$$⊢\phi \to W/\underset{\dot{}}{\sim }={\mathrm{Base}}_L$$