Theorem rlocmulval

Description: Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocaddval.1	$$⊢B={\mathrm{Base}}_R$$
	rlocaddval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rlocaddval.3	$$⊢\underset{\dot{}}{+}={+}_R$$
	rlocaddval.4	No typesetting found for |- L = ( R RLocal S ) with typecode |-
	rlocaddval.5	No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
	rlocaddval.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	rlocaddval.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
	rlocaddval.6	$$⊢\phi \to E\in B$$
	rlocaddval.7	$$⊢\phi \to F\in B$$
	rlocaddval.8	$$⊢\phi \to G\in S$$
	rlocaddval.9	$$⊢\phi \to H\in S$$
	rlocmulval.1	$$⊢\underset{\dot{}}{\otimes }={\cdot }_L$$
Assertion	rlocmulval	$$⊢\phi \to \left[⟨E,G⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{\otimes }\left[⟨F,H⟩\right]\underset{\dot{}}{\sim }=\left[⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩\right]\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		rlocaddval.1	$$⊢B={\mathrm{Base}}_R$$
2		rlocaddval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		rlocaddval.3	$$⊢\underset{\dot{}}{+}={+}_R$$
4		rlocaddval.4	Could not format L = ( R RLocal S ) : No typesetting found for |- L = ( R RLocal S ) with typecode |-
5		rlocaddval.5	Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
6		rlocaddval.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		rlocaddval.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
8		rlocaddval.6	$$⊢\phi \to E\in B$$
9		rlocaddval.7	$$⊢\phi \to F\in B$$
10		rlocaddval.8	$$⊢\phi \to G\in S$$
11		rlocaddval.9	$$⊢\phi \to H\in S$$
12		rlocmulval.1	$$⊢\underset{\dot{}}{\otimes }={\cdot }_L$$
13	8 10	opelxpd	$$⊢\phi \to ⟨E,G⟩\in \left(B\times S\right)$$
14	9 11	opelxpd	$$⊢\phi \to ⟨F,H⟩\in \left(B\times S\right)$$
15		eqid	$$⊢0_R=0_R$$
16		eqid	$$⊢{-}_R={-}_R$$
17		eqid	$$⊢{\le }_R={\le }_R$$
18		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
19		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
20		eqid	$$⊢{\cdot }_R={\cdot }_R$$
21		eqid	$$⊢B\times S=B\times S$$
22		eqid	$$⊢\mathrm{TopSet}\left(R\right)=\mathrm{TopSet}\left(R\right)$$
23		eqid	$$⊢\mathrm{dist}\left(R\right)=\mathrm{dist}\left(R\right)$$
24		eqid	$$⊢\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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)$$
25		eqid	$$⊢\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)$$
26		eqid	$$⊢\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},a\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)$$
27		eqid	$$⊢\left\{⟨a,b⟩|\left(\left(a\in \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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\}$$
28		eqid	$$⊢\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)$$
29		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
30	29 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
31	30	submss	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to S\subseteq B$$
32	7 31	syl	$$⊢\phi \to S\subseteq B$$
33	1 15 2 16 3 17 18 19 20 21 5 22 23 24 25 26 27 28 6 32	rlocval	Could not format ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , ( B X. S ) >. , <. ( +g ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` R ) ) , a e. ( B X. S ) |-> <. ( 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. ( B X. S ) /\ b e. ( B X. S ) ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( le ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( dist ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) >. } ) /s .~ ) ) : No typesetting found for |- ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , ( B X. S ) >. , <. ( +g ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` R ) ) , a e. ( B X. S ) |-> <. ( 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. ( B X. S ) /\ b e. ( B X. S ) ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( le ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( dist ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) >. } ) /s .~ ) ) with typecode |-
34	4 33	eqtrid	$$⊢\phi \to L=\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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 }$$
35		eqidd	$$⊢\phi \to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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\}$$
36		eqid	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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\}$$
37	36	imasvalstr	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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⟩$$
38		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
39		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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\}$$
40		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}$$
41		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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\}$$
42	40 41	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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\}$$
43	39 42	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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\}$$
44	1	fvexi	$$⊢B\in \mathrm{V}$$
45	44	a1i	$$⊢\phi \to B\in \mathrm{V}$$
46	45 7	xpexd	$$⊢\phi \to B\times S\in \mathrm{V}$$
47		eqid	$$⊢{\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}$$
48	35 37 38 43 46 47	strfv3	$$⊢\phi \to {\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}=B\times S$$
49	48	eqcomd	$$⊢\phi \to B\times S={\mathrm{Base}}_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}$$
50		eqid	$$⊢1_R=1_R$$
51	1 15 50 2 16 21 5 6 7	erler	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}\left(B\times S\right)$$
52		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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}$$
53		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 \left(B\times S\right)⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\in \mathrm{V}$$
54	52 53	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨k{\cdot }_R{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\in \mathrm{V}$$
55		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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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}$$
56	54 55	unex	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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}$$
57	56	a1i	$$⊢\phi \to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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}$$
58	32	ad2antrr	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to S\subseteq B$$
59	58	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\to S\subseteq B$$
60	59	ad2antrr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to S\subseteq B$$
61		eqidd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩=⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩$$
62		eqidd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to ⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩=⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
63	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
64	63	ad6antr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to R\in \mathrm{Ring}$$
65		simplr	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to u\underset{\dot{}}{\sim }p$$
66	1 5 58 65	erlcl1	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to u\in \left(B\times S\right)$$
67	66	ad4antr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to u\in \left(B\times S\right)$$
68		xp1st	$$⊢u\in \left(B\times S\right)\to 1^{st}\left(u\right)\in B$$
69	67 68	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(u\right)\in B$$
70		simpr	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to v\underset{\dot{}}{\sim }q$$
71	1 5 58 70	erlcl1	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to v\in \left(B\times S\right)$$
72	71	ad4antr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to v\in \left(B\times S\right)$$
73		xp1st	$$⊢v\in \left(B\times S\right)\to 1^{st}\left(v\right)\in B$$
74	72 73	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(v\right)\in B$$
75	1 2 64 69 74	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\in B$$
76	1 5 58 65	erlcl2	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to p\in \left(B\times S\right)$$
77	76	ad4antr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to p\in \left(B\times S\right)$$
78		xp1st	$$⊢p\in \left(B\times S\right)\to 1^{st}\left(p\right)\in B$$
79	77 78	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(p\right)\in B$$
80	1 5 58 70	erlcl2	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to q\in \left(B\times S\right)$$
81	80	ad4antr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to q\in \left(B\times S\right)$$
82		xp1st	$$⊢q\in \left(B\times S\right)\to 1^{st}\left(q\right)\in B$$
83	81 82	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(q\right)\in B$$
84	1 2 64 79 83	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\in B$$
85	7	ad6antr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
86		xp2nd	$$⊢u\in \left(B\times S\right)\to 2^{nd}\left(u\right)\in S$$
87	67 86	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(u\right)\in S$$
88		xp2nd	$$⊢v\in \left(B\times S\right)\to 2^{nd}\left(v\right)\in S$$
89	72 88	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(v\right)\in S$$
90	29 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
91	90	submcl	$$⊢\left(S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\wedge 2^{nd}\left(u\right)\in S\wedge 2^{nd}\left(v\right)\in S\right)\to 2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\in S$$
92	85 87 89 91	syl3anc	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\in S$$
93		xp2nd	$$⊢p\in \left(B\times S\right)\to 2^{nd}\left(p\right)\in S$$
94	77 93	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(p\right)\in S$$
95		xp2nd	$$⊢q\in \left(B\times S\right)\to 2^{nd}\left(q\right)\in S$$
96	81 95	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(q\right)\in S$$
97	90	submcl	$$⊢\left(S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\wedge 2^{nd}\left(p\right)\in S\wedge 2^{nd}\left(q\right)\in S\right)\to 2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\in S$$
98	85 94 96 97	syl3anc	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\in S$$
99		simp-4r	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\in S$$
100		simplr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to g\in S$$
101	90	submcl	$$⊢\left(S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\wedge f\in S\wedge g\in S\right)\to f\underset{\dot{}}{·}g\in S$$
102	85 99 100 101	syl3anc	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\underset{\dot{}}{·}g\in S$$
103	60 102	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\underset{\dot{}}{·}g\in B$$
104	60 98	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\in B$$
105	1 2 64 75 104	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\in B$$
106	60 92	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\in B$$
107	1 2 64 84 106	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\in B$$
108	1 2 16 64 103 105 107	ringsubdi	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right){-}_R\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)$$
109	64	ringgrpd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to R\in \mathrm{Grp}$$
110	1 2 64 103 105	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\in B$$
111	1 2 64 79 74	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\in B$$
112	60 87	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(u\right)\in B$$
113	60 96	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(q\right)\in B$$
114	1 2 64 112 113	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\in B$$
115	1 2 64 111 114	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\in B$$
116	1 2 64 103 115	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\in B$$
117	1 2 64 103 107	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\in B$$
118	1 3 16	grpnpncan	$$⊢\left(R\in \mathrm{Grp}\wedge \left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\in B\wedge \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\in B\wedge \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\in B\right)\right)\to \left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)\right)=\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)$$
119	109 110 116 117 118	syl13anc	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)\right)=\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)$$
120	6	ad2antrr	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to R\in \mathrm{CRing}$$
121	120	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\to R\in \mathrm{CRing}$$
122	121	ad2antrr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to R\in \mathrm{CRing}$$
123	29	crngmgp	$$⊢R\in \mathrm{CRing}\to {\mathrm{mulGrp}}_R\in \mathrm{CMnd}$$
124	122 123	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to {\mathrm{mulGrp}}_R\in \mathrm{CMnd}$$
125	60 99	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\in B$$
126	60 100	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to g\in B$$
127	60 94	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(p\right)\in B$$
128	30 90 124 125 126 69 74 127 113	cmn246135	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)=\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right)$$
129	30 90 124 125 126 79 74 112 113	cmn246135	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)=\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)$$
130	128 129	oveq12d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right)=\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right)\right){-}_R\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\right)$$
131	1 2 64 74 113	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\in B$$
132	1 2 64 126 131	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\in B$$
133	1 2 64 69 127	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\in B$$
134	1 2 64 125 133	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\in B$$
135	1 2 64 79 112	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\in B$$
136	1 2 64 125 135	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\in B$$
137	1 2 16 64 132 134 136	ringsubdi	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right){-}_R\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\right)=\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right)\right){-}_R\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\right)$$
138	1 2 16 64 125 133 135	ringsubdi	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right){-}_R\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)$$
139		simpllr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R$$
140	138 139	eqtr3d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right){-}_R\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R$$
141	140	oveq2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right){-}_R\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\right)=\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}{0}_R$$
142	1 2 15 64 132	ringrzd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}{0}_R=0_R$$
143	141 142	eqtrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right){-}_R\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\right)=0_R$$
144	137 143	eqtr3d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right)\right)\right){-}_R\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\underset{\dot{}}{·}\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\right)=0_R$$
145	130 144	eqtrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right)=0_R$$
146	1 2 122 79 74	crngcomd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)=1^{st}\left(v\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)$$
147	146	oveq1d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)=\left(1^{st}\left(v\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)$$
148	147	oveq2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)=\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)$$
149	30 90 124 125 126 74 79 112 113	cmn145236	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)=\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)$$
150	148 149	eqtrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)=\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)$$
151	1 2 122 83 79	crngcomd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(q\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)=1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)$$
152	151	oveq1d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(1^{st}\left(q\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)=\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)$$
153	152	oveq2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(q\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)$$
154	60 89	sseldd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 2^{nd}\left(v\right)\in B$$
155	30 90 124 125 126 83 79 112 154	cmn145236	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(q\right)\underset{\dot{}}{·}{1}^{st}\left(p\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)$$
156	153 155	eqtr3d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)$$
157	150 156	oveq12d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)$$
158	1 2 64 83 154	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\in B$$
159	1 2 16 64 126 131 158	ringsubdi	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right){-}_R\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)$$
160		simpr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R$$
161	159 160	eqtr3d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right){-}_R\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R$$
162	161	oveq2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right){-}_R\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}{0}_R$$
163	1 2 64 126 158	ringcld	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\in B$$
164	1 2 16 64 136 132 163	ringsubdi	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right){-}_R\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)$$
165	1 2 15 64 136	ringrzd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}{0}_R=0_R$$
166	162 164 165	3eqtr3d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)\underset{\dot{}}{·}\left(g\underset{\dot{}}{·}\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=0_R$$
167	157 166	eqtrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=0_R$$
168	145 167	oveq12d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)\right)=0_R\underset{\dot{}}{+}{0}_R$$
169	1 15	grpidcl	$$⊢R\in \mathrm{Grp}\to 0_R\in B$$
170	109 169	syl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 0_R\in B$$
171	1 3 15 109 170	grplidd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to 0_R\underset{\dot{}}{+}{0}_R=0_R$$
172	168 171	eqtrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right)\right){-}_R\left(\left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)\right)=0_R$$
173	108 119 172	3eqtr2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to \left(f\underset{\dot{}}{·}g\right)\underset{\dot{}}{·}\left(\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right)\right){-}_R\left(\left(1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\right)\underset{\dot{}}{·}\left(2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)\right)=0_R$$
174	1 5 60 15 2 16 61 62 75 84 92 98 102 173	erlbrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\wedge g\in S\right)\wedge g\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R\right)\to ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\underset{\dot{}}{\sim }⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
175	70	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\to v\underset{\dot{}}{\sim }q$$
176	1 5 59 15 2 16 175	erldi	$$⊢\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\to \exists g\in Sg\underset{\dot{}}{·}\left(\left(1^{st}\left(v\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\right){-}_R\left(1^{st}\left(q\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)\right)\right)=0_R$$
177	174 176	r19.29a	$$⊢\left(\left(\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\wedge f\in S\right)\wedge f\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R\right)\to ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\underset{\dot{}}{\sim }⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
178	1 5 58 15 2 16 65	erldi	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to \exists f\in Sf\underset{\dot{}}{·}\left(\left(1^{st}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(p\right)\right){-}_R\left(1^{st}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(u\right)\right)\right)=0_R$$
179	177 178	r19.29a	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\underset{\dot{}}{\sim }⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
180		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
181		snsstp3	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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\}$$
182	181 42	sstri	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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\}$$
183	25	mpoexg	$$⊢\left(B\times S\in \mathrm{V}\wedge B\times S\in \mathrm{V}\right)\to \left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)\in \mathrm{V}$$
184	46 46 183	syl2anc	$$⊢\phi \to \left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)\in \mathrm{V}$$
185		eqid	$$⊢{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}={\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}$$
186	35 37 180 182 184 185	strfv3	$$⊢\phi \to {\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}=\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)$$
187	186	ad2antrr	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to {\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}=\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)$$
188	187	oveqd	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to u{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}v=u\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)v$$
189		opex	$$⊢⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\in \mathrm{V}$$
190	189	a1i	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\in \mathrm{V}$$
191		simpl	$$⊢\left(a=u\wedge b=v\right)\to a=u$$
192	191	fveq2d	$$⊢\left(a=u\wedge b=v\right)\to 1^{st}\left(a\right)=1^{st}\left(u\right)$$
193		simpr	$$⊢\left(a=u\wedge b=v\right)\to b=v$$
194	193	fveq2d	$$⊢\left(a=u\wedge b=v\right)\to 1^{st}\left(b\right)=1^{st}\left(v\right)$$
195	192 194	oveq12d	$$⊢\left(a=u\wedge b=v\right)\to 1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right)=1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right)$$
196	191	fveq2d	$$⊢\left(a=u\wedge b=v\right)\to 2^{nd}\left(a\right)=2^{nd}\left(u\right)$$
197	193	fveq2d	$$⊢\left(a=u\wedge b=v\right)\to 2^{nd}\left(b\right)=2^{nd}\left(v\right)$$
198	196 197	oveq12d	$$⊢\left(a=u\wedge b=v\right)\to 2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)=2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)$$
199	195 198	opeq12d	$$⊢\left(a=u\wedge b=v\right)\to ⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩=⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩$$
200	199 25	ovmpoga	$$⊢\left(u\in \left(B\times S\right)\wedge v\in \left(B\times S\right)\wedge ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\in \mathrm{V}\right)\to u\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)v=⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩$$
201	66 71 190 200	syl3anc	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to u\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)v=⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩$$
202	188 201	eqtrd	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to u{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}v=⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩$$
203	187	oveqd	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q=p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q$$
204		opex	$$⊢⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩\in \mathrm{V}$$
205	204	a1i	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to ⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩\in \mathrm{V}$$
206		simpl	$$⊢\left(a=p\wedge b=q\right)\to a=p$$
207	206	fveq2d	$$⊢\left(a=p\wedge b=q\right)\to 1^{st}\left(a\right)=1^{st}\left(p\right)$$
208		simpr	$$⊢\left(a=p\wedge b=q\right)\to b=q$$
209	208	fveq2d	$$⊢\left(a=p\wedge b=q\right)\to 1^{st}\left(b\right)=1^{st}\left(q\right)$$
210	207 209	oveq12d	$$⊢\left(a=p\wedge b=q\right)\to 1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right)=1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)$$
211	206	fveq2d	$$⊢\left(a=p\wedge b=q\right)\to 2^{nd}\left(a\right)=2^{nd}\left(p\right)$$
212	208	fveq2d	$$⊢\left(a=p\wedge b=q\right)\to 2^{nd}\left(b\right)=2^{nd}\left(q\right)$$
213	211 212	oveq12d	$$⊢\left(a=p\wedge b=q\right)\to 2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)=2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)$$
214	210 213	opeq12d	$$⊢\left(a=p\wedge b=q\right)\to ⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩=⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
215	214 25	ovmpoga	$$⊢\left(p\in \left(B\times S\right)\wedge q\in \left(B\times S\right)\wedge ⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩\in \mathrm{V}\right)\to p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q=⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
216	76 80 205 215	syl3anc	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q=⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
217	203 216	eqtrd	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q=⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
218	202 217	breq12d	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to \left(\left(u{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}v\right)\underset{\dot{}}{\sim }\left(p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q\right)\leftrightarrow ⟨1^{st}\left(u\right)\underset{\dot{}}{·}{1}^{st}\left(v\right),2^{nd}\left(u\right)\underset{\dot{}}{·}{2}^{nd}\left(v\right)⟩\underset{\dot{}}{\sim }⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩\right)$$
219	179 218	mpbird	$$⊢\left(\left(\phi \wedge u\underset{\dot{}}{\sim }p\right)\wedge v\underset{\dot{}}{\sim }q\right)\to \left(u{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}v\right)\underset{\dot{}}{\sim }\left(p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q\right)$$
220	219	anasss	$$⊢\left(\phi \wedge \left(u\underset{\dot{}}{\sim }p\wedge v\underset{\dot{}}{\sim }q\right)\right)\to \left(u{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}v\right)\underset{\dot{}}{\sim }\left(p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q\right)$$
221	220	ex	$$⊢\phi \to \left(\left(u\underset{\dot{}}{\sim }p\wedge v\underset{\dot{}}{\sim }q\right)\to \left(u{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}v\right)\underset{\dot{}}{\sim }\left(p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q\right)\right)$$
222	186	oveqd	$$⊢\phi \to p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q=p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q$$
223	222	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q=p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q$$
224		simplr	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to p\in \left(B\times S\right)$$
225		simpr	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to q\in \left(B\times S\right)$$
226	204	a1i	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to ⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩\in \mathrm{V}$$
227	224 225 226 215	syl3anc	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q=⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩$$
228	63	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to R\in \mathrm{Ring}$$
229	224 78	syl	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to 1^{st}\left(p\right)\in B$$
230	225 82	syl	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to 1^{st}\left(q\right)\in B$$
231	1 2 228 229 230	ringcld	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to 1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right)\in B$$
232	7	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
233	224 93	syl	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to 2^{nd}\left(p\right)\in S$$
234	225 95	syl	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to 2^{nd}\left(q\right)\in S$$
235	232 233 234 97	syl3anc	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to 2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)\in S$$
236	231 235	opelxpd	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to ⟨1^{st}\left(p\right)\underset{\dot{}}{·}{1}^{st}\left(q\right),2^{nd}\left(p\right)\underset{\dot{}}{·}{2}^{nd}\left(q\right)⟩\in \left(B\times S\right)$$
237	227 236	eqeltrd	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to p\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)q\in \left(B\times S\right)$$
238	223 237	eqeltrd	$$⊢\left(\left(\phi \wedge p\in \left(B\times S\right)\right)\wedge q\in \left(B\times S\right)\right)\to p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q\in \left(B\times S\right)$$
239	238	anasss	$$⊢\left(\phi \wedge \left(p\in \left(B\times S\right)\wedge q\in \left(B\times S\right)\right)\right)\to p{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}q\in \left(B\times S\right)$$
240	34 49 51 57 221 239 185 12	qusmulval	$$⊢\left(\phi \wedge ⟨E,G⟩\in \left(B\times S\right)\wedge ⟨F,H⟩\in \left(B\times S\right)\right)\to \left[⟨E,G⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{\otimes }\left[⟨F,H⟩\right]\underset{\dot{}}{\sim }=\left[\left(⟨E,G⟩{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}⟨F,H⟩\right)\right]\underset{\dot{}}{\sim }$$
241	13 14 240	mpd3an23	$$⊢\phi \to \left[⟨E,G⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{\otimes }\left[⟨F,H⟩\right]\underset{\dot{}}{\sim }=\left[\left(⟨E,G⟩{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}⟨F,H⟩\right)\right]\underset{\dot{}}{\sim }$$
242	186	oveqd	$$⊢\phi \to ⟨E,G⟩{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}⟨F,H⟩=⟨E,G⟩\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)⟨F,H⟩$$
243	25	a1i	$$⊢\phi \to \left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)$$
244		simprl	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to a=⟨E,G⟩$$
245	244	fveq2d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(a\right)=1^{st}\left(⟨E,G⟩\right)$$
246	8	adantr	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to E\in B$$
247	10	adantr	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to G\in S$$
248		op1stg	$$⊢\left(E\in B\wedge G\in S\right)\to 1^{st}\left(⟨E,G⟩\right)=E$$
249	246 247 248	syl2anc	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(⟨E,G⟩\right)=E$$
250	245 249	eqtrd	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(a\right)=E$$
251		simprr	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to b=⟨F,H⟩$$
252	251	fveq2d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(b\right)=1^{st}\left(⟨F,H⟩\right)$$
253	9	adantr	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to F\in B$$
254	11	adantr	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to H\in S$$
255		op1stg	$$⊢\left(F\in B\wedge H\in S\right)\to 1^{st}\left(⟨F,H⟩\right)=F$$
256	253 254 255	syl2anc	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(⟨F,H⟩\right)=F$$
257	252 256	eqtrd	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(b\right)=F$$
258	250 257	oveq12d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right)=E\underset{\dot{}}{·}F$$
259	244	fveq2d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(a\right)=2^{nd}\left(⟨E,G⟩\right)$$
260		op2ndg	$$⊢\left(E\in B\wedge G\in S\right)\to 2^{nd}\left(⟨E,G⟩\right)=G$$
261	246 247 260	syl2anc	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(⟨E,G⟩\right)=G$$
262	259 261	eqtrd	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(a\right)=G$$
263	251	fveq2d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(b\right)=2^{nd}\left(⟨F,H⟩\right)$$
264		op2ndg	$$⊢\left(F\in B\wedge H\in S\right)\to 2^{nd}\left(⟨F,H⟩\right)=H$$
265	253 254 264	syl2anc	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(⟨F,H⟩\right)=H$$
266	263 265	eqtrd	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(b\right)=H$$
267	262 266	oveq12d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to 2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)=G\underset{\dot{}}{·}H$$
268	258 267	opeq12d	$$⊢\left(\phi \wedge \left(a=⟨E,G⟩\wedge b=⟨F,H⟩\right)\right)\to ⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩=⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩$$
269		opex	$$⊢⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩\in \mathrm{V}$$
270	269	a1i	$$⊢\phi \to ⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩\in \mathrm{V}$$
271	243 268 13 14 270	ovmpod	$$⊢\phi \to ⟨E,G⟩\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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)⟨F,H⟩=⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩$$
272	242 271	eqtrd	$$⊢\phi \to ⟨E,G⟩{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}⟨F,H⟩=⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩$$
273	272	eceq1d	$$⊢\phi \to \left[\left(⟨E,G⟩{\cdot }_{\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B\times S⟩,⟨{+}_{\mathrm{ndx}},\left(a\in \left(B\times S\right),b\in \left(B\times S\right)⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{+}\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 \left(B\times S\right),b\in \left(B\times S\right)⟼⟨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 \left(B\times S\right)⟼⟨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 \left(B\times S\right)\wedge b\in \left(B\times S\right)\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 \left(B\times S\right),b\in \left(B\times S\right)⟼\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)}⟨F,H⟩\right)\right]\underset{\dot{}}{\sim }=\left[⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩\right]\underset{\dot{}}{\sim }$$
274	241 273	eqtrd	$$⊢\phi \to \left[⟨E,G⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{\otimes }\left[⟨F,H⟩\right]\underset{\dot{}}{\sim }=\left[⟨E\underset{\dot{}}{·}F,G\underset{\dot{}}{·}H⟩\right]\underset{\dot{}}{\sim }$$