rlocval

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

	Ref	Expression
Hypotheses	rlocval.1	$⊢ B = {Base}_{R}$
	rlocval.2	$⊢ \underset{˙}{0} = 0_{R}$
	rlocval.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rlocval.4	$⊢ \underset{˙}{-} = -_{R}$
	rlocval.5	$⊢ \underset{˙}{+} = +_{R}$
	rlocval.6	$⊢ \underset{˙}{\leq} = \leq_{R}$
	rlocval.7	$⊢ F = Scalar (R)$
	rlocval.8	$⊢ K = {Base}_{F}$
	rlocval.9	$⊢ C = \cdot_{R}$
	rlocval.10	$⊢ W = B \times S$
	rlocval.11	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	rlocval.12	$⊢ J = TopSet (R)$
	rlocval.13	$⊢ D = dist (R)$
	rlocval.14	$⊢ \underset{˙}{\oplus} = (a \in W, b \in W ⟼ ⟨(1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{+} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩)$
	rlocval.15	$⊢ \underset{˙}{\otimes} = (a \in W, b \in W ⟼ ⟨1^{st} (a) \underset{˙}{\cdot} 1^{st} (b), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩)$
	rlocval.16	$⊢ \underset{˙}{\times} = (k \in K, a \in W ⟼ ⟨k C 1^{st} (a), 2^{nd} (a)⟩)$
	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 = (a \in W, b \in W ⟼ (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) D (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)))$
	rlocval.19	$⊢ φ \to R \in V$
	rlocval.20	$⊢ φ \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 = {Base}_{R}$
2		rlocval.2	$⊢ \underset{˙}{0} = 0_{R}$
3		rlocval.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		rlocval.4	$⊢ \underset{˙}{-} = -_{R}$
5		rlocval.5	$⊢ \underset{˙}{+} = +_{R}$
6		rlocval.6	$⊢ \underset{˙}{\leq} = \leq_{R}$
7		rlocval.7	$⊢ F = Scalar (R)$
8		rlocval.8	$⊢ K = {Base}_{F}$
9		rlocval.9	$⊢ C = \cdot_{R}$
10		rlocval.10	$⊢ W = B \times S$
11		rlocval.11	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
12		rlocval.12	$⊢ J = TopSet (R)$
13		rlocval.13	$⊢ D = dist (R)$
14		rlocval.14	$⊢ \underset{˙}{\oplus} = (a \in W, b \in W ⟼ ⟨(1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{+} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩)$
15		rlocval.15	$⊢ \underset{˙}{\otimes} = (a \in W, b \in W ⟼ ⟨1^{st} (a) \underset{˙}{\cdot} 1^{st} (b), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩)$
16		rlocval.16	$⊢ \underset{˙}{\times} = (k \in K, a \in W ⟼ ⟨k C 1^{st} (a), 2^{nd} (a)⟩)$
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 = (a \in W, b \in W ⟼ (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) D (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)))$
19		rlocval.19	$⊢ φ \to R \in V$
20		rlocval.20	$⊢ φ \to S \subseteq B$
21	19	elexd	$⊢ φ \to R \in V$
22	1	fvexi	$⊢ B \in V$
23	22	a1i	$⊢ φ \to B \in V$
24	23 20	ssexd	$⊢ φ \to S \in 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	$⊢ (r = R \land s = S) \to \cdot_{r} \in V$
27		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
28	27	adantr	$⊢ (r = R \land s = S) \to \cdot_{r} = \cdot_{R}$
29	28 3	eqtr4di	$⊢ (r = R \land s = S) \to \cdot_{r} = \underset{˙}{\cdot}$
30		fvexd	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \in V$
31		vex	$⊢ s \in V$
32	31	a1i	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to s \in V$
33	30 32	xpexd	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \times s \in V$
34		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
35	34	ad2antrr	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} = {Base}_{R}$
36	35 1	eqtr4di	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} = B$
37		simplr	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to s = S$
38	36 37	xpeq12d	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \times s = B \times S$
39	38 10	eqtr4di	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \times s = W$
40		simpr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to w = W$
41	40	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨{Base}_{ndx}, w⟩ = ⟨{Base}_{ndx}, W⟩$
42		simplll	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to r = R$
43	42	fveq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to +_{r} = +_{R}$
44	43 5	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to +_{r} = \underset{˙}{+}$
45		simplr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to x = \underset{˙}{\cdot}$
46	45	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 1^{st} (a) x 2^{nd} (b) = 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)$
47	45	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 1^{st} (b) x 2^{nd} (a) = 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)$
48	44 46 47	oveq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)) = (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{+} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))$
49	45	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 2^{nd} (a) x 2^{nd} (b) = 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)$
50	48 49	opeq12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩ = ⟨(1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{+} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩$
51	40 40 50	mpoeq123dv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩) = (a \in W, b \in W ⟼ ⟨(1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{+} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩)$
52	51 14	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩) = \underset{˙}{\oplus}$
53	52	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩ = ⟨+_{ndx}, \underset{˙}{\oplus}⟩$
54	45	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 1^{st} (a) x 1^{st} (b) = 1^{st} (a) \underset{˙}{\cdot} 1^{st} (b)$
55	54 49	opeq12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩ = ⟨1^{st} (a) \underset{˙}{\cdot} 1^{st} (b), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩$
56	40 40 55	mpoeq123dv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩) = (a \in W, b \in W ⟼ ⟨1^{st} (a) \underset{˙}{\cdot} 1^{st} (b), 2^{nd} (a) \underset{˙}{\cdot} 2^{nd} (b)⟩)$
57	56 15	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩) = \underset{˙}{\otimes}$
58	57	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩ = ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩$
59	41 53 58	tpeq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} = \{⟨{Base}_{ndx}, W⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩\}$
60	42	fveq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to Scalar (r) = Scalar (R)$
61	60 7	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to Scalar (r) = F$
62	61	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨Scalar (ndx), Scalar (r)⟩ = ⟨Scalar (ndx), F⟩$
63	60	fveq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to {Base}_{Scalar (r)} = {Base}_{Scalar (R)}$
64	7	fveq2i	$⊢ {Base}_{F} = {Base}_{Scalar (R)}$
65	8 64	eqtri	$⊢ K = {Base}_{Scalar (R)}$
66	63 65	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to {Base}_{Scalar (r)} = K$
67	42	fveq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \cdot_{r} = \cdot_{R}$
68	67 9	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \cdot_{r} = C$
69	68	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to k \cdot_{r} 1^{st} (a) = k C 1^{st} (a)$
70	69	opeq1d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩ = ⟨k C 1^{st} (a), 2^{nd} (a)⟩$
71	66 40 70	mpoeq123dv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩) = (k \in K, a \in W ⟼ ⟨k C 1^{st} (a), 2^{nd} (a)⟩)$
72	71 16	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩) = \underset{˙}{\times}$
73	72	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩ = ⟨\cdot_{ndx}, \underset{˙}{\times}⟩$
74		eqidd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨\cdot_{𝑖} (ndx), \emptyset⟩ = ⟨\cdot_{𝑖} (ndx), \emptyset⟩$
75	62 73 74	tpeq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\} = \{⟨Scalar (ndx), F⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}$
76	59 75	uneq12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\} = \{⟨{Base}_{ndx}, W⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩\} \cup \{⟨Scalar (ndx), F⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}$
77	42	fveq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to TopSet (r) = TopSet (R)$
78	77 12	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to TopSet (r) = J$
79	37	adantr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to s = S$
80	78 79	oveq12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to TopSet (r) ↾_{𝑡} s = J ↾_{𝑡} S$
81	78 80	oveq12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s) = J \times_{t} (J ↾_{𝑡} S)$
82	81	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩ = ⟨TopSet (ndx), J \times_{t} (J ↾_{𝑡} S)⟩$
83	40	eleq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w \leftrightarrow a \in W)$
84	40	eleq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (b \in w \leftrightarrow b \in W)$
85	83 84	anbi12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ((a \in w \land b \in w) \leftrightarrow (a \in W \land b \in W))$
86	42	fveq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \leq_{r} = \leq_{R}$
87	86 6	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \leq_{r} = \underset{˙}{\leq}$
88	46 87 47	breq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ((1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)) \leftrightarrow (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{\leq} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)))$
89	85 88	anbi12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a))) \leftrightarrow ((a \in W \land b \in W) \land (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{\leq} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))))$
90	89	opabbidv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\} = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{\leq} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)))\}$
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	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to dist (r) = dist (R)$
94	93 13	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to dist (r) = D$
95	94 46 47	oveq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)) = (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) D (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))$
96	40 40 95	mpoeq123dv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a))) = (a \in W, b \in W ⟼ (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) D (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)))$
97	96 18	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a))) = E$
98	97	opeq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩ = ⟨dist (ndx), 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	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to r ~_{RL} s = R ~_{RL} S$
102	101 11	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to r ~_{RL} s = \underset{˙}{\sim}$
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	$⊢ RLocal = (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s)))$
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 \|-

Metamath Proof Explorer

Theorem rlocval

Proof