This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qus2idrng

Description: The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring ( qusring analog). (Contributed by AV, 23-Feb-2025)

Ref Expression
Hypotheses qus2idrng.u ⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
qus2idrng.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
Assertion qus2idrng ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑈 ∈ Rng )

Proof

Step Hyp Ref Expression
1 qus2idrng.u ⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
2 qus2idrng.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
3 1 a1i ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) ) )
4 eqidd ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 simp3 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( 𝑅 ~QG 𝑆 ) = ( 𝑅 ~QG 𝑆 )
10 8 9 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝑆 ) Er ( Base ‘ 𝑅 ) )
11 7 10 syl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑅 ~QG 𝑆 ) Er ( Base ‘ 𝑅 ) )
12 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
13 12 3ad2ant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑅 ∈ Abel )
14 ablnsg ⊢ ( 𝑅 ∈ Abel → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
15 13 14 syl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( NrmSGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑅 ) )
16 7 15 eleqtrrd ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑆 ∈ ( NrmSGrp ‘ 𝑅 ) )
17 8 9 5 eqgcpbl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝑅 ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( +g ‘ 𝑅 ) 𝑑 ) ) )
18 16 17 syl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( +g ‘ 𝑅 ) 𝑑 ) ) )
19 8 9 2 6 2idlcpblrng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐 ∧ 𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ) )
20 simp1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑅 ∈ Rng )
21 3 4 5 6 11 18 19 20 qusrng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑈 ∈ Rng )