Metamath Proof Explorer

Theorem opprqus1r

Description: The ring unity of the quotient of the opposite ring is the same as the ring unity 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
opprqus1r.r ⊢ φ → R ∈ Ring
opprqus1r.i ⊢ φ → I ∈ 2Ideal ⁡ R
Assertion opprqus1r ⊢ φ → 1 opp r ⁡ Q = 1 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 opprqus1r.r ⊢ φ → R ∈ Ring
5 opprqus1r.i ⊢ φ → I ∈ 2Ideal ⁡ R
6 eqid ⊢ Base opp r ⁡ Q = Base opp r ⁡ Q
7 fvexd ⊢ φ → opp r ⁡ Q ∈ V
8 ovexd ⊢ φ → O / 𝑠 O ~ QG I ∈ V
9 5 2idllidld ⊢ φ → I ∈ LIdeal ⁡ R
10 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
11 1 10 lidlss ⊢ I ∈ LIdeal ⁡ R → I ⊆ B
12 9 11 syl ⊢ φ → I ⊆ B
13 1 2 3 4 12 opprqusbas ⊢ φ → Base opp r ⁡ Q = Base O / 𝑠 O ~ QG I
14 4 ad2antrr ⊢ φ ∧ x ∈ Base opp r ⁡ Q ∧ y ∈ Base opp r ⁡ Q → R ∈ Ring
15 5 ad2antrr ⊢ φ ∧ x ∈ Base opp r ⁡ Q ∧ y ∈ Base opp r ⁡ Q → I ∈ 2Ideal ⁡ R
16 eqid ⊢ Base Q = Base Q
17 simpr ⊢ φ ∧ x ∈ Base opp r ⁡ Q → x ∈ Base opp r ⁡ Q
18 eqid ⊢ opp r ⁡ Q = opp r ⁡ Q
19 18 16 opprbas ⊢ Base Q = Base opp r ⁡ Q
20 17 19 eleqtrrdi ⊢ φ ∧ x ∈ Base opp r ⁡ Q → x ∈ Base Q
21 20 adantr ⊢ φ ∧ x ∈ Base opp r ⁡ Q ∧ y ∈ Base opp r ⁡ Q → x ∈ Base Q
22 simpr ⊢ φ ∧ y ∈ Base opp r ⁡ Q → y ∈ Base opp r ⁡ Q
23 22 19 eleqtrrdi ⊢ φ ∧ y ∈ Base opp r ⁡ Q → y ∈ Base Q
24 23 adantlr ⊢ φ ∧ x ∈ Base opp r ⁡ Q ∧ y ∈ Base opp r ⁡ Q → y ∈ Base Q
25 1 2 3 14 15 16 21 24 opprqusmulr ⊢ φ ∧ x ∈ Base opp r ⁡ Q ∧ y ∈ Base opp r ⁡ Q → x ⋅ opp r ⁡ Q y = x ⋅ O / 𝑠 O ~ QG I y
26 6 7 8 13 25 urpropd ⊢ φ → 1 opp r ⁡ Q = 1 O / 𝑠 O ~ QG I