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

Metamath Proof Explorer

Theorem opprlidlabs

Description: The ideals of the opposite ring's opposite ring are the ideals of the original ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 oppreqg.o 
 |-  O = ( oppR ` R )
2 oppr2idl.2 
 |-  ( ph -> R e. Ring )
3 eqid 
 |-  ( Base ` O ) = ( Base ` O )
4 eqid 
 |-  ( .r ` O ) = ( .r ` O )
5 eqid 
 |-  ( oppR ` O ) = ( oppR ` O )
6 eqid 
 |-  ( .r ` ( oppR ` O ) ) = ( .r ` ( oppR ` O ) )
7 3 4 5 6 opprmul 
 |-  ( x ( .r ` ( oppR ` O ) ) a ) = ( a ( .r ` O ) x )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 8 9 1 4 opprmul 
 |-  ( a ( .r ` O ) x ) = ( x ( .r ` R ) a )
11 7 10 eqtr2i 
 |-  ( x ( .r ` R ) a ) = ( x ( .r ` ( oppR ` O ) ) a )
12 11 a1i 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ a e. i ) /\ b e. i ) -> ( x ( .r ` R ) a ) = ( x ( .r ` ( oppR ` O ) ) a ) )
13 12 oveq1d 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ a e. i ) /\ b e. i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) = ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) )
14 13 eleq1d 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ a e. i ) /\ b e. i ) -> ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i <-> ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) e. i ) )
15 14 ralbidva 
 |-  ( ( ( ph /\ x e. ( Base ` R ) ) /\ a e. i ) -> ( A. b e. i ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i <-> A. b e. i ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) e. i ) )
16 15 anasss 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. i ) ) -> ( A. b e. i ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i <-> A. b e. i ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) e. i ) )
17 16 2ralbidva 
 |-  ( ph -> ( A. x e. ( Base ` R ) A. a e. i A. b e. i ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i <-> A. x e. ( Base ` R ) A. a e. i A. b e. i ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) e. i ) )
18 17 3anbi3d 
 |-  ( ph -> ( ( i C_ ( Base ` R ) /\ i =/= (/) /\ A. x e. ( Base ` R ) A. a e. i A. b e. i ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i ) <-> ( i C_ ( Base ` R ) /\ i =/= (/) /\ A. x e. ( Base ` R ) A. a e. i A. b e. i ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) e. i ) ) )
19 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
20 eqid 
 |-  ( +g ` R ) = ( +g ` R )
21 19 8 20 9 islidl 
 |-  ( i e. ( LIdeal ` R ) <-> ( i C_ ( Base ` R ) /\ i =/= (/) /\ A. x e. ( Base ` R ) A. a e. i A. b e. i ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i ) )
22 eqid 
 |-  ( LIdeal ` ( oppR ` O ) ) = ( LIdeal ` ( oppR ` O ) )
23 1 8 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
24 5 23 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` O ) )
25 1 20 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
26 5 25 oppradd 
 |-  ( +g ` R ) = ( +g ` ( oppR ` O ) )
27 22 24 26 6 islidl 
 |-  ( i e. ( LIdeal ` ( oppR ` O ) ) <-> ( i C_ ( Base ` R ) /\ i =/= (/) /\ A. x e. ( Base ` R ) A. a e. i A. b e. i ( ( x ( .r ` ( oppR ` O ) ) a ) ( +g ` R ) b ) e. i ) )
28 18 21 27 3bitr4g 
 |-  ( ph -> ( i e. ( LIdeal ` R ) <-> i e. ( LIdeal ` ( oppR ` O ) ) ) )
29 28 eqrdv 
 |-  ( ph -> ( LIdeal ` R ) = ( LIdeal ` ( oppR ` O ) ) )