quscrng

Description: The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015) (Proof shortened by AV, 3-Apr-2025)

	Ref	Expression
Hypotheses	quscrng.u	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
	quscrng.i	$⊢ I = LIdeal (R)$
Assertion	quscrng	$⊢ (R \in CRing \land S \in I) \to U \in CRing$

Proof

Step	Hyp	Ref	Expression
1		quscrng.u	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
2		quscrng.i	$⊢ I = LIdeal (R)$
3		crngring	$⊢ R \in CRing \to R \in Ring$
4		simpr	$⊢ (R \in CRing \land S \in I) \to S \in I$
5	2	crng2idl	$⊢ R \in CRing \to I = 2Ideal (R)$
6	5	adantr	$⊢ (R \in CRing \land S \in I) \to I = 2Ideal (R)$
7	4 6	eleqtrd	$⊢ (R \in CRing \land S \in I) \to S \in 2Ideal (R)$
8		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
9	1 8	qusring	$⊢ (R \in Ring \land S \in 2Ideal (R)) \to U \in Ring$
10	3 7 9	syl2an2r	$⊢ (R \in CRing \land S \in I) \to U \in Ring$
11	1	a1i	$⊢ (R \in CRing \land S \in I) \to U = R /_{𝑠} (R ~_{QG} S)$
12		eqidd	$⊢ (R \in CRing \land S \in I) \to {Base}_{R} = {Base}_{R}$
13		ovexd	$⊢ (R \in CRing \land S \in I) \to R ~_{QG} S \in V$
14	3	adantr	$⊢ (R \in CRing \land S \in I) \to R \in Ring$
15	11 12 13 14	qusbas	$⊢ (R \in CRing \land S \in I) \to {Base}_{R} / (R ~_{QG} S) = {Base}_{U}$
16	15	eleq2d	$⊢ (R \in CRing \land S \in I) \to (x \in ({Base}_{R} / (R ~_{QG} S)) \leftrightarrow x \in {Base}_{U})$
17	15	eleq2d	$⊢ (R \in CRing \land S \in I) \to (y \in ({Base}_{R} / (R ~_{QG} S)) \leftrightarrow y \in {Base}_{U})$
18	16 17	anbi12d	$⊢ (R \in CRing \land S \in I) \to ((x \in ({Base}_{R} / (R ~_{QG} S)) \land y \in ({Base}_{R} / (R ~_{QG} S))) \leftrightarrow (x \in {Base}_{U} \land y \in {Base}_{U}))$
19		eqid	$⊢ {Base}_{R} / (R ~_{QG} S) = {Base}_{R} / (R ~_{QG} S)$
20		oveq2	$⊢ [u] (R ~_{QG} S) = y \to x \cdot_{U} [u] (R ~_{QG} S) = x \cdot_{U} y$
21		oveq1	$⊢ [u] (R ~_{QG} S) = y \to [u] (R ~_{QG} S) \cdot_{U} x = y \cdot_{U} x$
22	20 21	eqeq12d	$⊢ [u] (R ~_{QG} S) = y \to (x \cdot_{U} [u] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} x \leftrightarrow x \cdot_{U} y = y \cdot_{U} x)$
23		oveq1	$⊢ [v] (R ~_{QG} S) = x \to [v] (R ~_{QG} S) \cdot_{U} [u] (R ~_{QG} S) = x \cdot_{U} [u] (R ~_{QG} S)$
24		oveq2	$⊢ [v] (R ~_{QG} S) = x \to [u] (R ~_{QG} S) \cdot_{U} [v] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} x$
25	23 24	eqeq12d	$⊢ [v] (R ~_{QG} S) = x \to ([v] (R ~_{QG} S) \cdot_{U} [u] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} [v] (R ~_{QG} S) \leftrightarrow x \cdot_{U} [u] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} x)$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27		eqid	$⊢ \cdot_{R} = \cdot_{R}$
28	26 27	crngcom	$⊢ (R \in CRing \land u \in {Base}_{R} \land v \in {Base}_{R}) \to u \cdot_{R} v = v \cdot_{R} u$
29	28	ad4ant134	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to u \cdot_{R} v = v \cdot_{R} u$
30	29	eceq1d	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to [(u \cdot_{R} v)] (R ~_{QG} S) = [(v \cdot_{R} u)] (R ~_{QG} S)$
31		ringrng	$⊢ R \in Ring \to R \in Rng$
32	3 31	syl	$⊢ R \in CRing \to R \in Rng$
33	32	adantr	$⊢ (R \in CRing \land S \in I) \to R \in Rng$
34	2	lidlsubg	$⊢ (R \in Ring \land S \in I) \to S \in SubGrp (R)$
35	3 34	sylan	$⊢ (R \in CRing \land S \in I) \to S \in SubGrp (R)$
36	33 7 35	3jca	$⊢ (R \in CRing \land S \in I) \to (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R))$
37	36	adantr	$⊢ ((R \in CRing \land S \in I) \land u \in {Base}_{R}) \to (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R))$
38		simpr	$⊢ ((R \in CRing \land S \in I) \land u \in {Base}_{R}) \to u \in {Base}_{R}$
39	38	anim1i	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to (u \in {Base}_{R} \land v \in {Base}_{R})$
40		eqid	$⊢ R ~_{QG} S = R ~_{QG} S$
41		eqid	$⊢ \cdot_{U} = \cdot_{U}$
42	40 1 26 27 41	qusmulrng	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (u \in {Base}_{R} \land v \in {Base}_{R})) \to [u] (R ~_{QG} S) \cdot_{U} [v] (R ~_{QG} S) = [(u \cdot_{R} v)] (R ~_{QG} S)$
43	37 39 42	syl2an2r	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to [u] (R ~_{QG} S) \cdot_{U} [v] (R ~_{QG} S) = [(u \cdot_{R} v)] (R ~_{QG} S)$
44	39	ancomd	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to (v \in {Base}_{R} \land u \in {Base}_{R})$
45	40 1 26 27 41	qusmulrng	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (v \in {Base}_{R} \land u \in {Base}_{R})) \to [v] (R ~_{QG} S) \cdot_{U} [u] (R ~_{QG} S) = [(v \cdot_{R} u)] (R ~_{QG} S)$
46	37 44 45	syl2an2r	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to [v] (R ~_{QG} S) \cdot_{U} [u] (R ~_{QG} S) = [(v \cdot_{R} u)] (R ~_{QG} S)$
47	30 43 46	3eqtr4rd	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land v \in {Base}_{R}) \to [v] (R ~_{QG} S) \cdot_{U} [u] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} [v] (R ~_{QG} S)$
48	19 25 47	ectocld	$⊢ (((R \in CRing \land S \in I) \land u \in {Base}_{R}) \land x \in ({Base}_{R} / (R ~_{QG} S))) \to x \cdot_{U} [u] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} x$
49	48	an32s	$⊢ (((R \in CRing \land S \in I) \land x \in ({Base}_{R} / (R ~_{QG} S))) \land u \in {Base}_{R}) \to x \cdot_{U} [u] (R ~_{QG} S) = [u] (R ~_{QG} S) \cdot_{U} x$
50	19 22 49	ectocld	$⊢ (((R \in CRing \land S \in I) \land x \in ({Base}_{R} / (R ~_{QG} S))) \land y \in ({Base}_{R} / (R ~_{QG} S))) \to x \cdot_{U} y = y \cdot_{U} x$
51	50	expl	$⊢ (R \in CRing \land S \in I) \to ((x \in ({Base}_{R} / (R ~_{QG} S)) \land y \in ({Base}_{R} / (R ~_{QG} S))) \to x \cdot_{U} y = y \cdot_{U} x)$
52	18 51	sylbird	$⊢ (R \in CRing \land S \in I) \to ((x \in {Base}_{U} \land y \in {Base}_{U}) \to x \cdot_{U} y = y \cdot_{U} x)$
53	52	ralrimivv	$⊢ (R \in CRing \land S \in I) \to \forall x \in {Base}_{U} \forall y \in {Base}_{U} x \cdot_{U} y = y \cdot_{U} x$
54		eqid	$⊢ {Base}_{U} = {Base}_{U}$
55	54 41	iscrng2	$⊢ U \in CRing \leftrightarrow (U \in Ring \land \forall x \in {Base}_{U} \forall y \in {Base}_{U} x \cdot_{U} y = y \cdot_{U} x)$
56	10 53 55	sylanbrc	$⊢ (R \in CRing \land S \in I) \to U \in CRing$

Metamath Proof Explorer

Theorem quscrng

Proof