Theorem opprqusbas

Description: The base of the quotient of the opposite ring is the same as the base of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	opprqus.b	|- B = ( Base ` R )
	opprqus.o	|- O = ( oppR ` R )
	opprqus.q	|- Q = ( R /s ( R ~QG I ) )
	opprqusbas.r	|- ( ph -> R e. V )
	opprqusbas.i	|- ( ph -> I C_ B )
Assertion	opprqusbas	|- ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		opprqus.b	|- B = ( Base ` R )
2		opprqus.o	|- O = ( oppR ` R )
3		opprqus.q	|- Q = ( R /s ( R ~QG I ) )
4		opprqusbas.r	|- ( ph -> R e. V )
5		opprqusbas.i	|- ( ph -> I C_ B )
6		eqid	|- ( oppR ` Q ) = ( oppR ` Q )
7		eqid	|- ( Base ` Q ) = ( Base ` Q )
8	6 7	opprbas	|- ( Base ` Q ) = ( Base ` ( oppR ` Q ) )
9	2 1	oppreqg	|- ( ( R e. V /\ I C_ B ) -> ( R ~QG I ) = ( O ~QG I ) )
10	4 5 9	syl2anc	|- ( ph -> ( R ~QG I ) = ( O ~QG I ) )
11	10	qseq2d	|- ( ph -> ( B /. ( R ~QG I ) ) = ( B /. ( O ~QG I ) ) )
12	3	a1i	|- ( ph -> Q = ( R /s ( R ~QG I ) ) )
13	1	a1i	|- ( ph -> B = ( Base ` R ) )
14		ovexd	|- ( ph -> ( R ~QG I ) e. _V )
15	12 13 14 4	qusbas	|- ( ph -> ( B /. ( R ~QG I ) ) = ( Base ` Q ) )
16		eqidd	|- ( ph -> ( O /s ( O ~QG I ) ) = ( O /s ( O ~QG I ) ) )
17	2 1	opprbas	|- B = ( Base ` O )
18	17	a1i	|- ( ph -> B = ( Base ` O ) )
19		ovexd	|- ( ph -> ( O ~QG I ) e. _V )
20	2	fvexi	|- O e. _V
21	20	a1i	|- ( ph -> O e. _V )
22	16 18 19 21	qusbas	|- ( ph -> ( B /. ( O ~QG I ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
23	11 15 22	3eqtr3d	|- ( ph -> ( Base ` Q ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
24	8 23	eqtr3id	|- ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )