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 ~ QG I
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 ~ QG I
2 crngring R CRing R Ring
3 2 ad2antrr R CRing I LIdeal R Q IDomn R Ring
4 simplr R CRing I LIdeal R Q IDomn I LIdeal R
5 simpr R CRing I LIdeal R Q IDomn I = Base R I = Base R
6 5 oveq2d R CRing I LIdeal R Q IDomn I = Base R R ~ QG I = R ~ QG Base R
7 6 oveq2d R CRing I LIdeal R Q IDomn I = Base R R / 𝑠 R ~ QG I = R / 𝑠 R ~ QG Base R
8 1 7 syl5eq R CRing I LIdeal R Q IDomn I = Base R Q = R / 𝑠 R ~ QG Base R
9 8 fveq2d R CRing I LIdeal R Q IDomn I = Base R Base Q = Base R / 𝑠 R ~ QG Base R
10 ringgrp R Ring R Grp
11 2 10 syl R CRing R Grp
12 11 ad3antrrr R CRing I LIdeal R Q IDomn I = Base R R Grp
13 eqid Base R = Base R
14 eqid R / 𝑠 R ~ QG Base R = R / 𝑠 R ~ QG Base R
15 13 14 qustriv R Grp Base R / 𝑠 R ~ QG Base R = Base R
16 12 15 syl R CRing I LIdeal R Q IDomn I = Base R Base R / 𝑠 R ~ QG Base R = Base R
17 9 16 eqtrd R CRing I LIdeal R Q IDomn I = Base R Base Q = Base R
18 17 fveq2d R CRing I LIdeal R Q IDomn I = Base R Base Q = Base R
19 fvex Base R V
20 hashsng Base R V Base R = 1
21 19 20 ax-mp Base R = 1
22 18 21 eqtrdi R CRing I LIdeal R Q IDomn I = Base R Base Q = 1
23 1red R CRing I LIdeal R Q IDomn I = Base R 1
24 isidom Q IDomn Q CRing Q Domn
25 24 simprbi Q IDomn Q Domn
26 domnnzr Q Domn Q NzRing
27 25 26 syl Q IDomn Q NzRing
28 27 ad2antlr R CRing I LIdeal R Q IDomn I = Base R Q NzRing
29 eqid Base Q = Base Q
30 29 isnzr2hash Q NzRing Q Ring 1 < Base Q
31 30 simprbi Q NzRing 1 < Base Q
32 28 31 syl R CRing I LIdeal R Q IDomn I = Base R 1 < Base Q
33 23 32 gtned R CRing I LIdeal R Q IDomn I = Base R Base Q 1
34 33 neneqd R CRing I LIdeal R Q IDomn I = Base R ¬ Base Q = 1
35 22 34 pm2.65da R CRing I LIdeal R Q IDomn ¬ I = Base R
36 35 neqned R CRing I LIdeal R Q IDomn I Base R
37 25 ad4antlr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I Q Domn
38 ovex R ~ QG I V
39 38 ecelqsi x Base R x R ~ QG I Base R / R ~ QG I
40 39 ad3antlr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R ~ QG I Base R / R ~ QG I
41 simp-5l R CRing I LIdeal R Q IDomn x Base R y Base R x R y I R CRing
42 1 a1i R CRing Q = R / 𝑠 R ~ QG I
43 eqidd R CRing Base R = Base R
44 ovexd R CRing R ~ QG I V
45 id R CRing R CRing
46 42 43 44 45 qusbas R CRing Base R / R ~ QG I = Base Q
47 41 46 syl R CRing I LIdeal R Q IDomn x Base R y Base R x R y I Base R / R ~ QG I = Base Q
48 40 47 eleqtrd R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R ~ QG I Base Q
49 38 ecelqsi y Base R y R ~ QG I Base R / R ~ QG I
50 49 ad2antlr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I y R ~ QG I Base R / R ~ QG I
51 50 47 eleqtrd R CRing I LIdeal R Q IDomn x Base R y Base R x R y I y R ~ QG I Base Q
52 41 2 10 3syl R CRing I LIdeal R Q IDomn x Base R y Base R x R y I R Grp
53 eqid LIdeal R = LIdeal R
54 53 lidlsubg R Ring I LIdeal R I SubGrp R
55 2 54 sylan R CRing I LIdeal R I SubGrp R
56 55 ad4antr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I I SubGrp R
57 simpr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R y I
58 eqid R ~ QG I = R ~ QG I
59 58 eqg0el R Grp I SubGrp R x R y R ~ QG I = I x R y I
60 59 biimpar R Grp I SubGrp R x R y I x R y R ~ QG I = I
61 52 56 57 60 syl21anc R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R y R ~ QG I = I
62 1 a1i R CRing I LIdeal R Q = R / 𝑠 R ~ QG I
63 eqidd R CRing I LIdeal R Base R = Base R
64 13 58 eqger I SubGrp R R ~ QG I Er Base R
65 55 64 syl R CRing I LIdeal R R ~ QG I Er Base R
66 simpl R CRing I LIdeal R R CRing
67 53 crng2idl R CRing LIdeal R = 2Ideal R
68 67 eleq2d R CRing I LIdeal R I 2Ideal R
69 68 biimpa R CRing I LIdeal R I 2Ideal R
70 eqid 2Ideal R = 2Ideal R
71 eqid R = R
72 13 58 70 71 2idlcpbl R Ring I 2Ideal R g R ~ QG I e h R ~ QG I f g R h R ~ QG I e R f
73 2 69 72 syl2an2r R CRing I LIdeal R g R ~ QG I e h R ~ QG I f g R h R ~ QG I e R f
74 2 ad2antrr R CRing I LIdeal R e Base R f Base R R Ring
75 simprl R CRing I LIdeal R e Base R f Base R e Base R
76 simprr R CRing I LIdeal R e Base R f Base R f Base R
77 13 71 ringcl R Ring e Base R f Base R e R f Base R
78 74 75 76 77 syl3anc R CRing I LIdeal R e Base R f Base R e R f Base R
79 eqid Q = Q
80 62 63 65 66 73 78 71 79 qusmulval R CRing I LIdeal R x Base R y Base R x R ~ QG I Q y R ~ QG I = x R y R ~ QG I
81 80 ad5ant134 R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R ~ QG I Q y R ~ QG I = x R y R ~ QG I
82 lidlnsg R Ring I LIdeal R I NrmSGrp R
83 2 82 sylan R CRing I LIdeal R I NrmSGrp R
84 eqid 0 R = 0 R
85 1 84 qus0 I NrmSGrp R 0 R R ~ QG I = 0 Q
86 83 85 syl R CRing I LIdeal R 0 R R ~ QG I = 0 Q
87 13 58 84 eqgid I SubGrp R 0 R R ~ QG I = I
88 55 87 syl R CRing I LIdeal R 0 R R ~ QG I = I
89 86 88 eqtr3d R CRing I LIdeal R 0 Q = I
90 89 ad4antr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I 0 Q = I
91 61 81 90 3eqtr4d R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R ~ QG I Q y R ~ QG I = 0 Q
92 eqid 0 Q = 0 Q
93 29 79 92 domneq0 Q Domn x R ~ QG I Base Q y R ~ QG I Base Q x R ~ QG I Q y R ~ QG I = 0 Q x R ~ QG I = 0 Q y R ~ QG I = 0 Q
94 93 biimpa Q Domn x R ~ QG I Base Q y R ~ QG I Base Q x R ~ QG I Q y R ~ QG I = 0 Q x R ~ QG I = 0 Q y R ~ QG I = 0 Q
95 37 48 51 91 94 syl31anc R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R ~ QG I = 0 Q y R ~ QG I = 0 Q
96 89 eqeq2d R CRing I LIdeal R x R ~ QG I = 0 Q x R ~ QG I = I
97 66 2 10 3syl R CRing I LIdeal R R Grp
98 58 eqg0el R Grp I SubGrp R x R ~ QG I = I x I
99 97 55 98 syl2anc R CRing I LIdeal R x R ~ QG I = I x I
100 96 99 bitrd R CRing I LIdeal R x R ~ QG I = 0 Q x I
101 89 eqeq2d R CRing I LIdeal R y R ~ QG I = 0 Q y R ~ QG I = I
102 58 eqg0el R Grp I SubGrp R y R ~ QG I = I y I
103 97 55 102 syl2anc R CRing I LIdeal R y R ~ QG I = I y I
104 101 103 bitrd R CRing I LIdeal R y R ~ QG I = 0 Q y I
105 100 104 orbi12d R CRing I LIdeal R x R ~ QG I = 0 Q y R ~ QG I = 0 Q x I y I
106 105 ad4antr R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x R ~ QG I = 0 Q y R ~ QG I = 0 Q x I y I
107 95 106 mpbid R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x I y I
108 107 ex R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x I y I
109 108 anasss R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x I y I
110 109 ralrimivva R CRing I LIdeal R Q IDomn x Base R y Base R x R y I x I y I
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 |-