df-rloc

Description: Define the operation giving the localization of a ring r by a given set s . The localized ring r RLocal s is the set of equivalence classes of pairs of elements in r over the relation r ~RL s with addition and multiplication defined naturally. (Contributed by Thierry Arnoux, 27-Apr-2025)

		Ref	Expression
	Assertion	df-rloc	⊢ RLocal = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crloc	⊢ RLocal
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		cmulr	⊢ ._r
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( ._r ‘ 𝑟 )
7		vx	⊢ 𝑥
8		cbs	⊢ Base
9	5 8	cfv	⊢ ( Base ‘ 𝑟 )
10	3	cv	⊢ 𝑠
11	9 10	cxp	⊢ ( ( Base ‘ 𝑟 ) × 𝑠 )
12		vw	⊢ 𝑤
13		cnx	⊢ ndx
14	13 8	cfv	⊢ ( Base ‘ ndx )
15	12	cv	⊢ 𝑤
16	14 15	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑤 ⟩
17		cplusg	⊢ +_g
18	13 17	cfv	⊢ ( +_g ‘ ndx )
19		va	⊢ 𝑎
20		vb	⊢ 𝑏
21		c1st	⊢ 1^st
22	19	cv	⊢ 𝑎
23	22 21	cfv	⊢ ( 1^st ‘ 𝑎 )
24	7	cv	⊢ 𝑥
25		c2nd	⊢ 2^nd
26	20	cv	⊢ 𝑏
27	26 25	cfv	⊢ ( 2^nd ‘ 𝑏 )
28	23 27 24	co	⊢ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) )
29	5 17	cfv	⊢ ( +_g ‘ 𝑟 )
30	26 21	cfv	⊢ ( 1^st ‘ 𝑏 )
31	22 25	cfv	⊢ ( 2^nd ‘ 𝑎 )
32	30 31 24	co	⊢ ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) )
33	28 32 29	co	⊢ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) )
34	31 27 24	co	⊢ ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) )
35	33 34	cop	⊢ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩
36	19 20 15 15 35	cmpo	⊢ ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ )
37	18 36	cop	⊢ ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩
38	13 4	cfv	⊢ ( ._r ‘ ndx )
39	23 30 24	co	⊢ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) )
40	39 34	cop	⊢ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩
41	19 20 15 15 40	cmpo	⊢ ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ )
42	38 41	cop	⊢ ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩
43	16 37 42	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ }
44		csca	⊢ Scalar
45	13 44	cfv	⊢ ( Scalar ‘ ndx )
46	5 44	cfv	⊢ ( Scalar ‘ 𝑟 )
47	45 46	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩
48		cvsca	⊢ ·_𝑠
49	13 48	cfv	⊢ ( ·_𝑠 ‘ ndx )
50		vk	⊢ 𝑘
51	46 8	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑟 ) )
52	50	cv	⊢ 𝑘
53	5 48	cfv	⊢ ( ·_𝑠 ‘ 𝑟 )
54	52 23 53	co	⊢ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) )
55	54 31	cop	⊢ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩
56	50 19 51 15 55	cmpo	⊢ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ )
57	49 56	cop	⊢ ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩
58		cip	⊢ ·_𝑖
59	13 58	cfv	⊢ ( ·_𝑖 ‘ ndx )
60		c0	⊢ ∅
61	59 60	cop	⊢ ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩
62	47 57 61	ctp	⊢ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ }
63	43 62	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } )
64		cts	⊢ TopSet
65	13 64	cfv	⊢ ( TopSet ‘ ndx )
66	5 64	cfv	⊢ ( TopSet ‘ 𝑟 )
67		ctx	⊢ ×_t
68		crest	⊢ ↾_t
69	66 10 68	co	⊢ ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 )
70	66 69 67	co	⊢ ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) )
71	65 70	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩
72		cple	⊢ le
73	13 72	cfv	⊢ ( le ‘ ndx )
74	22 15	wcel	⊢ 𝑎 ∈ 𝑤
75	26 15	wcel	⊢ 𝑏 ∈ 𝑤
76	74 75	wa	⊢ ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 )
77	5 72	cfv	⊢ ( le ‘ 𝑟 )
78	28 32 77	wbr	⊢ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) )
79	76 78	wa	⊢ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) )
80	79 19 20	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) }
81	73 80	cop	⊢ ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩
82		cds	⊢ dist
83	13 82	cfv	⊢ ( dist ‘ ndx )
84	5 82	cfv	⊢ ( dist ‘ 𝑟 )
85	28 32 84	co	⊢ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) )
86	19 20 15 15 85	cmpo	⊢ ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) )
87	83 86	cop	⊢ ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩
88	71 81 87	ctp	⊢ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ }
89	63 88	cun	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } )
90		cqus	⊢ /_s
91		cerl	⊢ ~_RL
92	5 10 91	co	⊢ ( 𝑟 ~_RL 𝑠 )
93	89 92 90	co	⊢ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) )
94	12 11 93	csb	⊢ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) )
95	7 6 94	csb	⊢ ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) )
96	1 3 2 2 95	cmpo	⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) )
97	0 96	wceq	⊢ RLocal = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) )

Metamath Proof Explorer

Definition df-rloc

Detailed syntax breakdown