Metamath Proof Explorer

Theorem 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 ) )