Theorem fracbas

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

	Ref	Expression
Hypotheses	fracbas.1	|- B = ( Base ` R )
	fracbas.2	|- E = ( RLReg ` R )
	fracbas.3	|- F = ( Frac ` R )
	fracbas.4	|- .~ = ( R ~RL E )
Assertion	fracbas	|- ( ( B X. E ) /. .~ ) = ( Base ` F )

Proof

Step	Hyp	Ref	Expression
1		fracbas.1	|- B = ( Base ` R )
2		fracbas.2	|- E = ( RLReg ` R )
3		fracbas.3	|- F = ( Frac ` R )
4		fracbas.4	|- .~ = ( R ~RL E )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6		eqid	|- ( .r ` R ) = ( .r ` R )
7		eqid	|- ( -g ` R ) = ( -g ` R )
8		eqid	|- ( B X. E ) = ( B X. E )
9		fracval	|- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) )
10	2	oveq2i	|- ( R RLocal E ) = ( R RLocal ( RLReg ` R ) )
11	9 3 10	3eqtr4i	|- F = ( R RLocal E )
12		id	|- ( R e. _V -> R e. _V )
13	2 1	rrgss	|- E C_ B
14	13	a1i	|- ( R e. _V -> E C_ B )
15	1 5 6 7 8 11 4 12 14	rlocbas	|- ( R e. _V -> ( ( B X. E ) /. .~ ) = ( Base ` F ) )
16		0qs	|- ( (/) /. .~ ) = (/)
17		fvprc	|- ( -. R e. _V -> ( Base ` R ) = (/) )
18	1 17	eqtrid	|- ( -. R e. _V -> B = (/) )
19	18	xpeq1d	|- ( -. R e. _V -> ( B X. E ) = ( (/) X. E ) )
20		0xp	|- ( (/) X. E ) = (/)
21	19 20	eqtrdi	|- ( -. R e. _V -> ( B X. E ) = (/) )
22	21	qseq1d	|- ( -. R e. _V -> ( ( B X. E ) /. .~ ) = ( (/) /. .~ ) )
23		fvprc	|- ( -. R e. _V -> ( Frac ` R ) = (/) )
24	3 23	eqtrid	|- ( -. R e. _V -> F = (/) )
25	24	fveq2d	|- ( -. R e. _V -> ( Base ` F ) = ( Base ` (/) ) )
26		base0	|- (/) = ( Base ` (/) )
27	25 26	eqtr4di	|- ( -. R e. _V -> ( Base ` F ) = (/) )
28	16 22 27	3eqtr4a	|- ( -. R e. _V -> ( ( B X. E ) /. .~ ) = ( Base ` F ) )
29	15 28	pm2.61i	|- ( ( B X. E ) /. .~ ) = ( Base ` F )