Theorem rlocval 33347

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

Hypotheses

Ref	Expression
rlocval.1	⊢ 𝐵 = (Base‘𝑅)
rlocval.2	⊢ 0 = (0g‘𝑅)
rlocval.3	⊢ · = (.r‘𝑅)
rlocval.4	⊢ − = (-g‘𝑅)
rlocval.5	⊢ + = (+g‘𝑅)
rlocval.6	⊢ ≤ = (le‘𝑅)
rlocval.7	⊢ 𝐹 = (Scalar‘𝑅)
rlocval.8	⊢ 𝐾 = (Base‘𝐹)
rlocval.9	⊢ 𝐶 = ( ·𝑠 ‘𝑅)
rlocval.10	⊢ 𝑊 = (𝐵 × 𝑆)
rlocval.11	⊢ ∼ = (𝑅 ~RL 𝑆)
rlocval.12	⊢ 𝐽 = (TopSet‘𝑅)
rlocval.13	⊢ 𝐷 = (dist‘𝑅)
rlocval.14	⊢ ⊕ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
rlocval.15	⊢ ⊗ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
rlocval.16	⊢ × = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩)
rlocval.17	⊢ ≲ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))}
rlocval.18	⊢ 𝐸 = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎))))
rlocval.19	⊢ (𝜑 → 𝑅 ∈ 𝑉)
rlocval.20	⊢ (𝜑 → 𝑆 ⊆ 𝐵)

Assertion

Ref	Expression
rlocval	⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))

Distinct variable groups:   · ,𝑎,𝑏,𝑘   𝑅,𝑎,𝑏,𝑘   𝑆,𝑎,𝑏,𝑘   𝑊,𝑎,𝑏,𝑘

Allowed substitution hints:   𝜑(𝑘,𝑎,𝑏)   𝐵(𝑘,𝑎,𝑏)   𝐶(𝑘,𝑎,𝑏)   𝐷(𝑘,𝑎,𝑏)   + (𝑘,𝑎,𝑏)   ⊕ (𝑘,𝑎,𝑏)   ∼ (𝑘,𝑎,𝑏)   × (𝑘,𝑎,𝑏)   ⊗ (𝑘,𝑎,𝑏)   𝐸(𝑘,𝑎,𝑏)   𝐹(𝑘,𝑎,𝑏)   𝐽(𝑘,𝑎,𝑏)   𝐾(𝑘,𝑎,𝑏)   ≤ (𝑘,𝑎,𝑏)   − (𝑘,𝑎,𝑏)   𝑉(𝑘,𝑎,𝑏)   0 (𝑘,𝑎,𝑏)   ≲ (𝑘,𝑎,𝑏)

Proof of Theorem rlocval

Dummy variables 𝑟 𝑠 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rlocval.19	. . 3 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
2	1	elexd 3456	. 2 ⊢ (𝜑 → 𝑅 ∈ V)
3		rlocval.1	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
4	3	fvexi 6848	. . . 4 ⊢ 𝐵 ∈ V
5	4	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
6		rlocval.20	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
7	5, 6	ssexd 5259	. 2 ⊢ (𝜑 → 𝑆 ∈ V)
8		ovexd 7398	. 2 ⊢ (𝜑 → ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ) ∈ V)
9		fvexd 6849	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) ∈ V)
10		fveq2 6834	. . . . . 6 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅))
11	10	adantr 481	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = (.r‘𝑅))
12		rlocval.3	. . . . 5 ⊢ · = (.r‘𝑅)
13	11, 12	eqtr4di 2793	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = · )
14		fvexd 6849	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) ∈ V)
15		vex 3436	. . . . . . 7 ⊢ 𝑠 ∈ V
16	15	a1i 11	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 ∈ V)
17	14, 16	xpexd 7701	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) ∈ V)
18		fveq2 6834	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
19	18	ad2antrr 732	. . . . . . . 8 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) = (Base‘𝑅))
20	19, 3	eqtr4di 2793	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) = 𝐵)
21		simplr 774	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 = 𝑆)
22	20, 21	xpeq12d 5656	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) = (𝐵 × 𝑆))
23		rlocval.10	. . . . . 6 ⊢ 𝑊 = (𝐵 × 𝑆)
24	22, 23	eqtr4di 2793	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) = 𝑊)
25		simpr 485	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊)
26	25	opeq2d 4818	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(Base‘ndx), 𝑤⟩ = ⟨(Base‘ndx), 𝑊⟩)
27		simplll 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑟 = 𝑅)
28	27	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g‘𝑟) = (+g‘𝑅))
29		rlocval.5	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘𝑅)
30	28, 29	eqtr4di 2793	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g‘𝑟) = + )
31		simplr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑥 = · )
32	31	oveqd 7380	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(2nd ‘𝑏)) = ((1st ‘𝑎) · (2nd ‘𝑏)))
33	31	oveqd 7380	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑏)𝑥(2nd ‘𝑎)) = ((1st ‘𝑏) · (2nd ‘𝑎)))
34	30, 32, 33	oveq123d 7384	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))))
35	31	oveqd 7380	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((2nd ‘𝑎)𝑥(2nd ‘𝑏)) = ((2nd ‘𝑎) · (2nd ‘𝑏)))
36	34, 35	opeq12d 4819	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩ = ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
37	25, 25, 36	mpoeq123dv 7438	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩))
38		rlocval.14	. . . . . . . . . . 11 ⊢ ⊕ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
39	37, 38	eqtr4di 2793	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = ⊕ )
40	39	opeq2d 4818	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩ = ⟨(+g‘ndx), ⊕ ⟩)
41	31	oveqd 7380	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(1st ‘𝑏)) = ((1st ‘𝑎) · (1st ‘𝑏)))
42	41, 35	opeq12d 4819	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩ = ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
43	25, 25, 42	mpoeq123dv 7438	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩))
44		rlocval.15	. . . . . . . . . . 11 ⊢ ⊗ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
45	43, 44	eqtr4di 2793	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = ⊗ )
46	45	opeq2d 4818	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩ = ⟨(.r‘ndx), ⊗ ⟩)
47	26, 40, 46	tpeq123d 4687	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} = {⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩})
48	27	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = (Scalar‘𝑅))
49		rlocval.7	. . . . . . . . . . 11 ⊢ 𝐹 = (Scalar‘𝑅)
50	48, 49	eqtr4di 2793	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = 𝐹)
51	50	opeq2d 4818	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐹⟩)
52	48	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = (Base‘(Scalar‘𝑅)))
53		rlocval.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝐹)
54	49	fveq2i 6837	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐹) = (Base‘(Scalar‘𝑅))
55	53, 54	eqtri 2763	. . . . . . . . . . . . 13 ⊢ 𝐾 = (Base‘(Scalar‘𝑅))
56	52, 55	eqtr4di 2793	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = 𝐾)
57	27	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑟) = ( ·𝑠 ‘𝑅))
58		rlocval.9	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ( ·𝑠 ‘𝑅)
59	57, 58	eqtr4di 2793	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑟) = 𝐶)
60	59	oveqd 7380	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)) = (𝑘𝐶(1st ‘𝑎)))
61	60	opeq1d 4817	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩ = ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩)
62	56, 25, 61	mpoeq123dv 7438	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩) = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩))
63		rlocval.16	. . . . . . . . . . 11 ⊢ × = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩)
64	62, 63	eqtr4di 2793	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩) = × )
65	64	opeq2d 4818	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩ = ⟨( ·𝑠 ‘ndx), × ⟩)
66		eqidd 2741	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(·𝑖‘ndx), ∅⟩ = ⟨(·𝑖‘ndx), ∅⟩)
67	51, 65, 66	tpeq123d 4687	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩} = {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩})
68	47, 67	uneq12d 4106	. . . . . . 7 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) = ({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}))
69	27	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = (TopSet‘𝑅))
70		rlocval.12	. . . . . . . . . . 11 ⊢ 𝐽 = (TopSet‘𝑅)
71	69, 70	eqtr4di 2793	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = 𝐽)
72	21	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑠 = 𝑆)
73	71, 72	oveq12d 7381	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ↾t 𝑠) = (𝐽 ↾t 𝑆))
74	71, 73	oveq12d 7381	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠)) = (𝐽 ×t (𝐽 ↾t 𝑆)))
75	74	opeq2d 4818	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩ = ⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩)
76	25	eleq2d 2826	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤 ↔ 𝑎 ∈ 𝑊))
77	25	eleq2d 2826	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑊))
78	76, 77	anbi12d 638	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ↔ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)))
79	27	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = (le‘𝑅))
80		rlocval.6	. . . . . . . . . . . . . 14 ⊢ ≤ = (le‘𝑅)
81	79, 80	eqtr4di 2793	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = ≤ )
82	32, 81, 33	breq123d 5093	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)) ↔ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎))))
83	78, 82	anbi12d 638	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) ↔ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))))
84	83	opabbidv 5145	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))})
85		rlocval.17	. . . . . . . . . 10 ⊢ ≲ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))}
86	84, 85	eqtr4di 2793	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))} = ≲ )
87	86	opeq2d 4818	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩ = ⟨(le‘ndx), ≲ ⟩)
88	27	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = (dist‘𝑅))
89		rlocval.13	. . . . . . . . . . . . 13 ⊢ 𝐷 = (dist‘𝑅)
90	88, 89	eqtr4di 2793	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = 𝐷)
91	90, 32, 33	oveq123d 7384	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎))))
92	25, 25, 91	mpoeq123dv 7438	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎)))))
93		rlocval.18	. . . . . . . . . 10 ⊢ 𝐸 = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎))))
94	92, 93	eqtr4di 2793	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = 𝐸)
95	94	opeq2d 4818	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩ = ⟨(dist‘ndx), 𝐸⟩)
96	75, 87, 95	tpeq123d 4687	. . . . . . 7 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩} = {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩})
97	68, 96	uneq12d 4106	. . . . . 6 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) = (({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}))
98	27, 72	oveq12d 7381	. . . . . . 7 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = (𝑅 ~RL 𝑆))
99		rlocval.11	. . . . . . 7 ⊢ ∼ = (𝑅 ~RL 𝑆)
100	98, 99	eqtr4di 2793	. . . . . 6 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = ∼ )
101	97, 100	oveq12d 7381	. . . . 5 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))
102	17, 24, 101	csbied2 3875	. . . 4 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))
103	9, 13, 102	csbied2 3875	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))
104		df-rloc 33344	. . 3 ⊢ RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)))
105	103, 104	ovmpoga 7517	. 2 ⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V ∧ ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ) ∈ V) → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))
106	2, 7, 8, 105	syl3anc 1379	1 ⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ⦋csb 3838   ∪ cun 3888   ⊆ wss 3890  ∅c0 4268  {ctp 4566  ⟨cop 4568   class class class wbr 5079  {copab 5141   × cxp 5623  ‘cfv 6492  (class class class)co 7363   ∈ cmpo 7365  1^st c1st 7936  2^nd c2nd 7937  ndxcnx 17161  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  ·_𝑖cip 17223  TopSetcts 17224  lecple 17225  distcds 17227   ↾_t crest 17381  0_gc0g 17400   /_s cqus 17467  -_gcsg 18909   ×_t ctx 23550   ~_RL cerl 33341   RLocal crloc 33342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-rloc 33344

This theorem is referenced by:  rlocbas  33355  rlocaddval  33356  rlocmulval  33357