Metamath Proof Explorer

Theorem qsdrng

Description: An ideal M is both left and right maximal if and only if the factor ring Q is a division ring. (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses qsdrng.0 
|- O = ( oppR ` R )
qsdrng.q 
|- Q = ( R /s ( R ~QG M ) )
qsdrng.r 
|- ( ph -> R e. NzRing )
qsdrng.2 
|- ( ph -> M e. ( 2Ideal ` R ) )
Assertion qsdrng 
|- ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) )

Proof

Step Hyp Ref Expression
1 qsdrng.0 
 |-  O = ( oppR ` R )
2 qsdrng.q 
 |-  Q = ( R /s ( R ~QG M ) )
3 qsdrng.r 
 |-  ( ph -> R e. NzRing )
4 qsdrng.2 
 |-  ( ph -> M e. ( 2Ideal ` R ) )
5 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
6 3 5 syl 
 |-  ( ph -> R e. Ring )
7 6 adantr 
 |-  ( ( ph /\ Q e. DivRing ) -> R e. Ring )
8 4 2idllidld 
 |-  ( ph -> M e. ( LIdeal ` R ) )
9 8 adantr 
 |-  ( ( ph /\ Q e. DivRing ) -> M e. ( LIdeal ` R ) )
10 drngnzr 
 |-  ( Q e. DivRing -> Q e. NzRing )
11 10 ad2antlr 
 |-  ( ( ( ph /\ Q e. DivRing ) /\ M = ( Base ` R ) ) -> Q e. NzRing )
12 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
13 2 12 qusring 
 |-  ( ( R e. Ring /\ M e. ( 2Ideal ` R ) ) -> Q e. Ring )
14 6 4 13 syl2anc 
 |-  ( ph -> Q e. Ring )
15 14 adantr 
 |-  ( ( ph /\ M = ( Base ` R ) ) -> Q e. Ring )
16 oveq2 
 |-  ( M = ( Base ` R ) -> ( R ~QG M ) = ( R ~QG ( Base ` R ) ) )
17 16 oveq2d 
 |-  ( M = ( Base ` R ) -> ( R /s ( R ~QG M ) ) = ( R /s ( R ~QG ( Base ` R ) ) ) )
18 2 17 eqtrid 
 |-  ( M = ( Base ` R ) -> Q = ( R /s ( R ~QG ( Base ` R ) ) ) )
19 18 fveq2d 
 |-  ( M = ( Base ` R ) -> ( Base ` Q ) = ( Base ` ( R /s ( R ~QG ( Base ` R ) ) ) ) )
20 6 ringgrpd 
 |-  ( ph -> R e. Grp )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 eqid 
 |-  ( R /s ( R ~QG ( Base ` R ) ) ) = ( R /s ( R ~QG ( Base ` R ) ) )
23 21 22 qustriv 
 |-  ( R e. Grp -> ( Base ` ( R /s ( R ~QG ( Base ` R ) ) ) ) = { ( Base ` R ) } )
24 20 23 syl 
 |-  ( ph -> ( Base ` ( R /s ( R ~QG ( Base ` R ) ) ) ) = { ( Base ` R ) } )
25 19 24 sylan9eqr 
 |-  ( ( ph /\ M = ( Base ` R ) ) -> ( Base ` Q ) = { ( Base ` R ) } )
26 25 fveq2d 
 |-  ( ( ph /\ M = ( Base ` R ) ) -> ( # ` ( Base ` Q ) ) = ( # ` { ( Base ` R ) } ) )
27 fvex 
 |-  ( Base ` R ) e. _V
28 hashsng 
 |-  ( ( Base ` R ) e. _V -> ( # ` { ( Base ` R ) } ) = 1 )
29 27 28 ax-mp 
 |-  ( # ` { ( Base ` R ) } ) = 1
30 26 29 eqtrdi 
 |-  ( ( ph /\ M = ( Base ` R ) ) -> ( # ` ( Base ` Q ) ) = 1 )
31 0ringnnzr 
 |-  ( Q e. Ring -> ( ( # ` ( Base ` Q ) ) = 1 <-> -. Q e. NzRing ) )
32 31 biimpa 
 |-  ( ( Q e. Ring /\ ( # ` ( Base ` Q ) ) = 1 ) -> -. Q e. NzRing )
33 15 30 32 syl2anc 
 |-  ( ( ph /\ M = ( Base ` R ) ) -> -. Q e. NzRing )
34 33 adantlr 
 |-  ( ( ( ph /\ Q e. DivRing ) /\ M = ( Base ` R ) ) -> -. Q e. NzRing )
35 11 34 pm2.65da 
 |-  ( ( ph /\ Q e. DivRing ) -> -. M = ( Base ` R ) )
36 35 neqned 
 |-  ( ( ph /\ Q e. DivRing ) -> M =/= ( Base ` R ) )
37 simplr 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> M C_ j )
38 simpr 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> -. j = M )
39 38 neqned 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> j =/= M )
40 39 necomd 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> M =/= j )
41 pssdifn0 
 |-  ( ( M C_ j /\ M =/= j ) -> ( j \ M ) =/= (/) )
42 37 40 41 syl2anc 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> ( j \ M ) =/= (/) )
43 n0 
 |-  ( ( j \ M ) =/= (/) <-> E. x x e. ( j \ M ) )
44 42 43 sylib 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> E. x x e. ( j \ M ) )
45 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> R e. NzRing )
46 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> M e. ( 2Ideal ` R ) )
47 simp-5r 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> Q e. DivRing )
48 simp-4r 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> j e. ( LIdeal ` R ) )
49 37 adantr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> M C_ j )
50 simpr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> x e. ( j \ M ) )
51 1 2 45 46 21 47 48 49 50 qsdrnglem2 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> j = ( Base ` R ) )
52 44 51 exlimddv 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) /\ -. j = M ) -> j = ( Base ` R ) )
53 52 ex 
 |-  ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) -> ( -. j = M -> j = ( Base ` R ) ) )
54 53 orrd 
 |-  ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) /\ M C_ j ) -> ( j = M \/ j = ( Base ` R ) ) )
55 54 ex 
 |-  ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` R ) ) -> ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
56 55 ralrimiva 
 |-  ( ( ph /\ Q e. DivRing ) -> A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
57 21 ismxidl 
 |-  ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) )
58 57 biimpar 
 |-  ( ( R e. Ring /\ ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` R ) )
59 7 9 36 56 58 syl13anc 
 |-  ( ( ph /\ Q e. DivRing ) -> M e. ( MaxIdeal ` R ) )
60 1 opprring 
 |-  ( R e. Ring -> O e. Ring )
61 6 60 syl 
 |-  ( ph -> O e. Ring )
62 61 adantr 
 |-  ( ( ph /\ Q e. DivRing ) -> O e. Ring )
63 4 adantr 
 |-  ( ( ph /\ Q e. DivRing ) -> M e. ( 2Ideal ` R ) )
64 63 1 2idlridld 
 |-  ( ( ph /\ Q e. DivRing ) -> M e. ( LIdeal ` O ) )
65 simplr 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> M C_ j )
66 simpr 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> -. j = M )
67 66 neqned 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> j =/= M )
68 67 necomd 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> M =/= j )
69 65 68 41 syl2anc 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> ( j \ M ) =/= (/) )
70 69 43 sylib 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> E. x x e. ( j \ M ) )
71 eqid 
 |-  ( oppR ` O ) = ( oppR ` O )
72 eqid 
 |-  ( O /s ( O ~QG M ) ) = ( O /s ( O ~QG M ) )
73 1 opprnzr 
 |-  ( R e. NzRing -> O e. NzRing )
74 3 73 syl 
 |-  ( ph -> O e. NzRing )
75 74 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> O e. NzRing )
76 1 6 oppr2idl 
 |-  ( ph -> ( 2Ideal ` R ) = ( 2Ideal ` O ) )
77 4 76 eleqtrd 
 |-  ( ph -> M e. ( 2Ideal ` O ) )
78 77 ad5antr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> M e. ( 2Ideal ` O ) )
79 1 21 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
80 eqid 
 |-  ( oppR ` Q ) = ( oppR ` Q )
81 80 opprdrng 
 |-  ( Q e. DivRing <-> ( oppR ` Q ) e. DivRing )
82 21 1 2 6 4 opprqusdrng 
 |-  ( ph -> ( ( oppR ` Q ) e. DivRing <-> ( O /s ( O ~QG M ) ) e. DivRing ) )
83 82 biimpa 
 |-  ( ( ph /\ ( oppR ` Q ) e. DivRing ) -> ( O /s ( O ~QG M ) ) e. DivRing )
84 81 83 sylan2b 
 |-  ( ( ph /\ Q e. DivRing ) -> ( O /s ( O ~QG M ) ) e. DivRing )
85 84 ad4antr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> ( O /s ( O ~QG M ) ) e. DivRing )
86 simp-4r 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> j e. ( LIdeal ` O ) )
87 65 adantr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> M C_ j )
88 simpr 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> x e. ( j \ M ) )
89 71 72 75 78 79 85 86 87 88 qsdrnglem2 
 |-  ( ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) /\ x e. ( j \ M ) ) -> j = ( Base ` R ) )
90 70 89 exlimddv 
 |-  ( ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) /\ -. j = M ) -> j = ( Base ` R ) )
91 90 ex 
 |-  ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) -> ( -. j = M -> j = ( Base ` R ) ) )
92 91 orrd 
 |-  ( ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) /\ M C_ j ) -> ( j = M \/ j = ( Base ` R ) ) )
93 92 ex 
 |-  ( ( ( ph /\ Q e. DivRing ) /\ j e. ( LIdeal ` O ) ) -> ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
94 93 ralrimiva 
 |-  ( ( ph /\ Q e. DivRing ) -> A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) )
95 79 ismxidl 
 |-  ( O e. Ring -> ( M e. ( MaxIdeal ` O ) <-> ( M e. ( LIdeal ` O ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) )
96 95 biimpar 
 |-  ( ( O e. Ring /\ ( M e. ( LIdeal ` O ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` O ) )
97 62 64 36 94 96 syl13anc 
 |-  ( ( ph /\ Q e. DivRing ) -> M e. ( MaxIdeal ` O ) )
98 59 97 jca 
 |-  ( ( ph /\ Q e. DivRing ) -> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) )
99 3 adantr 
 |-  ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> R e. NzRing )
100 simprl 
 |-  ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> M e. ( MaxIdeal ` R ) )
101 simprr 
 |-  ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> M e. ( MaxIdeal ` O ) )
102 1 2 99 100 101 qsdrngi 
 |-  ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> Q e. DivRing )
103 98 102 impbida 
 |-  ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) )