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 /_{𝑠} (R ~_{QG} I)$
	Assertion	qsidomlem2	$⊢ (R \in CRing \land I \in PrmIdeal (R)) \to Q \in IDomn$

Proof

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

Metamath Proof Explorer

Theorem qsidomlem2

Proof