Theorem rlocval

Description: Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocval.1	$$⊢B={\mathrm{Base}}_R$$
	rlocval.2	$$⊢\underset{\dot{}}{0}=0_R$$
	rlocval.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rlocval.4	$$⊢\underset{\dot{}}{-}={-}_R$$
	rlocval.5	$$⊢\underset{\dot{}}{+}={+}_R$$
	rlocval.6	$$⊢\underset{\dot{}}{\le }={\le }_R$$
	rlocval.7	$$⊢F=\mathrm{Scalar}\left(R\right)$$
	rlocval.8	$$⊢K={\mathrm{Base}}_F$$
	rlocval.9	$$⊢C={\cdot }_R$$
	rlocval.10	$$⊢W=B\times S$$
	rlocval.11	No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
	rlocval.12	$$⊢J=\mathrm{TopSet}\left(R\right)$$
	rlocval.13	$$⊢D=\mathrm{dist}\left(R\right)$$
	rlocval.14	$$⊢\underset{\dot{}}{\oplus }=\left(a\in W,b\in W⟼⟨\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)$$
	rlocval.15	$$⊢\underset{\dot{}}{\otimes }=\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)$$
	rlocval.16	$$⊢\underset{\dot{}}{\times }=\left(k\in K,a\in W⟼⟨kC{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)$$
	rlocval.17	No typesetting found for |- .c_ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } with typecode |-
	rlocval.18	$$⊢E=\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)D\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)$$
	rlocval.19	$$⊢\phi \to R\in V$$
	rlocval.20	$$⊢\phi \to S\subseteq B$$
Assertion	rlocval	Could not format assertion : No typesetting found for |- ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rlocval.1	$$⊢B={\mathrm{Base}}_R$$
2		rlocval.2	$$⊢\underset{\dot{}}{0}=0_R$$
3		rlocval.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		rlocval.4	$$⊢\underset{\dot{}}{-}={-}_R$$
5		rlocval.5	$$⊢\underset{\dot{}}{+}={+}_R$$
6		rlocval.6	$$⊢\underset{\dot{}}{\le }={\le }_R$$
7		rlocval.7	$$⊢F=\mathrm{Scalar}\left(R\right)$$
8		rlocval.8	$$⊢K={\mathrm{Base}}_F$$
9		rlocval.9	$$⊢C={\cdot }_R$$
10		rlocval.10	$$⊢W=B\times S$$
11		rlocval.11	Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
12		rlocval.12	$$⊢J=\mathrm{TopSet}\left(R\right)$$
13		rlocval.13	$$⊢D=\mathrm{dist}\left(R\right)$$
14		rlocval.14	$$⊢\underset{\dot{}}{\oplus }=\left(a\in W,b\in W⟼⟨\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)$$
15		rlocval.15	$$⊢\underset{\dot{}}{\otimes }=\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)$$
16		rlocval.16	$$⊢\underset{\dot{}}{\times }=\left(k\in K,a\in W⟼⟨kC{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)$$
17		rlocval.17	Could not format .c_ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } : No typesetting found for |- .c_ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) .<_ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } with typecode |-
18		rlocval.18	$$⊢E=\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)D\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)$$
19		rlocval.19	$$⊢\phi \to R\in V$$
20		rlocval.20	$$⊢\phi \to S\subseteq B$$
21	19	elexd	$$⊢\phi \to R\in \mathrm{V}$$
22	1	fvexi	$$⊢B\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to B\in \mathrm{V}$$
24	23 20	ssexd	$$⊢\phi \to S\in \mathrm{V}$$
25		ovexd	Could not format ( ph -> ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) e. _V ) : No typesetting found for |- ( ph -> ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) e. _V ) with typecode |-
26		fvexd	$$⊢\left(r=R\wedge s=S\right)\to {\cdot }_r\in \mathrm{V}$$
27		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
28	27	adantr	$$⊢\left(r=R\wedge s=S\right)\to {\cdot }_r={\cdot }_R$$
29	28 3	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to {\cdot }_r=\underset{\dot{}}{·}$$
30		fvexd	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to {\mathrm{Base}}_r\in \mathrm{V}$$
31		vex	$$⊢s\in \mathrm{V}$$
32	31	a1i	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to s\in \mathrm{V}$$
33	30 32	xpexd	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to {\mathrm{Base}}_r\times s\in \mathrm{V}$$
34		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
35	34	ad2antrr	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
36	35 1	eqtr4di	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to {\mathrm{Base}}_r=B$$
37		simplr	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to s=S$$
38	36 37	xpeq12d	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to {\mathrm{Base}}_r\times s=B\times S$$
39	38 10	eqtr4di	$$⊢\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\to {\mathrm{Base}}_r\times s=W$$
40		simpr	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to w=W$$
41	40	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩$$
42		simplll	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to r=R$$
43	42	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {+}_r={+}_R$$
44	43 5	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {+}_r=\underset{\dot{}}{+}$$
45		simplr	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to x=\underset{\dot{}}{·}$$
46	45	oveqd	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to 1^{st}\left(a\right)x{2}^{nd}\left(b\right)=1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)$$
47	45	oveqd	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to 1^{st}\left(b\right)x{2}^{nd}\left(a\right)=1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)$$
48	44 46 47	oveq123d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\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)$$
49	45	oveqd	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to 2^{nd}\left(a\right)x{2}^{nd}\left(b\right)=2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)$$
50	48 49	opeq12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\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)⟩$$
51	40 40 50	mpoeq123dv	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)=\left(a\in W,b\in W⟼⟨\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\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)$$
52	51 14	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)=\underset{\dot{}}{\oplus }$$
53	52	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩$$
54	45	oveqd	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to 1^{st}\left(a\right)x{1}^{st}\left(b\right)=1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right)$$
55	54 49	opeq12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\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)⟩$$
56	40 40 55	mpoeq123dv	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)=\left(a\in W,b\in W⟼⟨1^{st}\left(a\right)\underset{\dot{}}{·}{1}^{st}\left(b\right),2^{nd}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)⟩\right)$$
57	56 15	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)=\underset{\dot{}}{\otimes }$$
58	57	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\otimes }⟩$$
59	41 53 58	tpeq123d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩,⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\otimes }⟩\right\}$$
60	42	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{Scalar}\left(r\right)=\mathrm{Scalar}\left(R\right)$$
61	60 7	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{Scalar}\left(r\right)=F$$
62	61	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩=⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩$$
63	60	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
64	7	fveq2i	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
65	8 64	eqtri	$$⊢K={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
66	63 65	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)}=K$$
67	42	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {\cdot }_r={\cdot }_R$$
68	67 9	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {\cdot }_r=C$$
69	68	oveqd	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to k{\cdot }_r{1}^{st}\left(a\right)=kC{1}^{st}\left(a\right)$$
70	69	opeq1d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩=⟨kC{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩$$
71	66 40 70	mpoeq123dv	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)=\left(k\in K,a\in W⟼⟨kC{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)$$
72	71 16	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)=\underset{\dot{}}{\times }$$
73	72	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩$$
74		eqidd	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩=⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩$$
75	62 73 74	tpeq123d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}=\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}$$
76	59 75	uneq12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩,⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},W⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{\oplus }⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\otimes }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}$$
77	42	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{TopSet}\left(r\right)=\mathrm{TopSet}\left(R\right)$$
78	77 12	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{TopSet}\left(r\right)=J$$
79	37	adantr	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to s=S$$
80	78 79	oveq12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s=J{\upharpoonright }_{𝑡}S$$
81	78 80	oveq12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)=J{\times }_t\left(J{\upharpoonright }_{𝑡}S\right)$$
82	81	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)⟩=⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J{\times }_t\left(J{\upharpoonright }_{𝑡}S\right)⟩$$
83	40	eleq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w\leftrightarrow a\in W\right)$$
84	40	eleq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(b\in w\leftrightarrow b\in W\right)$$
85	83 84	anbi12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(\left(a\in w\wedge b\in w\right)\leftrightarrow \left(a\in W\wedge b\in W\right)\right)$$
86	42	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {\le }_r={\le }_R$$
87	86 6	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to {\le }_r=\underset{\dot{}}{\le }$$
88	46 87 47	breq123d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\leftrightarrow \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{\le }\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)$$
89	85 88	anbi12d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\leftrightarrow \left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{\le }\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right)$$
90	89	opabbidv	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\right\}=\left\{⟨a,b⟩|\left(\left(a\in W\wedge b\in W\right)\wedge \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{\le }\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)\right\}$$
91	90 17	eqtr4di	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } = .c_ ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } = .c_ ) with typecode |-
92	91	opeq2d	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. = <. ( le ` ndx ) , .c_ >. ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. = <. ( le ` ndx ) , .c_ >. ) with typecode |-
93	42	fveq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{dist}\left(r\right)=\mathrm{dist}\left(R\right)$$
94	93 13	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \mathrm{dist}\left(r\right)=D$$
95	94 46 47	oveq123d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)=\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)D\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)$$
96	40 40 95	mpoeq123dv	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)=\left(a\in W,b\in W⟼\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)D\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)$$
97	96 18	eqtr4di	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to \left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)=E$$
98	97	opeq2d	$$⊢\left(\left(\left(r=R\wedge s=S\right)\wedge x=\underset{\dot{}}{·}\right)\wedge w=W\right)\to ⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)⟩=⟨\mathrm{dist}\left(\mathrm{ndx}\right),E⟩$$
99	82 92 98	tpeq123d	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } = { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } = { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) with typecode |-
100	76 99	uneq12d	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) = ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) = ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) ) with typecode |-
101	42 79	oveq12d	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( r ~RL s ) = ( R ~RL S ) ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( r ~RL s ) = ( R ~RL S ) ) with typecode |-
102	101 11	eqtr4di	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( r ~RL s ) = .~ ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( r ~RL s ) = .~ ) with typecode |-
103	100 102	oveq12d	Could not format ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) : No typesetting found for |- ( ( ( ( r = R /\ s = S ) /\ x = .x. ) /\ w = W ) -> ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) with typecode |-
104	33 39 103	csbied2	Could not format ( ( ( r = R /\ s = S ) /\ x = .x. ) -> [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) : No typesetting found for |- ( ( ( r = R /\ s = S ) /\ x = .x. ) -> [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) with typecode |-
105	26 29 104	csbied2	Could not format ( ( r = R /\ s = S ) -> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) : No typesetting found for |- ( ( r = R /\ s = S ) -> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) with typecode |-
106		df-rloc	Could not format RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) : No typesetting found for |- RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) with typecode |-
107	105 106	ovmpoga	Could not format ( ( R e. _V /\ S e. _V /\ ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) e. _V ) -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) : No typesetting found for |- ( ( R e. _V /\ S e. _V /\ ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) e. _V ) -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) with typecode |-
108	21 24 25 107	syl3anc	Could not format ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) : No typesetting found for |- ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , W >. , <. ( +g ` ndx ) , .(+) >. , <. ( .r ` ndx ) , .(x) >. } u. { <. ( Scalar ` ndx ) , F >. , <. ( .s ` ndx ) , .X. >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( J tX ( J |`t S ) ) >. , <. ( le ` ndx ) , .c_ >. , <. ( dist ` ndx ) , E >. } ) /s .~ ) ) with typecode |-