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

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 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
qsdrng.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
qsdrng.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
qsdrng.2 ⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
Assertion qsdrng ( 𝜑 → ( 𝑄 ∈ DivRing ↔ ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) ) ) )

Proof

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