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 = ( oppR ` R )
opprqus.q 
|- Q = ( R /s ( R ~QG I ) )
opprqusbas.r 
|- ( ph -> R e. V )
opprqusbas.i 
|- ( ph -> I C_ B )
Assertion opprqusbas 
|- ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( 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 opprqusbas.r 
 |-  ( ph -> R e. V )
5 opprqusbas.i 
 |-  ( ph -> I C_ B )
6 eqid 
 |-  ( oppR ` Q ) = ( oppR ` Q )
7 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
8 6 7 opprbas 
 |-  ( Base ` Q ) = ( Base ` ( oppR ` Q ) )
9 2 1 oppreqg 
 |-  ( ( R e. V /\ I C_ B ) -> ( R ~QG I ) = ( O ~QG I ) )
10 4 5 9 syl2anc 
 |-  ( ph -> ( R ~QG I ) = ( O ~QG I ) )
11 10 qseq2d 
 |-  ( ph -> ( B /. ( R ~QG I ) ) = ( B /. ( O ~QG I ) ) )
12 3 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG I ) ) )
13 1 a1i 
 |-  ( ph -> B = ( Base ` R ) )
14 ovexd 
 |-  ( ph -> ( R ~QG I ) e. _V )
15 12 13 14 4 qusbas 
 |-  ( ph -> ( B /. ( R ~QG I ) ) = ( Base ` Q ) )
16 eqidd 
 |-  ( ph -> ( O /s ( O ~QG I ) ) = ( O /s ( O ~QG I ) ) )
17 2 1 opprbas 
 |-  B = ( Base ` O )
18 17 a1i 
 |-  ( ph -> B = ( Base ` O ) )
19 ovexd 
 |-  ( ph -> ( O ~QG I ) e. _V )
20 2 fvexi 
 |-  O e. _V
21 20 a1i 
 |-  ( ph -> O e. _V )
22 16 18 19 21 qusbas 
 |-  ( ph -> ( B /. ( O ~QG I ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
23 11 15 22 3eqtr3d 
 |-  ( ph -> ( Base ` Q ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
24 8 23 eqtr3id 
 |-  ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )