quscrng

Description: The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015)

	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	3	adantr	$⊢ (R \in CRing \land S \in I) \to R \in Ring$
5		simpr	$⊢ (R \in CRing \land S \in I) \to S \in I$
6	2	crng2idl	$⊢ R \in CRing \to I = 2Ideal (R)$
7	6	adantr	$⊢ (R \in CRing \land S \in I) \to I = 2Ideal (R)$
8	5 7	eleqtrd	$⊢ (R \in CRing \land S \in I) \to S \in 2Ideal (R)$
9		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
10	1 9	qusring	$⊢ (R \in Ring \land S \in 2Ideal (R)) \to U \in Ring$
11	4 8 10	syl2anc	$⊢ (R \in CRing \land S \in I) \to U \in Ring$
12	1	a1i	$⊢ (R \in CRing \land S \in I) \to U = R /_{𝑠} (R ~_{QG} S)$
13		eqidd	$⊢ (R \in CRing \land S \in I) \to {Base}_{R} = {Base}_{R}$
14		ovexd	$⊢ (R \in CRing \land S \in I) \to R ~_{QG} S \in V$
15	12 13 14 4	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	2	lidlsubg	$⊢ (R \in Ring \land S \in I) \to S \in SubGrp (R)$
32	3 31	sylan	$⊢ (R \in CRing \land S \in I) \to S \in SubGrp (R)$
33		eqid	$⊢ R ~_{QG} S = R ~_{QG} S$
34	26 33	eqger	$⊢ S \in SubGrp (R) \to (R ~_{QG} S) Er {Base}_{R}$
35	32 34	syl	$⊢ (R \in CRing \land S \in I) \to (R ~_{QG} S) Er {Base}_{R}$
36	26 33 9 27	2idlcpbl	$⊢ (R \in Ring \land S \in 2Ideal (R)) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a \cdot_{R} b) (R ~_{QG} S) (c \cdot_{R} d))$
37	4 8 36	syl2anc	$⊢ (R \in CRing \land S \in I) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a \cdot_{R} b) (R ~_{QG} S) (c \cdot_{R} d))$
38	26 27	ringcl	$⊢ (R \in Ring \land c \in {Base}_{R} \land d \in {Base}_{R}) \to c \cdot_{R} d \in {Base}_{R}$
39	38	3expb	$⊢ (R \in Ring \land (c \in {Base}_{R} \land d \in {Base}_{R})) \to c \cdot_{R} d \in {Base}_{R}$
40	4 39	sylan	$⊢ ((R \in CRing \land S \in I) \land (c \in {Base}_{R} \land d \in {Base}_{R})) \to c \cdot_{R} d \in {Base}_{R}$
41		eqid	$⊢ \cdot_{U} = \cdot_{U}$
42	12 13 35 4 37 40 27 41	qusmulval	$⊢ ((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)$
43	42	3expa	$⊢ (((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	12 13 35 4 37 40 27 41	qusmulval	$⊢ ((R \in CRing \land S \in I) \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)$
45	44	3expa	$⊢ (((R \in CRing \land S \in I) \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	45	an32s	$⊢ (((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	11 53 55	sylanbrc	$⊢ (R \in CRing \land S \in I) \to U \in CRing$

Metamath Proof Explorer

Theorem quscrng

Proof