Metamath Proof Explorer

Theorem qsdrngilem

Description: Lemma for qsdrngi . (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses qsdrng.0 
|- O = ( oppR ` R )
qsdrng.q 
|- Q = ( R /s ( R ~QG M ) )
qsdrng.r 
|- ( ph -> R e. NzRing )
qsdrngi.1 
|- ( ph -> M e. ( MaxIdeal ` R ) )
qsdrngi.2 
|- ( ph -> M e. ( MaxIdeal ` O ) )
qsdrngilem.1 
|- ( ph -> X e. ( Base ` R ) )
qsdrngilem.2 
|- ( ph -> -. X e. M )
Assertion qsdrngilem 
|- ( ph -> E. v e. ( Base ` Q ) ( v ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) )

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 qsdrngi.1 
 |-  ( ph -> M e. ( MaxIdeal ` R ) )
5 qsdrngi.2 
 |-  ( ph -> M e. ( MaxIdeal ` O ) )
6 qsdrngilem.1 
 |-  ( ph -> X e. ( Base ` R ) )
7 qsdrngilem.2 
 |-  ( ph -> -. X e. M )
8 simpllr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> r e. ( Base ` R ) )
9 ovex 
 |-  ( R ~QG M ) e. _V
10 9 ecelqsi 
 |-  ( r e. ( Base ` R ) -> [ r ] ( R ~QG M ) e. ( ( Base ` R ) /. ( R ~QG M ) ) )
11 8 10 syl 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> [ r ] ( R ~QG M ) e. ( ( Base ` R ) /. ( R ~QG M ) ) )
12 2 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG M ) ) )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 13 a1i 
 |-  ( ph -> ( Base ` R ) = ( Base ` R ) )
15 ovexd 
 |-  ( ph -> ( R ~QG M ) e. _V )
16 12 14 15 3 qusbas 
 |-  ( ph -> ( ( Base ` R ) /. ( R ~QG M ) ) = ( Base ` Q ) )
17 16 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( Base ` R ) /. ( R ~QG M ) ) = ( Base ` Q ) )
18 11 17 eleqtrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> [ r ] ( R ~QG M ) e. ( Base ` Q ) )
19 oveq1 
 |-  ( v = [ r ] ( R ~QG M ) -> ( v ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( [ r ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) )
20 19 eqeq1d 
 |-  ( v = [ r ] ( R ~QG M ) -> ( ( v ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) <-> ( [ r ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) ) )
21 20 adantl 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) /\ v = [ r ] ( R ~QG M ) ) -> ( ( v ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) <-> ( [ r ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) ) )
22 eqid 
 |-  ( .r ` R ) = ( .r ` R )
23 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
24 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
25 3 24 syl 
 |-  ( ph -> R e. Ring )
26 25 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> R e. Ring )
27 13 mxidlidl 
 |-  ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) )
28 25 4 27 syl2anc 
 |-  ( ph -> M e. ( LIdeal ` R ) )
29 1 opprring 
 |-  ( R e. Ring -> O e. Ring )
30 25 29 syl 
 |-  ( ph -> O e. Ring )
31 eqid 
 |-  ( Base ` O ) = ( Base ` O )
32 31 mxidlidl 
 |-  ( ( O e. Ring /\ M e. ( MaxIdeal ` O ) ) -> M e. ( LIdeal ` O ) )
33 30 5 32 syl2anc 
 |-  ( ph -> M e. ( LIdeal ` O ) )
34 28 33 elind 
 |-  ( ph -> M e. ( ( LIdeal ` R ) i^i ( LIdeal ` O ) ) )
35 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
36 eqid 
 |-  ( LIdeal ` O ) = ( LIdeal ` O )
37 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
38 35 1 36 37 2idlval 
 |-  ( 2Ideal ` R ) = ( ( LIdeal ` R ) i^i ( LIdeal ` O ) )
39 34 38 eleqtrrdi 
 |-  ( ph -> M e. ( 2Ideal ` R ) )
40 39 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> M e. ( 2Ideal ` R ) )
41 6 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> X e. ( Base ` R ) )
42 2 13 22 23 26 40 8 41 qusmul2 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( [ r ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = [ ( r ( .r ` R ) X ) ] ( R ~QG M ) )
43 lidlnsg 
 |-  ( ( R e. Ring /\ M e. ( LIdeal ` R ) ) -> M e. ( NrmSGrp ` R ) )
44 25 28 43 syl2anc 
 |-  ( ph -> M e. ( NrmSGrp ` R ) )
45 nsgsubg 
 |-  ( M e. ( NrmSGrp ` R ) -> M e. ( SubGrp ` R ) )
46 eqid 
 |-  ( R ~QG M ) = ( R ~QG M )
47 13 46 eqger 
 |-  ( M e. ( SubGrp ` R ) -> ( R ~QG M ) Er ( Base ` R ) )
48 44 45 47 3syl 
 |-  ( ph -> ( R ~QG M ) Er ( Base ` R ) )
49 48 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( R ~QG M ) Er ( Base ` R ) )
50 13 35 lidlss 
 |-  ( M e. ( LIdeal ` R ) -> M C_ ( Base ` R ) )
51 28 50 syl 
 |-  ( ph -> M C_ ( Base ` R ) )
52 51 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> M C_ ( Base ` R ) )
53 13 22 26 8 41 ringcld 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( r ( .r ` R ) X ) e. ( Base ` R ) )
54 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
55 13 54 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
56 25 55 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
57 56 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( 1r ` R ) e. ( Base ` R ) )
58 simpr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) )
59 58 oveq2d 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) = ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) )
60 eqid 
 |-  ( +g ` R ) = ( +g ` R )
61 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
62 eqid 
 |-  ( invg ` R ) = ( invg ` R )
63 25 ringgrpd 
 |-  ( ph -> R e. Grp )
64 63 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> R e. Grp )
65 13 60 61 62 64 53 grplinvd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( r ( .r ` R ) X ) ) = ( 0g ` R ) )
66 65 oveq1d 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( r ( .r ` R ) X ) ) ( +g ` R ) m ) = ( ( 0g ` R ) ( +g ` R ) m ) )
67 13 62 64 53 grpinvcld 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) e. ( Base ` R ) )
68 simplr 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> m e. M )
69 52 68 sseldd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> m e. ( Base ` R ) )
70 13 60 64 67 53 69 grpassd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( r ( .r ` R ) X ) ) ( +g ` R ) m ) = ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) )
71 13 60 61 64 69 grplidd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( 0g ` R ) ( +g ` R ) m ) = m )
72 66 70 71 3eqtr3d 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) = m )
73 59 72 eqtrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) = m )
74 73 68 eqeltrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M )
75 13 62 60 46 eqgval 
 |-  ( ( R e. Ring /\ M C_ ( Base ` R ) ) -> ( ( r ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) <-> ( ( r ( .r ` R ) X ) e. ( Base ` R ) /\ ( 1r ` R ) e. ( Base ` R ) /\ ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M ) ) )
76 75 biimpar 
 |-  ( ( ( R e. Ring /\ M C_ ( Base ` R ) ) /\ ( ( r ( .r ` R ) X ) e. ( Base ` R ) /\ ( 1r ` R ) e. ( Base ` R ) /\ ( ( ( invg ` R ) ` ( r ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M ) ) -> ( r ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) )
77 26 52 53 57 74 76 syl23anc 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( r ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) )
78 49 77 erthi 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> [ ( r ( .r ` R ) X ) ] ( R ~QG M ) = [ ( 1r ` R ) ] ( R ~QG M ) )
79 42 78 eqtrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( [ r ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = [ ( 1r ` R ) ] ( R ~QG M ) )
80 2 37 54 qus1 
 |-  ( ( R e. Ring /\ M e. ( 2Ideal ` R ) ) -> ( Q e. Ring /\ [ ( 1r ` R ) ] ( R ~QG M ) = ( 1r ` Q ) ) )
81 80 simprd 
 |-  ( ( R e. Ring /\ M e. ( 2Ideal ` R ) ) -> [ ( 1r ` R ) ] ( R ~QG M ) = ( 1r ` Q ) )
82 26 40 81 syl2anc 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> [ ( 1r ` R ) ] ( R ~QG M ) = ( 1r ` Q ) )
83 79 82 eqtrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> ( [ r ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) )
84 18 21 83 rspcedvd 
 |-  ( ( ( ( ph /\ r e. ( Base ` R ) ) /\ m e. M ) /\ ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) -> E. v e. ( Base ` Q ) ( v ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) )
85 6 snssd 
 |-  ( ph -> { X } C_ ( Base ` R ) )
86 51 85 unssd 
 |-  ( ph -> ( M u. { X } ) C_ ( Base ` R ) )
87 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
88 87 13 35 rspcl 
 |-  ( ( R e. Ring /\ ( M u. { X } ) C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` ( M u. { X } ) ) e. ( LIdeal ` R ) )
89 25 86 88 syl2anc 
 |-  ( ph -> ( ( RSpan ` R ) ` ( M u. { X } ) ) e. ( LIdeal ` R ) )
90 87 13 rspssid 
 |-  ( ( R e. Ring /\ ( M u. { X } ) C_ ( Base ` R ) ) -> ( M u. { X } ) C_ ( ( RSpan ` R ) ` ( M u. { X } ) ) )
91 25 86 90 syl2anc 
 |-  ( ph -> ( M u. { X } ) C_ ( ( RSpan ` R ) ` ( M u. { X } ) ) )
92 91 unssad 
 |-  ( ph -> M C_ ( ( RSpan ` R ) ` ( M u. { X } ) ) )
93 91 unssbd 
 |-  ( ph -> { X } C_ ( ( RSpan ` R ) ` ( M u. { X } ) ) )
94 snssg 
 |-  ( X e. ( Base ` R ) -> ( X e. ( ( RSpan ` R ) ` ( M u. { X } ) ) <-> { X } C_ ( ( RSpan ` R ) ` ( M u. { X } ) ) ) )
95 94 biimpar 
 |-  ( ( X e. ( Base ` R ) /\ { X } C_ ( ( RSpan ` R ) ` ( M u. { X } ) ) ) -> X e. ( ( RSpan ` R ) ` ( M u. { X } ) ) )
96 6 93 95 syl2anc 
 |-  ( ph -> X e. ( ( RSpan ` R ) ` ( M u. { X } ) ) )
97 96 7 eldifd 
 |-  ( ph -> X e. ( ( ( RSpan ` R ) ` ( M u. { X } ) ) \ M ) )
98 13 25 4 89 92 97 mxidlmaxv 
 |-  ( ph -> ( ( RSpan ` R ) ` ( M u. { X } ) ) = ( Base ` R ) )
99 56 98 eleqtrrd 
 |-  ( ph -> ( 1r ` R ) e. ( ( RSpan ` R ) ` ( M u. { X } ) ) )
100 6 7 eldifd 
 |-  ( ph -> X e. ( ( Base ` R ) \ M ) )
101 87 13 61 22 25 60 28 100 elrspunsn 
 |-  ( ph -> ( ( 1r ` R ) e. ( ( RSpan ` R ) ` ( M u. { X } ) ) <-> E. r e. ( Base ` R ) E. m e. M ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) ) )
102 99 101 mpbid 
 |-  ( ph -> E. r e. ( Base ` R ) E. m e. M ( 1r ` R ) = ( ( r ( .r ` R ) X ) ( +g ` R ) m ) )
103 84 102 r19.29vva 
 |-  ( ph -> E. v e. ( Base ` Q ) ( v ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) )