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