Metamath Proof Explorer

Theorem opprqusdrng

Description: The quotient of the opposite ring is a division ring iff the opposite of the quotient ring is. (Contributed by Thierry Arnoux, 13-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 opprqusdrng 
|- ( ph -> ( ( oppR ` Q ) e. DivRing <-> ( O /s ( O ~QG I ) ) e. DivRing ) )

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 
 |-  ( oppR ` Q ) = ( oppR ` Q )
7 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
8 6 7 oppr1 
 |-  ( 1r ` Q ) = ( 1r ` ( oppR ` Q ) )
9 1 2 3 4 5 opprqus1r 
 |-  ( ph -> ( 1r ` ( oppR ` Q ) ) = ( 1r ` ( O /s ( O ~QG I ) ) ) )
10 8 9 eqtrid 
 |-  ( ph -> ( 1r ` Q ) = ( 1r ` ( O /s ( O ~QG I ) ) ) )
11 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
12 6 11 oppr0 
 |-  ( 0g ` Q ) = ( 0g ` ( oppR ` Q ) )
13 5 2idllidld 
 |-  ( ph -> I e. ( LIdeal ` R ) )
14 lidlnsg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( NrmSGrp ` R ) )
15 4 13 14 syl2anc 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
16 1 2 3 15 opprqus0g 
 |-  ( ph -> ( 0g ` ( oppR ` Q ) ) = ( 0g ` ( O /s ( O ~QG I ) ) ) )
17 12 16 eqtrid 
 |-  ( ph -> ( 0g ` Q ) = ( 0g ` ( O /s ( O ~QG I ) ) ) )
18 10 17 neeq12d 
 |-  ( ph -> ( ( 1r ` Q ) =/= ( 0g ` Q ) <-> ( 1r ` ( O /s ( O ~QG I ) ) ) =/= ( 0g ` ( O /s ( O ~QG I ) ) ) ) )
19 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
20 6 19 opprbas 
 |-  ( Base ` Q ) = ( Base ` ( oppR ` Q ) )
21 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
22 1 21 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
23 13 22 syl 
 |-  ( ph -> I C_ B )
24 1 2 3 4 23 opprqusbas 
 |-  ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
25 20 24 eqtrid 
 |-  ( ph -> ( Base ` Q ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
26 17 sneqd 
 |-  ( ph -> { ( 0g ` Q ) } = { ( 0g ` ( O /s ( O ~QG I ) ) ) } )
27 25 26 difeq12d 
 |-  ( ph -> ( ( Base ` Q ) \ { ( 0g ` Q ) } ) = ( ( Base ` ( O /s ( O ~QG I ) ) ) \ { ( 0g ` ( O /s ( O ~QG I ) ) ) } ) )
28 25 adantr 
 |-  ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) -> ( Base ` Q ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
29 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> R e. Ring )
30 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> I e. ( 2Ideal ` R ) )
31 simplr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) )
32 31 eldifad 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> x e. ( Base ` Q ) )
33 simpr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> y e. ( Base ` Q ) )
34 1 2 3 29 30 19 32 33 opprqusmulr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> ( x ( .r ` ( oppR ` Q ) ) y ) = ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) )
35 10 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> ( 1r ` Q ) = ( 1r ` ( O /s ( O ~QG I ) ) ) )
36 34 35 eqeq12d 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> ( ( x ( .r ` ( oppR ` Q ) ) y ) = ( 1r ` Q ) <-> ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) )
37 1 2 3 29 30 19 33 32 opprqusmulr 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> ( y ( .r ` ( oppR ` Q ) ) x ) = ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) )
38 37 35 eqeq12d 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> ( ( y ( .r ` ( oppR ` Q ) ) x ) = ( 1r ` Q ) <-> ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) )
39 36 38 anbi12d 
 |-  ( ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ y e. ( Base ` Q ) ) -> ( ( ( x ( .r ` ( oppR ` Q ) ) y ) = ( 1r ` Q ) /\ ( y ( .r ` ( oppR ` Q ) ) x ) = ( 1r ` Q ) ) <-> ( ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) = ( 1r ` ( O /s ( O ~QG I ) ) ) /\ ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) ) )
40 28 39 rexeqbidva 
 |-  ( ( ph /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) -> ( E. y e. ( Base ` Q ) ( ( x ( .r ` ( oppR ` Q ) ) y ) = ( 1r ` Q ) /\ ( y ( .r ` ( oppR ` Q ) ) x ) = ( 1r ` Q ) ) <-> E. y e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) = ( 1r ` ( O /s ( O ~QG I ) ) ) /\ ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) ) )
41 27 40 raleqbidva 
 |-  ( ph -> ( A. x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) E. y e. ( Base ` Q ) ( ( x ( .r ` ( oppR ` Q ) ) y ) = ( 1r ` Q ) /\ ( y ( .r ` ( oppR ` Q ) ) x ) = ( 1r ` Q ) ) <-> A. x e. ( ( Base ` ( O /s ( O ~QG I ) ) ) \ { ( 0g ` ( O /s ( O ~QG I ) ) ) } ) E. y e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) = ( 1r ` ( O /s ( O ~QG I ) ) ) /\ ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) ) )
42 18 41 anbi12d 
 |-  ( ph -> ( ( ( 1r ` Q ) =/= ( 0g ` Q ) /\ A. x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) E. y e. ( Base ` Q ) ( ( x ( .r ` ( oppR ` Q ) ) y ) = ( 1r ` Q ) /\ ( y ( .r ` ( oppR ` Q ) ) x ) = ( 1r ` Q ) ) ) <-> ( ( 1r ` ( O /s ( O ~QG I ) ) ) =/= ( 0g ` ( O /s ( O ~QG I ) ) ) /\ A. x e. ( ( Base ` ( O /s ( O ~QG I ) ) ) \ { ( 0g ` ( O /s ( O ~QG I ) ) ) } ) E. y e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) = ( 1r ` ( O /s ( O ~QG I ) ) ) /\ ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) ) ) )
43 eqid 
 |-  ( .r ` ( oppR ` Q ) ) = ( .r ` ( oppR ` Q ) )
44 eqid 
 |-  ( Unit ` Q ) = ( Unit ` Q )
45 44 6 opprunit 
 |-  ( Unit ` Q ) = ( Unit ` ( oppR ` Q ) )
46 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
47 3 46 qusring 
 |-  ( ( R e. Ring /\ I e. ( 2Ideal ` R ) ) -> Q e. Ring )
48 4 5 47 syl2anc 
 |-  ( ph -> Q e. Ring )
49 6 opprring 
 |-  ( Q e. Ring -> ( oppR ` Q ) e. Ring )
50 48 49 syl 
 |-  ( ph -> ( oppR ` Q ) e. Ring )
51 20 12 8 43 45 50 isdrng4 
 |-  ( ph -> ( ( oppR ` Q ) e. DivRing <-> ( ( 1r ` Q ) =/= ( 0g ` Q ) /\ A. x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) E. y e. ( Base ` Q ) ( ( x ( .r ` ( oppR ` Q ) ) y ) = ( 1r ` Q ) /\ ( y ( .r ` ( oppR ` Q ) ) x ) = ( 1r ` Q ) ) ) ) )
52 eqid 
 |-  ( Base ` ( O /s ( O ~QG I ) ) ) = ( Base ` ( O /s ( O ~QG I ) ) )
53 eqid 
 |-  ( 0g ` ( O /s ( O ~QG I ) ) ) = ( 0g ` ( O /s ( O ~QG I ) ) )
54 eqid 
 |-  ( 1r ` ( O /s ( O ~QG I ) ) ) = ( 1r ` ( O /s ( O ~QG I ) ) )
55 eqid 
 |-  ( .r ` ( O /s ( O ~QG I ) ) ) = ( .r ` ( O /s ( O ~QG I ) ) )
56 eqid 
 |-  ( Unit ` ( O /s ( O ~QG I ) ) ) = ( Unit ` ( O /s ( O ~QG I ) ) )
57 2 opprring 
 |-  ( R e. Ring -> O e. Ring )
58 4 57 syl 
 |-  ( ph -> O e. Ring )
59 2 4 oppr2idl 
 |-  ( ph -> ( 2Ideal ` R ) = ( 2Ideal ` O ) )
60 5 59 eleqtrd 
 |-  ( ph -> I e. ( 2Ideal ` O ) )
61 eqid 
 |-  ( O /s ( O ~QG I ) ) = ( O /s ( O ~QG I ) )
62 eqid 
 |-  ( 2Ideal ` O ) = ( 2Ideal ` O )
63 61 62 qusring 
 |-  ( ( O e. Ring /\ I e. ( 2Ideal ` O ) ) -> ( O /s ( O ~QG I ) ) e. Ring )
64 58 60 63 syl2anc 
 |-  ( ph -> ( O /s ( O ~QG I ) ) e. Ring )
65 52 53 54 55 56 64 isdrng4 
 |-  ( ph -> ( ( O /s ( O ~QG I ) ) e. DivRing <-> ( ( 1r ` ( O /s ( O ~QG I ) ) ) =/= ( 0g ` ( O /s ( O ~QG I ) ) ) /\ A. x e. ( ( Base ` ( O /s ( O ~QG I ) ) ) \ { ( 0g ` ( O /s ( O ~QG I ) ) ) } ) E. y e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( x ( .r ` ( O /s ( O ~QG I ) ) ) y ) = ( 1r ` ( O /s ( O ~QG I ) ) ) /\ ( y ( .r ` ( O /s ( O ~QG I ) ) ) x ) = ( 1r ` ( O /s ( O ~QG I ) ) ) ) ) ) )
66 42 51 65 3bitr4d 
 |-  ( ph -> ( ( oppR ` Q ) e. DivRing <-> ( O /s ( O ~QG I ) ) e. DivRing ) )