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 ⊢ B = Base R
opprqus.o ⊢ O = opp r ⁡ R
opprqus.q ⊢ Q = R / 𝑠 R ~ QG I
opprqusbas.r ⊢ φ → R ∈ V
opprqusbas.i ⊢ φ → I ⊆ B
Assertion opprqusbas ⊢ φ → 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 ⊢ φ → R ∈ V
5 opprqusbas.i ⊢ φ → I ⊆ 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 ∈ V ∧ I ⊆ B → R ~ QG I = O ~ QG I
10 4 5 9 syl2anc ⊢ φ → R ~ QG I = O ~ QG I
11 10 qseq2d ⊢ φ → B / R ~ QG I = B / O ~ QG I
12 3 a1i ⊢ φ → Q = R / 𝑠 R ~ QG I
13 1 a1i ⊢ φ → B = Base R
14 ovexd ⊢ φ → R ~ QG I ∈ V
15 12 13 14 4 qusbas ⊢ φ → B / R ~ QG I = Base Q
16 eqidd ⊢ φ → O / 𝑠 O ~ QG I = O / 𝑠 O ~ QG I
17 2 1 opprbas ⊢ B = Base O
18 17 a1i ⊢ φ → B = Base O
19 ovexd ⊢ φ → O ~ QG I ∈ V
20 2 fvexi ⊢ O ∈ V
21 20 a1i ⊢ φ → O ∈ V
22 16 18 19 21 qusbas ⊢ φ → B / O ~ QG I = Base O / 𝑠 O ~ QG I
23 11 15 22 3eqtr3d ⊢ φ → Base Q = Base O / 𝑠 O ~ QG I
24 8 23 eqtr3id ⊢ φ → Base opp r ⁡ Q = Base O / 𝑠 O ~ QG I