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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	opprqus.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	opprqus.q	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
	opprqusbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	opprqusbas.i	⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
Assertion	opprqusbas	⊢ ( 𝜑 → ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		opprqus.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		opprqus.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
3		opprqus.q	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
4		opprqusbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5		opprqusbas.i	⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
6		eqid	⊢ ( oppr ‘ 𝑄 ) = ( oppr ‘ 𝑄 )
7		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
8	6 7	opprbas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( oppr ‘ 𝑄 ) )
9	2 1	oppreqg	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
10	4 5 9	syl2anc	⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
11	10	qseq2d	⊢ ( 𝜑 → ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) = ( 𝐵 / ( 𝑂 ~QG 𝐼 ) ) )
12	3	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
13	1	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
14		ovexd	⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) ∈ V )
15	12 13 14 4	qusbas	⊢ ( 𝜑 → ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
16		eqidd	⊢ ( 𝜑 → ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) = ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
17	2 1	opprbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
18	17	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
19		ovexd	⊢ ( 𝜑 → ( 𝑂 ~QG 𝐼 ) ∈ V )
20	2	fvexi	⊢ 𝑂 ∈ V
21	20	a1i	⊢ ( 𝜑 → 𝑂 ∈ V )
22	16 18 19 21	qusbas	⊢ ( 𝜑 → ( 𝐵 / ( 𝑂 ~QG 𝐼 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
23	11 15 22	3eqtr3d	⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
24	8 23	eqtr3id	⊢ ( 𝜑 → ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )