Theorem fracbas

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

	Ref	Expression
Hypotheses	fracbas.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	fracbas.2	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	fracbas.3	⊢ 𝐹 = ( Frac ‘ 𝑅 )
	fracbas.4	⊢ ∼ = ( 𝑅 ~RL 𝐸 )
Assertion	fracbas	⊢ ( ( 𝐵 × 𝐸 ) / ∼ ) = ( Base ‘ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fracbas.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		fracbas.2	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
3		fracbas.3	⊢ 𝐹 = ( Frac ‘ 𝑅 )
4		fracbas.4	⊢ ∼ = ( 𝑅 ~RL 𝐸 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
8		eqid	⊢ ( 𝐵 × 𝐸 ) = ( 𝐵 × 𝐸 )
9		fracval	⊢ ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )
10	2	oveq2i	⊢ ( 𝑅 RLocal 𝐸 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )
11	9 3 10	3eqtr4i	⊢ 𝐹 = ( 𝑅 RLocal 𝐸 )
12		id	⊢ ( 𝑅 ∈ V → 𝑅 ∈ V )
13	2 1	rrgss	⊢ 𝐸 ⊆ 𝐵
14	13	a1i	⊢ ( 𝑅 ∈ V → 𝐸 ⊆ 𝐵 )
15	1 5 6 7 8 11 4 12 14	rlocbas	⊢ ( 𝑅 ∈ V → ( ( 𝐵 × 𝐸 ) / ∼ ) = ( Base ‘ 𝐹 ) )
16		0qs	⊢ ( ∅ / ∼ ) = ∅
17		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
18	1 17	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
19	18	xpeq1d	⊢ ( ¬ 𝑅 ∈ V → ( 𝐵 × 𝐸 ) = ( ∅ × 𝐸 ) )
20		0xp	⊢ ( ∅ × 𝐸 ) = ∅
21	19 20	eqtrdi	⊢ ( ¬ 𝑅 ∈ V → ( 𝐵 × 𝐸 ) = ∅ )
22	21	qseq1d	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝐵 × 𝐸 ) / ∼ ) = ( ∅ / ∼ ) )
23		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Frac ‘ 𝑅 ) = ∅ )
24	3 23	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝐹 = ∅ )
25	24	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝐹 ) = ( Base ‘ ∅ ) )
26		base0	⊢ ∅ = ( Base ‘ ∅ )
27	25 26	eqtr4di	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝐹 ) = ∅ )
28	16 22 27	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝐵 × 𝐸 ) / ∼ ) = ( Base ‘ 𝐹 ) )
29	15 28	pm2.61i	⊢ ( ( 𝐵 × 𝐸 ) / ∼ ) = ( Base ‘ 𝐹 )