Metamath Proof Explorer

Theorem qsidomlem2

Description: A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024)

Ref Expression
Hypothesis qsidom.1 
|- Q = ( R /s ( R ~QG I ) )
Assertion qsidomlem2 
|- ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn )

Proof

Step Hyp Ref Expression
1 qsidom.1 
 |-  Q = ( R /s ( R ~QG I ) )
2 crngring 
 |-  ( R e. CRing -> R e. Ring )
3 prmidlidl 
 |-  ( ( R e. Ring /\ I e. ( PrmIdeal ` R ) ) -> I e. ( LIdeal ` R ) )
4 2 3 sylan 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> I e. ( LIdeal ` R ) )
5 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
6 1 5 quscrng 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> Q e. CRing )
7 4 6 syldan 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. CRing )
8 5 crng2idl 
 |-  ( R e. CRing -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
9 8 eleq2d 
 |-  ( R e. CRing -> ( I e. ( LIdeal ` R ) <-> I e. ( 2Ideal ` R ) ) )
10 9 biimpa 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> I e. ( 2Ideal ` R ) )
11 4 10 syldan 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> I e. ( 2Ideal ` R ) )
12 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
13 1 12 qusring 
 |-  ( ( R e. Ring /\ I e. ( 2Ideal ` R ) ) -> Q e. Ring )
14 2 11 13 syl2an2r 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. Ring )
15 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
16 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
17 15 16 ring0cl 
 |-  ( Q e. Ring -> ( 0g ` Q ) e. ( Base ` Q ) )
18 14 17 syl 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> ( 0g ` Q ) e. ( Base ` Q ) )
19 18 snssd 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> { ( 0g ` Q ) } C_ ( Base ` Q ) )
20 lidlnsg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( NrmSGrp ` R ) )
21 2 20 sylan 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> I e. ( NrmSGrp ` R ) )
22 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
23 1 22 qus0 
 |-  ( I e. ( NrmSGrp ` R ) -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
24 21 23 syl 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
25 5 lidlsubg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
26 2 25 sylan 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
27 eqid 
 |-  ( Base ` R ) = ( Base ` R )
28 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
29 27 28 22 eqgid 
 |-  ( I e. ( SubGrp ` R ) -> [ ( 0g ` R ) ] ( R ~QG I ) = I )
30 26 29 syl 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> [ ( 0g ` R ) ] ( R ~QG I ) = I )
31 24 30 eqtr3d 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( 0g ` Q ) = I )
32 4 31 syldan 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> ( 0g ` Q ) = I )
33 32 sneqd 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> { ( 0g ` Q ) } = { I } )
34 eqid 
 |-  ( .r ` R ) = ( .r ` R )
35 27 34 isprmidlc 
 |-  ( R e. CRing -> ( I e. ( PrmIdeal ` R ) <-> ( 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 ) ) ) ) )
36 35 biimpa 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> ( 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 ) ) ) )
37 36 simp2d 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> I =/= ( Base ` R ) )
38 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
39 2 38 syl 
 |-  ( R e. CRing -> R e. Grp )
40 39 ad2antrr 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( Base ` Q ) = { I } ) -> R e. Grp )
41 2 ad2antrr 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( Base ` Q ) = { I } ) -> R e. Ring )
42 4 adantr 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( Base ` Q ) = { I } ) -> I e. ( LIdeal ` R ) )
43 41 42 25 syl2anc 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( Base ` Q ) = { I } ) -> I e. ( SubGrp ` R ) )
44 simpr 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( Base ` Q ) = { I } ) -> ( Base ` Q ) = { I } )
45 27 1 qustrivr 
 |-  ( ( R e. Grp /\ I e. ( SubGrp ` R ) /\ ( Base ` Q ) = { I } ) -> I = ( Base ` R ) )
46 40 43 44 45 syl3anc 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( Base ` Q ) = { I } ) -> I = ( Base ` R ) )
47 37 46 mteqand 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> ( Base ` Q ) =/= { I } )
48 47 necomd 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> { I } =/= ( Base ` Q ) )
49 33 48 eqnetrd 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> { ( 0g ` Q ) } =/= ( Base ` Q ) )
50 pssdifn0 
 |-  ( ( { ( 0g ` Q ) } C_ ( Base ` Q ) /\ { ( 0g ` Q ) } =/= ( Base ` Q ) ) -> ( ( Base ` Q ) \ { ( 0g ` Q ) } ) =/= (/) )
51 19 49 50 syl2anc 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> ( ( Base ` Q ) \ { ( 0g ` Q ) } ) =/= (/) )
52 n0 
 |-  ( ( ( Base ` Q ) \ { ( 0g ` Q ) } ) =/= (/) <-> E. x x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) )
53 51 52 sylib 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> E. x x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) )
54 16 15 ringelnzr 
 |-  ( ( Q e. Ring /\ x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) -> Q e. NzRing )
55 54 ex 
 |-  ( Q e. Ring -> ( x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) -> Q e. NzRing ) )
56 55 exlimdv 
 |-  ( Q e. Ring -> ( E. x x e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) -> Q e. NzRing ) )
57 14 53 56 sylc 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. NzRing )
58 36 simp3d 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) )
59 58 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) )
60 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> x e. ( Base ` R ) )
61 simplr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> y e. ( Base ` R ) )
62 simp-8l 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> R e. CRing )
63 62 39 syl 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> R e. Grp )
64 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> I e. ( LIdeal ` R ) )
65 62 64 26 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> I e. ( SubGrp ` R ) )
66 1 a1i 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> Q = ( R /s ( R ~QG I ) ) )
67 eqidd 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Base ` R ) = ( Base ` R ) )
68 27 28 eqger 
 |-  ( I e. ( SubGrp ` R ) -> ( R ~QG I ) Er ( Base ` R ) )
69 26 68 syl 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( R ~QG I ) Er ( Base ` R ) )
70 simpl 
 |-  ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> R e. CRing )
71 27 28 12 34 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 ) ) )
72 2 10 71 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 ) ) )
73 2 ad2antrr 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( e e. ( Base ` R ) /\ f e. ( Base ` R ) ) ) -> R e. Ring )
74 simprl 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( e e. ( Base ` R ) /\ f e. ( Base ` R ) ) ) -> e e. ( Base ` R ) )
75 simprr 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( e e. ( Base ` R ) /\ f e. ( Base ` R ) ) ) -> f e. ( Base ` R ) )
76 27 34 ringcl 
 |-  ( ( R e. Ring /\ e e. ( Base ` R ) /\ f e. ( Base ` R ) ) -> ( e ( .r ` R ) f ) e. ( Base ` R ) )
77 73 74 75 76 syl3anc 
 |-  ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ ( e e. ( Base ` R ) /\ f e. ( Base ` R ) ) ) -> ( e ( .r ` R ) f ) e. ( Base ` R ) )
78 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
79 66 67 69 70 72 77 34 78 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 ) )
80 62 64 60 61 79 syl211anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( [ x ] ( R ~QG I ) ( .r ` Q ) [ y ] ( R ~QG I ) ) = [ ( x ( .r ` R ) y ) ] ( R ~QG I ) )
81 simpr 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> ( a ( .r ` Q ) b ) = ( 0g ` Q ) )
82 81 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( a ( .r ` Q ) b ) = ( 0g ` Q ) )
83 simpllr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> a = [ x ] ( R ~QG I ) )
84 simpr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> b = [ y ] ( R ~QG I ) )
85 83 84 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( a ( .r ` Q ) b ) = ( [ x ] ( R ~QG I ) ( .r ` Q ) [ y ] ( R ~QG I ) ) )
86 62 64 31 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( 0g ` Q ) = I )
87 82 85 86 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( [ x ] ( R ~QG I ) ( .r ` Q ) [ y ] ( R ~QG I ) ) = I )
88 80 87 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> [ ( x ( .r ` R ) y ) ] ( R ~QG I ) = I )
89 28 eqg0el 
 |-  ( ( R e. Grp /\ I e. ( SubGrp ` R ) ) -> ( [ ( x ( .r ` R ) y ) ] ( R ~QG I ) = I <-> ( x ( .r ` R ) y ) e. I ) )
90 89 biimpa 
 |-  ( ( ( R e. Grp /\ I e. ( SubGrp ` R ) ) /\ [ ( x ( .r ` R ) y ) ] ( R ~QG I ) = I ) -> ( x ( .r ` R ) y ) e. I )
91 63 65 88 90 syl21anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( x ( .r ` R ) y ) e. I )
92 rsp2 
 |-  ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) ) )
93 92 impl 
 |-  ( ( ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) )
94 93 imp 
 |-  ( ( ( ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. I -> ( x e. I \/ y e. I ) ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. I ) -> ( x e. I \/ y e. I ) )
95 59 60 61 91 94 syl1111anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( x e. I \/ y e. I ) )
96 86 eqeq2d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( a = ( 0g ` Q ) <-> a = I ) )
97 83 eqeq1d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( a = I <-> [ x ] ( R ~QG I ) = I ) )
98 28 eqg0el 
 |-  ( ( R e. Grp /\ I e. ( SubGrp ` R ) ) -> ( [ x ] ( R ~QG I ) = I <-> x e. I ) )
99 63 65 98 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( [ x ] ( R ~QG I ) = I <-> x e. I ) )
100 96 97 99 3bitrrd 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( x e. I <-> a = ( 0g ` Q ) ) )
101 86 eqeq2d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( b = ( 0g ` Q ) <-> b = I ) )
102 84 eqeq1d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( b = I <-> [ y ] ( R ~QG I ) = I ) )
103 28 eqg0el 
 |-  ( ( R e. Grp /\ I e. ( SubGrp ` R ) ) -> ( [ y ] ( R ~QG I ) = I <-> y e. I ) )
104 63 65 103 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( [ y ] ( R ~QG I ) = I <-> y e. I ) )
105 101 102 104 3bitrrd 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( y e. I <-> b = ( 0g ` Q ) ) )
106 100 105 orbi12d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( ( x e. I \/ y e. I ) <-> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) ) )
107 95 106 mpbid 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) /\ y e. ( Base ` R ) ) /\ b = [ y ] ( R ~QG I ) ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) )
108 simplr 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> b e. ( Base ` Q ) )
109 1 a1i 
 |-  ( R e. CRing -> Q = ( R /s ( R ~QG I ) ) )
110 eqidd 
 |-  ( R e. CRing -> ( Base ` R ) = ( Base ` R ) )
111 ovexd 
 |-  ( R e. CRing -> ( R ~QG I ) e. _V )
112 id 
 |-  ( R e. CRing -> R e. CRing )
113 109 110 111 112 qusbas 
 |-  ( R e. CRing -> ( ( Base ` R ) /. ( R ~QG I ) ) = ( Base ` Q ) )
114 113 ad4antr 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> ( ( Base ` R ) /. ( R ~QG I ) ) = ( Base ` Q ) )
115 108 114 eleqtrrd 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> b e. ( ( Base ` R ) /. ( R ~QG I ) ) )
116 115 ad2antrr 
 |-  ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) -> b e. ( ( Base ` R ) /. ( R ~QG I ) ) )
117 elqsi 
 |-  ( b e. ( ( Base ` R ) /. ( R ~QG I ) ) -> E. y e. ( Base ` R ) b = [ y ] ( R ~QG I ) )
118 116 117 syl 
 |-  ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) -> E. y e. ( Base ` R ) b = [ y ] ( R ~QG I ) )
119 107 118 r19.29a 
 |-  ( ( ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) /\ x e. ( Base ` R ) ) /\ a = [ x ] ( R ~QG I ) ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) )
120 simpllr 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> a e. ( Base ` Q ) )
121 120 114 eleqtrrd 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> a e. ( ( Base ` R ) /. ( R ~QG I ) ) )
122 elqsi 
 |-  ( a e. ( ( Base ` R ) /. ( R ~QG I ) ) -> E. x e. ( Base ` R ) a = [ x ] ( R ~QG I ) )
123 121 122 syl 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> E. x e. ( Base ` R ) a = [ x ] ( R ~QG I ) )
124 119 123 r19.29a 
 |-  ( ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) /\ ( a ( .r ` Q ) b ) = ( 0g ` Q ) ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) )
125 124 ex 
 |-  ( ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ a e. ( Base ` Q ) ) /\ b e. ( Base ` Q ) ) -> ( ( a ( .r ` Q ) b ) = ( 0g ` Q ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) ) )
126 125 anasss 
 |-  ( ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) /\ ( a e. ( Base ` Q ) /\ b e. ( Base ` Q ) ) ) -> ( ( a ( .r ` Q ) b ) = ( 0g ` Q ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) ) )
127 126 ralrimivva 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> A. a e. ( Base ` Q ) A. b e. ( Base ` Q ) ( ( a ( .r ` Q ) b ) = ( 0g ` Q ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) ) )
128 15 78 16 isdomn 
 |-  ( Q e. Domn <-> ( Q e. NzRing /\ A. a e. ( Base ` Q ) A. b e. ( Base ` Q ) ( ( a ( .r ` Q ) b ) = ( 0g ` Q ) -> ( a = ( 0g ` Q ) \/ b = ( 0g ` Q ) ) ) ) )
129 57 127 128 sylanbrc 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. Domn )
130 isidom 
 |-  ( Q e. IDomn <-> ( Q e. CRing /\ Q e. Domn ) )
131 7 129 130 sylanbrc 
 |-  ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn )