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 )