Metamath Proof Explorer

Theorem qus1

Description: The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses qusring.u ⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
qusring.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
qus1.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion qus1 ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝑈 ∈ Ring ∧ [ 1 ] ( 𝑅 ~QG 𝑆 ) = ( 1r ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 qusring.u ⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
2 qusring.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
3 qus1.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 1 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) ) )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 5 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
7 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
10 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
11 eqid ⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
12 9 10 11 2 2idlval ⊢ 𝐼 = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
13 12 elin2 ⊢ ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
14 13 simplbi ⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
15 9 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
16 14 15 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
17 eqid ⊢ ( 𝑅 ~QG 𝑆 ) = ( 𝑅 ~QG 𝑆 )
18 5 17 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝑆 ) Er ( Base ‘ 𝑅 ) )
19 16 18 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝑅 ~QG 𝑆 ) Er ( Base ‘ 𝑅 ) )
20 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
21 20 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Abel )
22 ablnsg ⊢ ( 𝑅 ∈ Abel → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
23 21 22 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
24 16 23 eleqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝑅 ) )
25 5 17 7 eqgcpbl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝑅 ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( +g ‘ 𝑅 ) 𝑑 ) ) )
26 24 25 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( +g ‘ 𝑅 ) 𝑑 ) ) )
27 5 17 2 8 2idlcpbl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ) )
28 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Ring )
29 4 6 7 8 3 19 26 27 28 qusring2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝑈 ∈ Ring ∧ [ 1 ] ( 𝑅 ~QG 𝑆 ) = ( 1r ‘ 𝑈 ) ) )