Theorem erlcl2

Description: Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erlcl1.b	$$⊢B={\mathrm{Base}}_R$$
	erlcl1.e	No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
	erlcl1.s	$$⊢\phi \to S\subseteq B$$
	erlcl1.1	$$⊢\phi \to U\underset{\dot{}}{\sim }V$$
Assertion	erlcl2	$$⊢\phi \to V\in \left(B\times S\right)$$

Proof

Step	Hyp	Ref	Expression
1		erlcl1.b	$$⊢B={\mathrm{Base}}_R$$
2		erlcl1.e	Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
3		erlcl1.s	$$⊢\phi \to S\subseteq B$$
4		erlcl1.1	$$⊢\phi \to U\underset{\dot{}}{\sim }V$$
5		eqid	$$⊢0_R=0_R$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7		eqid	$$⊢{-}_R={-}_R$$
8		eqid	$$⊢B\times S=B\times S$$
9		eqid	$$⊢\left\{⟨a,b⟩|\left(\left(a\in \left(B\times S\right)\wedge b\in \left(B\times S\right)\right)\wedge \exists t\in St{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=0_R\right)\right\}=\left\{⟨a,b⟩|\left(\left(a\in \left(B\times S\right)\wedge b\in \left(B\times S\right)\right)\wedge \exists t\in St{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=0_R\right)\right\}$$
10	1 5 6 7 8 9 3	erlval	Could not format ( ph -> ( R ~RL S ) = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } ) : No typesetting found for |- ( ph -> ( R ~RL S ) = { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t ( .r ` R ) ( ( ( 1st ` a ) ( .r ` R ) ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) ( .r ` R ) ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } ) with typecode |-
11	2 10	eqtrid	$$⊢\phi \to \underset{\dot{}}{\sim }=\left\{⟨a,b⟩|\left(\left(a\in \left(B\times S\right)\wedge b\in \left(B\times S\right)\right)\wedge \exists t\in St{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=0_R\right)\right\}$$
12		simpl	$$⊢\left(a=U\wedge b=V\right)\to a=U$$
13	12	fveq2d	$$⊢\left(a=U\wedge b=V\right)\to 1^{st}\left(a\right)=1^{st}\left(U\right)$$
14		simpr	$$⊢\left(a=U\wedge b=V\right)\to b=V$$
15	14	fveq2d	$$⊢\left(a=U\wedge b=V\right)\to 2^{nd}\left(b\right)=2^{nd}\left(V\right)$$
16	13 15	oveq12d	$$⊢\left(a=U\wedge b=V\right)\to 1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)=1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)$$
17	14	fveq2d	$$⊢\left(a=U\wedge b=V\right)\to 1^{st}\left(b\right)=1^{st}\left(V\right)$$
18	12	fveq2d	$$⊢\left(a=U\wedge b=V\right)\to 2^{nd}\left(a\right)=2^{nd}\left(U\right)$$
19	17 18	oveq12d	$$⊢\left(a=U\wedge b=V\right)\to 1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)=1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)$$
20	16 19	oveq12d	$$⊢\left(a=U\wedge b=V\right)\to \left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)=\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)$$
21	20	oveq2d	$$⊢\left(a=U\wedge b=V\right)\to t{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=t{\cdot }_R\left(\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)\right)$$
22	21	eqeq1d	$$⊢\left(a=U\wedge b=V\right)\to \left(t{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=0_R\leftrightarrow t{\cdot }_R\left(\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)\right)=0_R\right)$$
23	22	rexbidv	$$⊢\left(a=U\wedge b=V\right)\to \left(\exists t\in St{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=0_R\leftrightarrow \exists t\in St{\cdot }_R\left(\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)\right)=0_R\right)$$
24	23	adantl	$$⊢\left(\phi \wedge \left(a=U\wedge b=V\right)\right)\to \left(\exists t\in St{\cdot }_R\left(\left(1^{st}\left(a\right){\cdot }_R{2}^{nd}\left(b\right)\right){-}_R\left(1^{st}\left(b\right){\cdot }_R{2}^{nd}\left(a\right)\right)\right)=0_R\leftrightarrow \exists t\in St{\cdot }_R\left(\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)\right)=0_R\right)$$
25	11 24	brab2d	$$⊢\phi \to \left(U\underset{\dot{}}{\sim }V\leftrightarrow \left(\left(U\in \left(B\times S\right)\wedge V\in \left(B\times S\right)\right)\wedge \exists t\in St{\cdot }_R\left(\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)\right)=0_R\right)\right)$$
26	4 25	mpbid	$$⊢\phi \to \left(\left(U\in \left(B\times S\right)\wedge V\in \left(B\times S\right)\right)\wedge \exists t\in St{\cdot }_R\left(\left(1^{st}\left(U\right){\cdot }_R{2}^{nd}\left(V\right)\right){-}_R\left(1^{st}\left(V\right){\cdot }_R{2}^{nd}\left(U\right)\right)\right)=0_R\right)$$
27	26	simplrd	$$⊢\phi \to V\in \left(B\times S\right)$$