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	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
	qus2idrng.i	$⊢ I = 2Ideal (R)$
Assertion	qus2idrng	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to U \in Rng$

Proof

Step	Hyp	Ref	Expression
1		qus2idrng.u	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
2		qus2idrng.i	$⊢ I = 2Ideal (R)$
3	1	a1i	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to U = R /_{𝑠} (R ~_{QG} S)$
4		eqidd	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ +_{R} = +_{R}$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		simp3	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to S \in SubGrp (R)$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ R ~_{QG} S = R ~_{QG} S$
10	8 9	eqger	$⊢ S \in SubGrp (R) \to (R ~_{QG} S) Er {Base}_{R}$
11	7 10	syl	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to (R ~_{QG} S) Er {Base}_{R}$
12		rngabl	$⊢ R \in Rng \to R \in Abel$
13	12	3ad2ant1	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to R \in Abel$
14		ablnsg	$⊢ R \in Abel \to NrmSGrp (R) = SubGrp (R)$
15	13 14	syl	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to NrmSGrp (R) = SubGrp (R)$
16	7 15	eleqtrrd	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to S \in NrmSGrp (R)$
17	8 9 5	eqgcpbl	$⊢ S \in NrmSGrp (R) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a +_{R} b) (R ~_{QG} S) (c +_{R} d))$
18	16 17	syl	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a +_{R} b) (R ~_{QG} S) (c +_{R} d))$
19	8 9 2 6	2idlcpblrng	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a \cdot_{R} b) (R ~_{QG} S) (c \cdot_{R} d))$
20		simp1	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to R \in Rng$
21	3 4 5 6 11 18 19 20	qusrng	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to U \in Rng$

Metamath Proof Explorer

Theorem qus2idrng

Proof