Metamath Proof Explorer

Theorem qsdrnglem2

Description: Lemma for qsdrng . (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 ) )
qsdrnglem2.1 
|- B = ( Base ` R )
qsdrnglem2.q 
|- ( ph -> Q e. DivRing )
qsdrnglem2.j 
|- ( ph -> J e. ( LIdeal ` R ) )
qsdrnglem2.m 
|- ( ph -> M C_ J )
qsdrnglem2.x 
|- ( ph -> X e. ( J \ M ) )
Assertion qsdrnglem2 
|- ( ph -> J = B )

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 qsdrnglem2.1 
 |-  B = ( Base ` R )
6 qsdrnglem2.q 
 |-  ( ph -> Q e. DivRing )
7 qsdrnglem2.j 
 |-  ( ph -> J e. ( LIdeal ` R ) )
8 qsdrnglem2.m 
 |-  ( ph -> M C_ J )
9 qsdrnglem2.x 
 |-  ( ph -> X e. ( J \ M ) )
10 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
11 3 10 syl 
 |-  ( ph -> R e. Ring )
12 11 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> R e. Ring )
13 7 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> J e. ( LIdeal ` R ) )
14 12 ringgrpd 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> R e. Grp )
15 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
16 5 15 lidlss 
 |-  ( J e. ( LIdeal ` R ) -> J C_ B )
17 13 16 syl 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> J C_ B )
18 simplr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> s e. B )
19 9 eldifad 
 |-  ( ph -> X e. J )
20 19 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> X e. J )
21 eqid 
 |-  ( .r ` R ) = ( .r ` R )
22 15 5 21 lidlmcl 
 |-  ( ( ( R e. Ring /\ J e. ( LIdeal ` R ) ) /\ ( s e. B /\ X e. J ) ) -> ( s ( .r ` R ) X ) e. J )
23 12 13 18 20 22 syl22anc 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( s ( .r ` R ) X ) e. J )
24 17 23 sseldd 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( s ( .r ` R ) X ) e. B )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 5 25 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
27 12 26 syl 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( 1r ` R ) e. B )
28 eqid 
 |-  ( +g ` R ) = ( +g ` R )
29 eqid 
 |-  ( invg ` R ) = ( invg ` R )
30 5 28 29 grpasscan1 
 |-  ( ( R e. Grp /\ ( s ( .r ` R ) X ) e. B /\ ( 1r ` R ) e. B ) -> ( ( s ( .r ` R ) X ) ( +g ` R ) ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) ) = ( 1r ` R ) )
31 14 24 27 30 syl3anc 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( s ( .r ` R ) X ) ( +g ` R ) ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) ) = ( 1r ` R ) )
32 8 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> M C_ J )
33 7 16 syl 
 |-  ( ph -> J C_ B )
34 8 33 sstrd 
 |-  ( ph -> M C_ B )
35 34 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> M C_ B )
36 simpr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) )
37 36 oveq1d 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( [ s ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) )
38 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
39 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
40 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
41 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
42 eqid 
 |-  ( invr ` Q ) = ( invr ` Q )
43 6 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> Q e. DivRing )
44 33 19 sseldd 
 |-  ( ph -> X e. B )
45 ovex 
 |-  ( R ~QG M ) e. _V
46 45 ecelqsi 
 |-  ( X e. B -> [ X ] ( R ~QG M ) e. ( B /. ( R ~QG M ) ) )
47 44 46 syl 
 |-  ( ph -> [ X ] ( R ~QG M ) e. ( B /. ( R ~QG M ) ) )
48 2 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG M ) ) )
49 5 a1i 
 |-  ( ph -> B = ( Base ` R ) )
50 45 a1i 
 |-  ( ph -> ( R ~QG M ) e. _V )
51 48 49 50 3 qusbas 
 |-  ( ph -> ( B /. ( R ~QG M ) ) = ( Base ` Q ) )
52 47 51 eleqtrd 
 |-  ( ph -> [ X ] ( R ~QG M ) e. ( Base ` Q ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> [ X ] ( R ~QG M ) e. ( Base ` Q ) )
54 4 2idllidld 
 |-  ( ph -> M e. ( LIdeal ` R ) )
55 15 lidlsubg 
 |-  ( ( R e. Ring /\ M e. ( LIdeal ` R ) ) -> M e. ( SubGrp ` R ) )
56 11 54 55 syl2anc 
 |-  ( ph -> M e. ( SubGrp ` R ) )
57 eqid 
 |-  ( R ~QG M ) = ( R ~QG M )
58 5 57 eqger 
 |-  ( M e. ( SubGrp ` R ) -> ( R ~QG M ) Er B )
59 56 58 syl 
 |-  ( ph -> ( R ~QG M ) Er B )
60 ecref 
 |-  ( ( ( R ~QG M ) Er B /\ X e. B ) -> X e. [ X ] ( R ~QG M ) )
61 59 44 60 syl2anc 
 |-  ( ph -> X e. [ X ] ( R ~QG M ) )
62 9 eldifbd 
 |-  ( ph -> -. X e. M )
63 nelne1 
 |-  ( ( X e. [ X ] ( R ~QG M ) /\ -. X e. M ) -> [ X ] ( R ~QG M ) =/= M )
64 61 62 63 syl2anc 
 |-  ( ph -> [ X ] ( R ~QG M ) =/= M )
65 lidlnsg 
 |-  ( ( R e. Ring /\ M e. ( LIdeal ` R ) ) -> M e. ( NrmSGrp ` R ) )
66 11 54 65 syl2anc 
 |-  ( ph -> M e. ( NrmSGrp ` R ) )
67 2 qus0g 
 |-  ( M e. ( NrmSGrp ` R ) -> ( 0g ` Q ) = M )
68 66 67 syl 
 |-  ( ph -> ( 0g ` Q ) = M )
69 64 68 neeqtrrd 
 |-  ( ph -> [ X ] ( R ~QG M ) =/= ( 0g ` Q ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> [ X ] ( R ~QG M ) =/= ( 0g ` Q ) )
71 38 39 40 41 42 43 53 70 drnginvrld 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = ( 1r ` Q ) )
72 4 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> M e. ( 2Ideal ` R ) )
73 44 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> X e. B )
74 2 5 21 40 12 72 18 73 qusmul2 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( [ s ] ( R ~QG M ) ( .r ` Q ) [ X ] ( R ~QG M ) ) = [ ( s ( .r ` R ) X ) ] ( R ~QG M ) )
75 37 71 74 3eqtr3rd 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> [ ( s ( .r ` R ) X ) ] ( R ~QG M ) = ( 1r ` Q ) )
76 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
77 2 76 25 qus1 
 |-  ( ( R e. Ring /\ M e. ( 2Ideal ` R ) ) -> ( Q e. Ring /\ [ ( 1r ` R ) ] ( R ~QG M ) = ( 1r ` Q ) ) )
78 77 simprd 
 |-  ( ( R e. Ring /\ M e. ( 2Ideal ` R ) ) -> [ ( 1r ` R ) ] ( R ~QG M ) = ( 1r ` Q ) )
79 12 72 78 syl2anc 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> [ ( 1r ` R ) ] ( R ~QG M ) = ( 1r ` Q ) )
80 75 79 eqtr4d 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> [ ( s ( .r ` R ) X ) ] ( R ~QG M ) = [ ( 1r ` R ) ] ( R ~QG M ) )
81 56 ad2antrr 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> M e. ( SubGrp ` R ) )
82 81 58 syl 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( R ~QG M ) Er B )
83 82 27 erth2 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( s ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) <-> [ ( s ( .r ` R ) X ) ] ( R ~QG M ) = [ ( 1r ` R ) ] ( R ~QG M ) ) )
84 80 83 mpbird 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( s ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) )
85 5 29 28 57 eqgval 
 |-  ( ( R e. Ring /\ M C_ B ) -> ( ( s ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) <-> ( ( s ( .r ` R ) X ) e. B /\ ( 1r ` R ) e. B /\ ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M ) ) )
86 85 biimpa 
 |-  ( ( ( R e. Ring /\ M C_ B ) /\ ( s ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) ) -> ( ( s ( .r ` R ) X ) e. B /\ ( 1r ` R ) e. B /\ ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M ) )
87 86 simp3d 
 |-  ( ( ( R e. Ring /\ M C_ B ) /\ ( s ( .r ` R ) X ) ( R ~QG M ) ( 1r ` R ) ) -> ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M )
88 12 35 84 87 syl21anc 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. M )
89 32 88 sseldd 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. J )
90 15 28 lidlacl 
 |-  ( ( ( R e. Ring /\ J e. ( LIdeal ` R ) ) /\ ( ( s ( .r ` R ) X ) e. J /\ ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) e. J ) ) -> ( ( s ( .r ` R ) X ) ( +g ` R ) ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) ) e. J )
91 12 13 23 89 90 syl22anc 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( ( s ( .r ` R ) X ) ( +g ` R ) ( ( ( invg ` R ) ` ( s ( .r ` R ) X ) ) ( +g ` R ) ( 1r ` R ) ) ) e. J )
92 31 91 eqeltrrd 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> ( 1r ` R ) e. J )
93 15 5 25 lidl1el 
 |-  ( ( R e. Ring /\ J e. ( LIdeal ` R ) ) -> ( ( 1r ` R ) e. J <-> J = B ) )
94 93 biimpa 
 |-  ( ( ( R e. Ring /\ J e. ( LIdeal ` R ) ) /\ ( 1r ` R ) e. J ) -> J = B )
95 12 13 92 94 syl21anc 
 |-  ( ( ( ph /\ s e. B ) /\ ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) ) -> J = B )
96 38 39 42 6 52 69 drnginvrcld 
 |-  ( ph -> ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) e. ( Base ` Q ) )
97 96 51 eleqtrrd 
 |-  ( ph -> ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) e. ( B /. ( R ~QG M ) ) )
98 elqsi 
 |-  ( ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) e. ( B /. ( R ~QG M ) ) -> E. s e. B ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) )
99 97 98 syl 
 |-  ( ph -> E. s e. B ( ( invr ` Q ) ` [ X ] ( R ~QG M ) ) = [ s ] ( R ~QG M ) )
100 95 99 r19.29a 
 |-  ( ph -> J = B )