This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppreqg

Description: Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses oppreqg.o 
|- O = ( oppR ` R )
oppreqg.b 
|- B = ( Base ` R )
Assertion oppreqg 
|- ( ( R e. V /\ I C_ B ) -> ( R ~QG I ) = ( O ~QG I ) )

Proof

Step Hyp Ref Expression
1 oppreqg.o 
 |-  O = ( oppR ` R )
2 oppreqg.b 
 |-  B = ( Base ` R )
3 eqid 
 |-  ( invg ` R ) = ( invg ` R )
4 eqid 
 |-  ( +g ` R ) = ( +g ` R )
5 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
6 2 3 4 5 eqgfval 
 |-  ( ( R e. V /\ I C_ B ) -> ( R ~QG I ) = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` R ) ` x ) ( +g ` R ) y ) e. I ) } )
7 1 fvexi 
 |-  O e. _V
8 1 2 opprbas 
 |-  B = ( Base ` O )
9 1 3 opprneg 
 |-  ( invg ` R ) = ( invg ` O )
10 1 4 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
11 eqid 
 |-  ( O ~QG I ) = ( O ~QG I )
12 8 9 10 11 eqgfval 
 |-  ( ( O e. _V /\ I C_ B ) -> ( O ~QG I ) = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` R ) ` x ) ( +g ` R ) y ) e. I ) } )
13 7 12 mpan 
 |-  ( I C_ B -> ( O ~QG I ) = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` R ) ` x ) ( +g ` R ) y ) e. I ) } )
14 13 adantl 
 |-  ( ( R e. V /\ I C_ B ) -> ( O ~QG I ) = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` R ) ` x ) ( +g ` R ) y ) e. I ) } )
15 6 14 eqtr4d 
 |-  ( ( R e. V /\ I C_ B ) -> ( R ~QG I ) = ( O ~QG I ) )