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 /s ( R ~QG I ) )
Assertion qsidomlem1 
|- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) )

Proof

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