Theorem rlocval 33263

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 3504	. 2 ⊢ (𝜑 → 𝑅 ∈ V)
3		rlocval.1	. . . . 5 ⊢ 𝐵 = (Base‘𝑅)
4	3	fvexi 6920	. . . 4 ⊢ 𝐵 ∈ V
5	4	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
6		rlocval.20	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
7	5, 6	ssexd 5324	. 2 ⊢ (𝜑 → 𝑆 ∈ V)
8		ovexd 7466	. 2 ⊢ (𝜑 → ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⊕ ⟩, ⟨(.r‘ndx), ⊗ ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩, ⟨(le‘ndx), ≲ ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ∼ ) ∈ V)
9		fvexd 6921	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) ∈ V)
10		fveq2 6906	. . . . . 6 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅))
11	10	adantr 480	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = (.r‘𝑅))
12		rlocval.3	. . . . 5 ⊢ · = (.r‘𝑅)
13	11, 12	eqtr4di 2795	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = · )
14		fvexd 6921	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) ∈ V)
15		vex 3484	. . . . . . 7 ⊢ 𝑠 ∈ V
16	15	a1i 11	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 ∈ V)
17	14, 16	xpexd 7771	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) ∈ V)
18		fveq2 6906	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
19	18	ad2antrr 726	. . . . . . . 8 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) = (Base‘𝑅))
20	19, 3	eqtr4di 2795	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) = 𝐵)
21		simplr 769	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 = 𝑆)
22	20, 21	xpeq12d 5716	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) = (𝐵 × 𝑆))
23		rlocval.10	. . . . . 6 ⊢ 𝑊 = (𝐵 × 𝑆)
24	22, 23	eqtr4di 2795	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) = 𝑊)
25		simpr 484	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊)
26	25	opeq2d 4880	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(Base‘ndx), 𝑤⟩ = ⟨(Base‘ndx), 𝑊⟩)
27		simplll 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑟 = 𝑅)
28	27	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g‘𝑟) = (+g‘𝑅))
29		rlocval.5	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘𝑅)
30	28, 29	eqtr4di 2795	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g‘𝑟) = + )
31		simplr 769	. . . . . . . . . . . . . . 15 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑥 = · )
32	31	oveqd 7448	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(2nd ‘𝑏)) = ((1st ‘𝑎) · (2nd ‘𝑏)))
33	31	oveqd 7448	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑏)𝑥(2nd ‘𝑎)) = ((1st ‘𝑏) · (2nd ‘𝑎)))
34	30, 32, 33	oveq123d 7452	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))))
35	31	oveqd 7448	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((2nd ‘𝑎)𝑥(2nd ‘𝑏)) = ((2nd ‘𝑎) · (2nd ‘𝑏)))
36	34, 35	opeq12d 4881	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩ = ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
37	25, 25, 36	mpoeq123dv 7508	. . . . . . . . . . 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 2795	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = ⊕ )
40	39	opeq2d 4880	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩ = ⟨(+g‘ndx), ⊕ ⟩)
41	31	oveqd 7448	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(1st ‘𝑏)) = ((1st ‘𝑎) · (1st ‘𝑏)))
42	41, 35	opeq12d 4881	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩ = ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
43	25, 25, 42	mpoeq123dv 7508	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩))
44		rlocval.15	. . . . . . . . . . 11 ⊢ ⊗ = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
45	43, 44	eqtr4di 2795	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩) = ⊗ )
46	45	opeq2d 4880	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩ = ⟨(.r‘ndx), ⊗ ⟩)
47	26, 40, 46	tpeq123d 4748	. . . . . . . 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 6910	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = (Scalar‘𝑅))
49		rlocval.7	. . . . . . . . . . 11 ⊢ 𝐹 = (Scalar‘𝑅)
50	48, 49	eqtr4di 2795	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = 𝐹)
51	50	opeq2d 4880	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐹⟩)
52	48	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = (Base‘(Scalar‘𝑅)))
53		rlocval.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝐹)
54	49	fveq2i 6909	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐹) = (Base‘(Scalar‘𝑅))
55	53, 54	eqtri 2765	. . . . . . . . . . . . 13 ⊢ 𝐾 = (Base‘(Scalar‘𝑅))
56	52, 55	eqtr4di 2795	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = 𝐾)
57	27	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑟) = ( ·𝑠 ‘𝑅))
58		rlocval.9	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ( ·𝑠 ‘𝑅)
59	57, 58	eqtr4di 2795	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑟) = 𝐶)
60	59	oveqd 7448	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)) = (𝑘𝐶(1st ‘𝑎)))
61	60	opeq1d 4879	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩ = ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩)
62	56, 25, 61	mpoeq123dv 7508	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩) = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩))
63		rlocval.16	. . . . . . . . . . 11 ⊢ × = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ ⟨(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)⟩)
64	62, 63	eqtr4di 2795	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩) = × )
65	64	opeq2d 4880	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩ = ⟨( ·𝑠 ‘ndx), × ⟩)
66		eqidd 2738	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(·𝑖‘ndx), ∅⟩ = ⟨(·𝑖‘ndx), ∅⟩)
67	51, 65, 66	tpeq123d 4748	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩} = {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩})
68	47, 67	uneq12d 4169	. . . . . . 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 6910	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = (TopSet‘𝑅))
70		rlocval.12	. . . . . . . . . . 11 ⊢ 𝐽 = (TopSet‘𝑅)
71	69, 70	eqtr4di 2795	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = 𝐽)
72	21	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑠 = 𝑆)
73	71, 72	oveq12d 7449	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ↾t 𝑠) = (𝐽 ↾t 𝑆))
74	71, 73	oveq12d 7449	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠)) = (𝐽 ×t (𝐽 ↾t 𝑆)))
75	74	opeq2d 4880	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩ = ⟨(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))⟩)
76	25	eleq2d 2827	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤 ↔ 𝑎 ∈ 𝑊))
77	25	eleq2d 2827	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑊))
78	76, 77	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ↔ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)))
79	27	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = (le‘𝑅))
80		rlocval.6	. . . . . . . . . . . . . 14 ⊢ ≤ = (le‘𝑅)
81	79, 80	eqtr4di 2795	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = ≤ )
82	32, 81, 33	breq123d 5157	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)) ↔ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎))))
83	78, 82	anbi12d 632	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) ↔ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))))
84	83	opabbidv 5209	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))})
85		rlocval.17	. . . . . . . . . 10 ⊢ ≲ = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd ‘𝑏)) ≤ ((1st ‘𝑏) · (2nd ‘𝑎)))}
86	84, 85	eqtr4di 2795	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))} = ≲ )
87	86	opeq2d 4880	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩ = ⟨(le‘ndx), ≲ ⟩)
88	27	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = (dist‘𝑅))
89		rlocval.13	. . . . . . . . . . . . 13 ⊢ 𝐷 = (dist‘𝑅)
90	88, 89	eqtr4di 2795	. . . . . . . . . . . 12 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = 𝐷)
91	90, 32, 33	oveq123d 7452	. . . . . . . . . . 11 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎))))
92	25, 25, 91	mpoeq123dv 7508	. . . . . . . . . 10 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎)))))
93		rlocval.18	. . . . . . . . . 10 ⊢ 𝐸 = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd ‘𝑏))𝐷((1st ‘𝑏) · (2nd ‘𝑎))))
94	92, 93	eqtr4di 2795	. . . . . . . . 9 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = 𝐸)
95	94	opeq2d 4880	. . . . . . . 8 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩ = ⟨(dist‘ndx), 𝐸⟩)
96	75, 87, 95	tpeq123d 4748	. . . . . . 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 4169	. . . . . 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 7449	. . . . . . 7 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = (𝑅 ~RL 𝑆))
99		rlocval.11	. . . . . . 7 ⊢ ∼ = (𝑅 ~RL 𝑆)
100	98, 99	eqtr4di 2795	. . . . . 6 ⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = ∼ )
101	97, 100	oveq12d 7449	. . . . 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 3936	. . . 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 3936	. . 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 33260	. . 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 7587	. 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 1373	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 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ⦋csb 3899   ∪ cun 3949   ⊆ wss 3951  ∅c0 4333  {ctp 4630  ⟨cop 4632   class class class wbr 5143  {copab 5205   × cxp 5683  ‘cfv 6561  (class class class)co 7431   ∈ cmpo 7433  1^st c1st 8012  2^nd c2nd 8013  ndxcnx 17230  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  ·_𝑖cip 17302  TopSetcts 17303  lecple 17304  distcds 17306   ↾_t crest 17465  0_gc0g 17484   /_s cqus 17550  -_gcsg 18953   ×_t ctx 23568   ~_RL cerl 33257   RLocal crloc 33258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-rloc 33260

This theorem is referenced by:  rlocbas  33271  rlocaddval  33272  rlocmulval  33273