qusrhm

Description: If S is a two-sided ideal in R , then the "natural map" from elements to their cosets is a ring homomorphism from R to R / S . (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	qusring.u	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
	qusring.i	$⊢ I = 2Ideal (R)$
	qusrhm.x	$⊢ X = {Base}_{R}$
	qusrhm.f	$⊢ F = (x \in X ⟼ [x] (R ~_{QG} S))$
Assertion	qusrhm	$⊢ (R \in Ring \land S \in I) \to F \in (R RingHom U)$

Proof

Step	Hyp	Ref	Expression
1		qusring.u	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
2		qusring.i	$⊢ I = 2Ideal (R)$
3		qusrhm.x	$⊢ X = {Base}_{R}$
4		qusrhm.f	$⊢ F = (x \in X ⟼ [x] (R ~_{QG} S))$
5		eqid	$⊢ 1_{R} = 1_{R}$
6		eqid	$⊢ 1_{U} = 1_{U}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ \cdot_{U} = \cdot_{U}$
9		simpl	$⊢ (R \in Ring \land S \in I) \to R \in Ring$
10	1 2	qusring	$⊢ (R \in Ring \land S \in I) \to U \in Ring$
11		eqid	$⊢ LIdeal (R) = LIdeal (R)$
12		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
13		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
14	11 12 13 2	2idlval	$⊢ I = LIdeal (R) \cap LIdeal ({opp}_{r} (R))$
15	14	elin2	$⊢ S \in I \leftrightarrow (S \in LIdeal (R) \land S \in LIdeal ({opp}_{r} (R)))$
16	15	simplbi	$⊢ S \in I \to S \in LIdeal (R)$
17	11	lidlsubg	$⊢ (R \in Ring \land S \in LIdeal (R)) \to S \in SubGrp (R)$
18	16 17	sylan2	$⊢ (R \in Ring \land S \in I) \to S \in SubGrp (R)$
19		eqid	$⊢ R ~_{QG} S = R ~_{QG} S$
20	3 19	eqger	$⊢ S \in SubGrp (R) \to (R ~_{QG} S) Er X$
21	18 20	syl	$⊢ (R \in Ring \land S \in I) \to (R ~_{QG} S) Er X$
22	3	fvexi	$⊢ X \in V$
23	22	a1i	$⊢ (R \in Ring \land S \in I) \to X \in V$
24	21 23 4	divsfval	$⊢ (R \in Ring \land S \in I) \to F (1_{R}) = [1_{R}] (R ~_{QG} S)$
25	1 2 5	qus1	$⊢ (R \in Ring \land S \in I) \to (U \in Ring \land [1_{R}] (R ~_{QG} S) = 1_{U})$
26	25	simprd	$⊢ (R \in Ring \land S \in I) \to [1_{R}] (R ~_{QG} S) = 1_{U}$
27	24 26	eqtrd	$⊢ (R \in Ring \land S \in I) \to F (1_{R}) = 1_{U}$
28	1	a1i	$⊢ (R \in Ring \land S \in I) \to U = R /_{𝑠} (R ~_{QG} S)$
29	3	a1i	$⊢ (R \in Ring \land S \in I) \to X = {Base}_{R}$
30	3 19 2 7	2idlcpbl	$⊢ (R \in Ring \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))$
31	3 7	ringcl	$⊢ (R \in Ring \land y \in X \land z \in X) \to y \cdot_{R} z \in X$
32	31	3expb	$⊢ (R \in Ring \land (y \in X \land z \in X)) \to y \cdot_{R} z \in X$
33	32	adantlr	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to y \cdot_{R} z \in X$
34	33	caovclg	$⊢ ((R \in Ring \land S \in I) \land (c \in X \land d \in X)) \to c \cdot_{R} d \in X$
35	28 29 21 9 30 34 7 8	qusmulval	$⊢ ((R \in Ring \land S \in I) \land y \in X \land z \in X) \to [y] (R ~_{QG} S) \cdot_{U} [z] (R ~_{QG} S) = [(y \cdot_{R} z)] (R ~_{QG} S)$
36	35	3expb	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to [y] (R ~_{QG} S) \cdot_{U} [z] (R ~_{QG} S) = [(y \cdot_{R} z)] (R ~_{QG} S)$
37	21	adantr	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to (R ~_{QG} S) Er X$
38	22	a1i	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to X \in V$
39	37 38 4	divsfval	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to F (y) = [y] (R ~_{QG} S)$
40	37 38 4	divsfval	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to F (z) = [z] (R ~_{QG} S)$
41	39 40	oveq12d	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to F (y) \cdot_{U} F (z) = [y] (R ~_{QG} S) \cdot_{U} [z] (R ~_{QG} S)$
42	37 38 4	divsfval	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to F (y \cdot_{R} z) = [(y \cdot_{R} z)] (R ~_{QG} S)$
43	36 41 42	3eqtr4rd	$⊢ ((R \in Ring \land S \in I) \land (y \in X \land z \in X)) \to F (y \cdot_{R} z) = F (y) \cdot_{U} F (z)$
44		ringabl	$⊢ R \in Ring \to R \in Abel$
45	44	adantr	$⊢ (R \in Ring \land S \in I) \to R \in Abel$
46		ablnsg	$⊢ R \in Abel \to NrmSGrp (R) = SubGrp (R)$
47	45 46	syl	$⊢ (R \in Ring \land S \in I) \to NrmSGrp (R) = SubGrp (R)$
48	18 47	eleqtrrd	$⊢ (R \in Ring \land S \in I) \to S \in NrmSGrp (R)$
49	3 1 4	qusghm	$⊢ S \in NrmSGrp (R) \to F \in (R GrpHom U)$
50	48 49	syl	$⊢ (R \in Ring \land S \in I) \to F \in (R GrpHom U)$
51	3 5 6 7 8 9 10 27 43 50	isrhm2d	$⊢ (R \in Ring \land S \in I) \to F \in (R RingHom U)$

Metamath Proof Explorer

Theorem qusrhm

Proof