Metamath Proof Explorer


Theorem qsidomlem1

Description: If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024)

Ref Expression
Hypothesis qsidom.1 Q=R/𝑠R~QGI
Assertion qsidomlem1 Could not format assertion : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 qsidom.1 Q=R/𝑠R~QGI
2 crngring RCRingRRing
3 2 ad2antrr RCRingILIdealRQIDomnRRing
4 simplr RCRingILIdealRQIDomnILIdealR
5 simpr RCRingILIdealRQIDomnI=BaseRI=BaseR
6 5 oveq2d RCRingILIdealRQIDomnI=BaseRR~QGI=R~QGBaseR
7 6 oveq2d RCRingILIdealRQIDomnI=BaseRR/𝑠R~QGI=R/𝑠R~QGBaseR
8 1 7 eqtrid RCRingILIdealRQIDomnI=BaseRQ=R/𝑠R~QGBaseR
9 8 fveq2d RCRingILIdealRQIDomnI=BaseRBaseQ=BaseR/𝑠R~QGBaseR
10 ringgrp RRingRGrp
11 2 10 syl RCRingRGrp
12 11 ad3antrrr RCRingILIdealRQIDomnI=BaseRRGrp
13 eqid BaseR=BaseR
14 eqid R/𝑠R~QGBaseR=R/𝑠R~QGBaseR
15 13 14 qustriv RGrpBaseR/𝑠R~QGBaseR=BaseR
16 12 15 syl RCRingILIdealRQIDomnI=BaseRBaseR/𝑠R~QGBaseR=BaseR
17 9 16 eqtrd RCRingILIdealRQIDomnI=BaseRBaseQ=BaseR
18 17 fveq2d RCRingILIdealRQIDomnI=BaseRBaseQ=BaseR
19 fvex BaseRV
20 hashsng BaseRVBaseR=1
21 19 20 ax-mp BaseR=1
22 18 21 eqtrdi RCRingILIdealRQIDomnI=BaseRBaseQ=1
23 1red RCRingILIdealRQIDomnI=BaseR1
24 isidom QIDomnQCRingQDomn
25 24 simprbi QIDomnQDomn
26 domnnzr QDomnQNzRing
27 25 26 syl QIDomnQNzRing
28 27 ad2antlr RCRingILIdealRQIDomnI=BaseRQNzRing
29 eqid BaseQ=BaseQ
30 29 isnzr2hash QNzRingQRing1<BaseQ
31 30 simprbi QNzRing1<BaseQ
32 28 31 syl RCRingILIdealRQIDomnI=BaseR1<BaseQ
33 23 32 gtned RCRingILIdealRQIDomnI=BaseRBaseQ1
34 33 neneqd RCRingILIdealRQIDomnI=BaseR¬BaseQ=1
35 22 34 pm2.65da RCRingILIdealRQIDomn¬I=BaseR
36 35 neqned RCRingILIdealRQIDomnIBaseR
37 25 ad4antlr RCRingILIdealRQIDomnxBaseRyBaseRxRyIQDomn
38 ovex R~QGIV
39 38 ecelqsi xBaseRxR~QGIBaseR/R~QGI
40 39 ad3antlr RCRingILIdealRQIDomnxBaseRyBaseRxRyIxR~QGIBaseR/R~QGI
41 simp-5l RCRingILIdealRQIDomnxBaseRyBaseRxRyIRCRing
42 1 a1i RCRingQ=R/𝑠R~QGI
43 eqidd RCRingBaseR=BaseR
44 ovexd RCRingR~QGIV
45 id RCRingRCRing
46 42 43 44 45 qusbas RCRingBaseR/R~QGI=BaseQ
47 41 46 syl RCRingILIdealRQIDomnxBaseRyBaseRxRyIBaseR/R~QGI=BaseQ
48 40 47 eleqtrd RCRingILIdealRQIDomnxBaseRyBaseRxRyIxR~QGIBaseQ
49 38 ecelqsi yBaseRyR~QGIBaseR/R~QGI
50 49 ad2antlr RCRingILIdealRQIDomnxBaseRyBaseRxRyIyR~QGIBaseR/R~QGI
51 50 47 eleqtrd RCRingILIdealRQIDomnxBaseRyBaseRxRyIyR~QGIBaseQ
52 41 2 10 3syl RCRingILIdealRQIDomnxBaseRyBaseRxRyIRGrp
53 eqid LIdealR=LIdealR
54 53 lidlsubg RRingILIdealRISubGrpR
55 2 54 sylan RCRingILIdealRISubGrpR
56 55 ad4antr RCRingILIdealRQIDomnxBaseRyBaseRxRyIISubGrpR
57 simpr RCRingILIdealRQIDomnxBaseRyBaseRxRyIxRyI
58 eqid R~QGI=R~QGI
59 58 eqg0el RGrpISubGrpRxRyR~QGI=IxRyI
60 59 biimpar RGrpISubGrpRxRyIxRyR~QGI=I
61 52 56 57 60 syl21anc RCRingILIdealRQIDomnxBaseRyBaseRxRyIxRyR~QGI=I
62 1 a1i RCRingILIdealRQ=R/𝑠R~QGI
63 eqidd RCRingILIdealRBaseR=BaseR
64 13 58 eqger ISubGrpRR~QGIErBaseR
65 55 64 syl RCRingILIdealRR~QGIErBaseR
66 simpl RCRingILIdealRRCRing
67 53 crng2idl RCRingLIdealR=2IdealR
68 67 eleq2d RCRingILIdealRI2IdealR
69 68 biimpa RCRingILIdealRI2IdealR
70 eqid 2IdealR=2IdealR
71 eqid R=R
72 13 58 70 71 2idlcpbl RRingI2IdealRgR~QGIehR~QGIfgRhR~QGIeRf
73 2 69 72 syl2an2r RCRingILIdealRgR~QGIehR~QGIfgRhR~QGIeRf
74 2 ad2antrr RCRingILIdealReBaseRfBaseRRRing
75 simprl RCRingILIdealReBaseRfBaseReBaseR
76 simprr RCRingILIdealReBaseRfBaseRfBaseR
77 13 71 ringcl RRingeBaseRfBaseReRfBaseR
78 74 75 76 77 syl3anc RCRingILIdealReBaseRfBaseReRfBaseR
79 eqid Q=Q
80 62 63 65 66 73 78 71 79 qusmulval RCRingILIdealRxBaseRyBaseRxR~QGIQyR~QGI=xRyR~QGI
81 80 ad5ant134 RCRingILIdealRQIDomnxBaseRyBaseRxRyIxR~QGIQyR~QGI=xRyR~QGI
82 lidlnsg RRingILIdealRINrmSGrpR
83 2 82 sylan RCRingILIdealRINrmSGrpR
84 eqid 0R=0R
85 1 84 qus0 INrmSGrpR0RR~QGI=0Q
86 83 85 syl RCRingILIdealR0RR~QGI=0Q
87 13 58 84 eqgid ISubGrpR0RR~QGI=I
88 55 87 syl RCRingILIdealR0RR~QGI=I
89 86 88 eqtr3d RCRingILIdealR0Q=I
90 89 ad4antr RCRingILIdealRQIDomnxBaseRyBaseRxRyI0Q=I
91 61 81 90 3eqtr4d RCRingILIdealRQIDomnxBaseRyBaseRxRyIxR~QGIQyR~QGI=0Q
92 eqid 0Q=0Q
93 29 79 92 domneq0 QDomnxR~QGIBaseQyR~QGIBaseQxR~QGIQyR~QGI=0QxR~QGI=0QyR~QGI=0Q
94 93 biimpa QDomnxR~QGIBaseQyR~QGIBaseQxR~QGIQyR~QGI=0QxR~QGI=0QyR~QGI=0Q
95 37 48 51 91 94 syl31anc RCRingILIdealRQIDomnxBaseRyBaseRxRyIxR~QGI=0QyR~QGI=0Q
96 89 eqeq2d RCRingILIdealRxR~QGI=0QxR~QGI=I
97 66 2 10 3syl RCRingILIdealRRGrp
98 58 eqg0el RGrpISubGrpRxR~QGI=IxI
99 97 55 98 syl2anc RCRingILIdealRxR~QGI=IxI
100 96 99 bitrd RCRingILIdealRxR~QGI=0QxI
101 89 eqeq2d RCRingILIdealRyR~QGI=0QyR~QGI=I
102 58 eqg0el RGrpISubGrpRyR~QGI=IyI
103 97 55 102 syl2anc RCRingILIdealRyR~QGI=IyI
104 101 103 bitrd RCRingILIdealRyR~QGI=0QyI
105 100 104 orbi12d RCRingILIdealRxR~QGI=0QyR~QGI=0QxIyI
106 105 ad4antr RCRingILIdealRQIDomnxBaseRyBaseRxRyIxR~QGI=0QyR~QGI=0QxIyI
107 95 106 mpbid RCRingILIdealRQIDomnxBaseRyBaseRxRyIxIyI
108 107 ex RCRingILIdealRQIDomnxBaseRyBaseRxRyIxIyI
109 108 anasss RCRingILIdealRQIDomnxBaseRyBaseRxRyIxIyI
110 109 ralrimivva RCRingILIdealRQIDomnxBaseRyBaseRxRyIxIyI
111 13 71 prmidl2 Could not format ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ ( I =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) ) ) -> I e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ ( I =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) ) ) -> I e. ( PrmIdeal ` R ) ) with typecode |-
112 3 4 36 110 111 syl22anc Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) with typecode |-