Definition df-erl

Description: Define the operation giving the equivalence relation used in the localization of a ring r by a set s . Two pairs a = <. x , y >. and b = <. z , w >. are equivalent if there exists t e. s such that t x. ( x x. w - z x. y ) = 0 . This corresponds to the usual comparison of fractions x / y and z / w . (Contributed by Thierry Arnoux, 28-Apr-2025)

	Ref	Expression
Assertion	df-erl	Could not format assertion : No typesetting found for |- ~RL = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cerl	Could not format ~RL : No typesetting found for class ~RL with typecode class
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cmulr	$$class{\cdot }_{𝑟}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\cdot }_r$$
7		vx	$$setvarx$$
8		cbs	$$class\mathrm{Base}$$
9	5 8	cfv	$$class{\mathrm{Base}}_r$$
10	3	cv	$$setvars$$
11	9 10	cxp	$$class\left({\mathrm{Base}}_r\times s\right)$$
12		vw	$$setvarw$$
13		va	$$setvara$$
14		vb	$$setvarb$$
15	13	cv	$$setvara$$
16	12	cv	$$setvarw$$
17	15 16	wcel	$$wffa\in w$$
18	14	cv	$$setvarb$$
19	18 16	wcel	$$wffb\in w$$
20	17 19	wa	$$wff\left(a\in w\wedge b\in w\right)$$
21		vt	$$setvart$$
22	21	cv	$$setvart$$
23	7	cv	$$setvarx$$
24		c1st	$$class{1}^{st}$$
25	15 24	cfv	$$class{1}^{st}\left(a\right)$$
26		c2nd	$$class{2}^{nd}$$
27	18 26	cfv	$$class{2}^{nd}\left(b\right)$$
28	25 27 23	co	$$class\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)$$
29		csg	$$class{-}_{𝑔}$$
30	5 29	cfv	$$class{-}_r$$
31	18 24	cfv	$$class{1}^{st}\left(b\right)$$
32	15 26	cfv	$$class{2}^{nd}\left(a\right)$$
33	31 32 23	co	$$class\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)$$
34	28 33 30	co	$$class\left(\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)\right)$$
35	22 34 23	co	$$class\left(tx\left(\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)\right)\right)$$
36		c0g	$$class{0}_{𝑔}$$
37	5 36	cfv	$$class{0}_r$$
38	35 37	wceq	$$wfftx\left(\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)\right)=0_r$$
39	38 21 10	wrex	$$wff\exists t\in stx\left(\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)\right)=0_r$$
40	20 39	wa	$$wff\left(\left(a\in w\wedge b\in w\right)\wedge \exists t\in stx\left(\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)\right)=0_r\right)$$
41	40 13 14	copab	$$class\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \exists t\in stx\left(\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)\right)=0_r\right)\right\}$$
42	12 11 41	csb	$$class⦋\left({\mathrm{Base}}_r\times s\right)/w⦌\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \exists t\in stx\left(\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)\right)=0_r\right)\right\}$$
43	7 6 42	csb	$$class⦋{\cdot }_r/x⦌⦋\left({\mathrm{Base}}_r\times s\right)/w⦌\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \exists t\in stx\left(\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)\right)=0_r\right)\right\}$$
44	1 3 2 2 43	cmpo	$$class\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋{\cdot }_r/x⦌⦋\left({\mathrm{Base}}_r\times s\right)/w⦌\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \exists t\in stx\left(\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)\right)=0_r\right)\right\}\right)$$
45	0 44	wceq	Could not format ~RL = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } ) : No typesetting found for wff ~RL = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } ) with typecode wff