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{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
Assertion	qsidomlem2	Could not format assertion : No typesetting found for |- ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) with typecode |-

Proof

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