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 = ( oppR ` R )
opprqus.q 
|- Q = ( R /s ( R ~QG I ) )
opprqus1r.r 
|- ( ph -> R e. Ring )
opprqus1r.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
Assertion opprqus1r 
|- ( ph -> ( 1r ` ( oppR ` Q ) ) = ( 1r ` ( O /s ( O ~QG I ) ) ) )

Proof

Step Hyp Ref Expression
1 opprqus.b 
 |-  B = ( Base ` R )
2 opprqus.o 
 |-  O = ( oppR ` R )
3 opprqus.q 
 |-  Q = ( R /s ( R ~QG I ) )
4 opprqus1r.r 
 |-  ( ph -> R e. Ring )
5 opprqus1r.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
6 eqid 
 |-  ( Base ` ( oppR ` Q ) ) = ( Base ` ( oppR ` Q ) )
7 fvexd 
 |-  ( ph -> ( oppR ` Q ) e. _V )
8 ovexd 
 |-  ( ph -> ( O /s ( O ~QG I ) ) e. _V )
9 5 2idllidld 
 |-  ( ph -> I e. ( LIdeal ` R ) )
10 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
11 1 10 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
12 9 11 syl 
 |-  ( ph -> I C_ B )
13 1 2 3 4 12 opprqusbas 
 |-  ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
14 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) /\ y e. ( Base ` ( oppR ` Q ) ) ) -> R e. Ring )
15 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) /\ y e. ( Base ` ( oppR ` Q ) ) ) -> I e. ( 2Ideal ` R ) )
16 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
17 simpr 
 |-  ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) -> x e. ( Base ` ( oppR ` Q ) ) )
18 eqid 
 |-  ( oppR ` Q ) = ( oppR ` Q )
19 18 16 opprbas 
 |-  ( Base ` Q ) = ( Base ` ( oppR ` Q ) )
20 17 19 eleqtrrdi 
 |-  ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) -> x e. ( Base ` Q ) )
21 20 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) /\ y e. ( Base ` ( oppR ` Q ) ) ) -> x e. ( Base ` Q ) )
22 simpr 
 |-  ( ( ph /\ y e. ( Base ` ( oppR ` Q ) ) ) -> y e. ( Base ` ( oppR ` Q ) ) )
23 22 19 eleqtrrdi 
 |-  ( ( ph /\ y e. ( Base ` ( oppR ` Q ) ) ) -> y e. ( Base ` Q ) )
24 23 adantlr 
 |-  ( ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) /\ y e. ( Base ` ( oppR ` Q ) ) ) -> y e. ( Base ` Q ) )
25 1 2 3 14 15 16 21 24 opprqusmulr 
 |-  ( ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) /\ y e. ( Base ` ( oppR ` Q ) ) ) -> ( x ( .r ` ( oppR ` Q ) ) y ) = ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) )
26 6 7 8 13 25 urpropd 
 |-  ( ph -> ( 1r ` ( oppR ` Q ) ) = ( 1r ` ( O /s ( O ~QG I ) ) ) )