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 /s ( R ~QG S ) )
	qusring.i	\|- I = ( 2Ideal ` R )
	qusrhm.x	\|- X = ( Base ` R )
	qusrhm.f	\|- F = ( x e. X \|-> [ x ] ( R ~QG S ) )
Assertion	qusrhm	\|- ( ( R e. Ring /\ S e. I ) -> F e. ( R RingHom U ) )

Proof

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

Metamath Proof Explorer

Theorem qusrhm

Proof