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

Proof

Step Hyp Ref Expression
1 opprqus.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 opprqus.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
3 opprqus.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
4 opprqus1r.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 opprqus1r.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
6 eqid ⊢ ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( Base ‘ ( oppr ‘ 𝑄 ) )
7 fvexd ⊢ ( 𝜑 → ( oppr ‘ 𝑄 ) ∈ V )
8 ovexd ⊢ ( 𝜑 → ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ∈ V )
9 5 2idllidld ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
10 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
11 1 10 lidlss ⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
12 9 11 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
13 1 2 3 4 12 opprqusbas ⊢ ( 𝜑 → ( Base ‘ ( oppr ‘ 𝑄 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
14 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑅 ∈ Ring )
15 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
16 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) )
18 eqid ⊢ ( oppr ‘ 𝑄 ) = ( oppr ‘ 𝑄 )
19 18 16 opprbas ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( oppr ‘ 𝑄 ) )
20 17 19 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑄 ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑄 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) )
23 22 19 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑄 ) )
24 23 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑄 ) )
25 1 2 3 14 15 16 21 24 opprqusmulr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( oppr ‘ 𝑄 ) ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑦 ) )
26 6 7 8 13 25 urpropd ⊢ ( 𝜑 → ( 1r ‘ ( oppr ‘ 𝑄 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )