This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐼 ) ) ) )