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	$⊢ ((R \in CRing \land I \in LIdeal (R)) \land Q \in IDomn) \to I \in PrmIdeal (R)$

Proof

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

Metamath Proof Explorer

Theorem qsidomlem1

Proof