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 = {opp}_{r} (R)$
	opprqus.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
	opprqusbas.r	$⊢ φ \to R \in V$
	opprqusbas.i	$⊢ φ \to I \subseteq B$
Assertion	opprqusbas	$⊢ φ \to {Base}_{{opp}_{r} (Q)} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$

Proof

Step	Hyp	Ref	Expression
1		opprqus.b	$⊢ B = {Base}_{R}$
2		opprqus.o	$⊢ O = {opp}_{r} (R)$
3		opprqus.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
4		opprqusbas.r	$⊢ φ \to R \in V$
5		opprqusbas.i	$⊢ φ \to I \subseteq B$
6		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
7		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
8	6 7	opprbas	$⊢ {Base}_{Q} = {Base}_{{opp}_{r} (Q)}$
9	2 1	oppreqg	$⊢ (R \in V \land I \subseteq B) \to R ~_{QG} I = O ~_{QG} I$
10	4 5 9	syl2anc	$⊢ φ \to R ~_{QG} I = O ~_{QG} I$
11	10	qseq2d	$⊢ φ \to B / (R ~_{QG} I) = B / (O ~_{QG} I)$
12	3	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} I)$
13	1	a1i	$⊢ φ \to B = {Base}_{R}$
14		ovexd	$⊢ φ \to R ~_{QG} I \in V$
15	12 13 14 4	qusbas	$⊢ φ \to B / (R ~_{QG} I) = {Base}_{Q}$
16		eqidd	$⊢ φ \to O /_{𝑠} (O ~_{QG} I) = O /_{𝑠} (O ~_{QG} I)$
17	2 1	opprbas	$⊢ B = {Base}_{O}$
18	17	a1i	$⊢ φ \to B = {Base}_{O}$
19		ovexd	$⊢ φ \to O ~_{QG} I \in V$
20	2	fvexi	$⊢ O \in V$
21	20	a1i	$⊢ φ \to O \in V$
22	16 18 19 21	qusbas	$⊢ φ \to B / (O ~_{QG} I) = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
23	11 15 22	3eqtr3d	$⊢ φ \to {Base}_{Q} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$
24	8 23	eqtr3id	$⊢ φ \to {Base}_{{opp}_{r} (Q)} = {Base}_{(O /_{𝑠} (O ~_{QG} I))}$

Metamath Proof Explorer

Theorem opprqusbas

Proof