Theorem erldi

Description: Main property of 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$$
	erldi.1	$$⊢\underset{\dot{}}{0}=0_R$$
	erldi.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	erldi.3	$$⊢\underset{\dot{}}{-}={-}_R$$
	erldi.4	$$⊢\phi \to U\underset{\dot{}}{\sim }V$$
Assertion	erldi	$$⊢\phi \to \exists t\in St\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}$$

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		erldi.1	$$⊢\underset{\dot{}}{0}=0_R$$
5		erldi.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		erldi.3	$$⊢\underset{\dot{}}{-}={-}_R$$
7		erldi.4	$$⊢\phi \to U\underset{\dot{}}{\sim }V$$
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\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\underset{\dot{}}{0}\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\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\underset{\dot{}}{0}\right)\right\}$$
10	1 4 5 6 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 .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } ) : 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 .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } ) 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\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\underset{\dot{}}{0}\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)\underset{\dot{}}{·}{2}^{nd}\left(b\right)=1^{st}\left(U\right)\underset{\dot{}}{·}{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)\underset{\dot{}}{·}{2}^{nd}\left(a\right)=1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)$$
20	16 19	oveq12d	$$⊢\left(a=U\wedge b=V\right)\to \left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)=\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)$$
21	20	oveq2d	$$⊢\left(a=U\wedge b=V\right)\to t\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=t\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)$$
22	21	eqeq1d	$$⊢\left(a=U\wedge b=V\right)\to \left(t\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\underset{\dot{}}{0}\leftrightarrow t\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}\right)$$
23	22	rexbidv	$$⊢\left(a=U\wedge b=V\right)\to \left(\exists t\in St\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\underset{\dot{}}{0}\leftrightarrow \exists t\in St\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}\right)$$
24	23	adantl	$$⊢\left(\phi \wedge \left(a=U\wedge b=V\right)\right)\to \left(\exists t\in St\underset{\dot{}}{·}\left(\left(1^{st}\left(a\right)\underset{\dot{}}{·}{2}^{nd}\left(b\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(b\right)\underset{\dot{}}{·}{2}^{nd}\left(a\right)\right)\right)=\underset{\dot{}}{0}\leftrightarrow \exists t\in St\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}\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\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}\right)\right)$$
26	7 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\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}\right)$$
27	26	simprd	$$⊢\phi \to \exists t\in St\underset{\dot{}}{·}\left(\left(1^{st}\left(U\right)\underset{\dot{}}{·}{2}^{nd}\left(V\right)\right)\underset{\dot{}}{-}\left(1^{st}\left(V\right)\underset{\dot{}}{·}{2}^{nd}\left(U\right)\right)\right)=\underset{\dot{}}{0}$$