Theorem fracbas

Description: The base of the field of fractions. (Contributed by Thierry Arnoux, 10-May-2025)

	Ref	Expression
Hypotheses	fracbas.1	$$⊢B={\mathrm{Base}}_R$$
	fracbas.2	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	fracbas.3	$$⊢F=\mathrm{Frac}\left(R\right)$$
	fracbas.4	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathrm{RL}}E$$
Assertion	fracbas	$$⊢\left(B\times E\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_F$$

Proof

Step	Hyp	Ref	Expression
1		fracbas.1	$$⊢B={\mathrm{Base}}_R$$
2		fracbas.2	$$⊢E=\mathrm{RLReg}\left(R\right)$$
3		fracbas.3	$$⊢F=\mathrm{Frac}\left(R\right)$$
4		fracbas.4	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathrm{RL}}E$$
5		eqid	$$⊢0_R=0_R$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7		eqid	$$⊢{-}_R={-}_R$$
8		eqid	$$⊢B\times E=B\times E$$
9		fracval	$$⊢\mathrm{Frac}\left(R\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
10	2	oveq2i	$$⊢R\mathrm{RLocal}E=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
11	9 3 10	3eqtr4i	$$⊢F=R\mathrm{RLocal}E$$
12		id	$$⊢R\in \mathrm{V}\to R\in \mathrm{V}$$
13	2 1	rrgss	$$⊢E\subseteq B$$
14	13	a1i	$$⊢R\in \mathrm{V}\to E\subseteq B$$
15	1 5 6 7 8 11 4 12 14	rlocbas	$$⊢R\in \mathrm{V}\to \left(B\times E\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_F$$
16		0qs	$$⊢\varnothing /\underset{\dot{}}{\sim }=\varnothing$$
17		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_R=\varnothing$$
18	1 17	eqtrid	$$⊢\neg R\in \mathrm{V}\to B=\varnothing$$
19	18	xpeq1d	$$⊢\neg R\in \mathrm{V}\to B\times E=\varnothing \times E$$
20		0xp	$$⊢\varnothing \times E=\varnothing$$
21	19 20	eqtrdi	$$⊢\neg R\in \mathrm{V}\to B\times E=\varnothing$$
22	21	qseq1d	$$⊢\neg R\in \mathrm{V}\to \left(B\times E\right)/\underset{\dot{}}{\sim }=\varnothing /\underset{\dot{}}{\sim }$$
23		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{Frac}\left(R\right)=\varnothing$$
24	3 23	eqtrid	$$⊢\neg R\in \mathrm{V}\to F=\varnothing$$
25	24	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_F={\mathrm{Base}}_{\varnothing }$$
26		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
27	25 26	eqtr4di	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_F=\varnothing$$
28	16 22 27	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to \left(B\times E\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_F$$
29	15 28	pm2.61i	$$⊢\left(B\times E\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_F$$