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	No typesetting found for |- F = ( Frac ` R ) with typecode |-
	fracbas.4	No typesetting found for |- .~ = ( R ~RL E ) with typecode |-
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	Could not format F = ( Frac ` R ) : No typesetting found for |- F = ( Frac ` R ) with typecode |-
4		fracbas.4	Could not format .~ = ( R ~RL E ) : No typesetting found for |- .~ = ( R ~RL E ) with typecode |-
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	Could not format ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) with typecode |-
10	2	oveq2i	Could not format ( R RLocal E ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( R RLocal E ) = ( R RLocal ( RLReg ` R ) ) with typecode |-
11	9 3 10	3eqtr4i	Could not format F = ( R RLocal E ) : No typesetting found for |- F = ( R RLocal E ) with typecode |-
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	Could not format ( -. R e. _V -> ( Frac ` R ) = (/) ) : No typesetting found for |- ( -. R e. _V -> ( Frac ` R ) = (/) ) with typecode |-
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$$