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 ⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
qusring.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
qusrhm.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
qusrhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝑅 ~QG 𝑆 ) )
Assertion qusrhm ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑈 ) )

Proof

Step Hyp Ref Expression
1 qusring.u ⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
2 qusring.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
3 qusrhm.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
4 qusrhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝑅 ~QG 𝑆 ) )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 eqid ⊢ ( 1r ‘ 𝑈 ) = ( 1r ‘ 𝑈 )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 eqid ⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 )
9 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Ring )
10 1 2 qusring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑈 ∈ Ring )
11 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
12 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
13 eqid ⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
14 11 12 13 2 2idlval ⊢ 𝐼 = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
15 14 elin2 ⊢ ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
16 15 simplbi ⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
17 11 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
18 16 17 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
19 eqid ⊢ ( 𝑅 ~QG 𝑆 ) = ( 𝑅 ~QG 𝑆 )
20 3 19 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝑆 ) Er 𝑋 )
21 18 20 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝑅 ~QG 𝑆 ) Er 𝑋 )
22 3 fvexi ⊢ 𝑋 ∈ V
23 22 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑋 ∈ V )
24 21 23 4 divsfval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑆 ) )
25 1 2 5 qus1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝑈 ∈ Ring ∧ [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑆 ) = ( 1r ‘ 𝑈 ) ) )
26 25 simprd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑆 ) = ( 1r ‘ 𝑈 ) )
27 24 26 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑈 ) )
28 1 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) ) )
29 3 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑋 = ( Base ‘ 𝑅 ) )
30 3 19 2 7 2idlcpbl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ) )
31 3 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 )
32 31 3expb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 )
33 32 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 )
34 33 caovclg ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) → ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝑋 )
35 28 29 21 9 30 34 7 8 qusmulval ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝑆 ) ( .r ‘ 𝑈 ) [ 𝑧 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ] ( 𝑅 ~QG 𝑆 ) )
36 35 3expb ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝑆 ) ( .r ‘ 𝑈 ) [ 𝑧 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ] ( 𝑅 ~QG 𝑆 ) )
37 21 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑅 ~QG 𝑆 ) Er 𝑋 )
38 22 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑋 ∈ V )
39 37 38 4 divsfval ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) = [ 𝑦 ] ( 𝑅 ~QG 𝑆 ) )
40 37 38 4 divsfval ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) = [ 𝑧 ] ( 𝑅 ~QG 𝑆 ) )
41 39 40 oveq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( [ 𝑦 ] ( 𝑅 ~QG 𝑆 ) ( .r ‘ 𝑈 ) [ 𝑧 ] ( 𝑅 ~QG 𝑆 ) ) )
42 37 38 4 divsfval ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = [ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ] ( 𝑅 ~QG 𝑆 ) )
43 36 41 42 3eqtr4rd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) )
44 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
45 44 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Abel )
46 ablnsg ⊢ ( 𝑅 ∈ Abel → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
47 45 46 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
48 18 47 eleqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝑅 ) )
49 3 1 4 qusghm ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑈 ) )
50 48 49 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑈 ) )
51 3 5 6 7 8 9 10 27 43 50 isrhm2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑈 ) )