Metamath Proof Explorer

Theorem oppr2idl

Description: Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses oppreqg.o 
|- O = ( oppR ` R )
oppr2idl.2 
|- ( ph -> R e. Ring )
Assertion oppr2idl 
|- ( ph -> ( 2Ideal ` R ) = ( 2Ideal ` O ) )

Proof

Step Hyp Ref Expression
1 oppreqg.o 
 |-  O = ( oppR ` R )
2 oppr2idl.2 
 |-  ( ph -> R e. Ring )
3 incom 
 |-  ( ( LIdeal ` R ) i^i ( LIdeal ` O ) ) = ( ( LIdeal ` O ) i^i ( LIdeal ` R ) )
4 1 2 opprlidlabs 
 |-  ( ph -> ( LIdeal ` R ) = ( LIdeal ` ( oppR ` O ) ) )
5 4 ineq2d 
 |-  ( ph -> ( ( LIdeal ` O ) i^i ( LIdeal ` R ) ) = ( ( LIdeal ` O ) i^i ( LIdeal ` ( oppR ` O ) ) ) )
6 3 5 eqtrid 
 |-  ( ph -> ( ( LIdeal ` R ) i^i ( LIdeal ` O ) ) = ( ( LIdeal ` O ) i^i ( LIdeal ` ( oppR ` O ) ) ) )
7 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
8 eqid 
 |-  ( LIdeal ` O ) = ( LIdeal ` O )
9 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
10 7 1 8 9 2idlval 
 |-  ( 2Ideal ` R ) = ( ( LIdeal ` R ) i^i ( LIdeal ` O ) )
11 eqid 
 |-  ( oppR ` O ) = ( oppR ` O )
12 eqid 
 |-  ( LIdeal ` ( oppR ` O ) ) = ( LIdeal ` ( oppR ` O ) )
13 eqid 
 |-  ( 2Ideal ` O ) = ( 2Ideal ` O )
14 8 11 12 13 2idlval 
 |-  ( 2Ideal ` O ) = ( ( LIdeal ` O ) i^i ( LIdeal ` ( oppR ` O ) ) )
15 6 10 14 3eqtr4g 
 |-  ( ph -> ( 2Ideal ` R ) = ( 2Ideal ` O ) )