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 
|- U = ( R /s ( R ~QG S ) )
qus2idrng.i 
|- I = ( 2Ideal ` R )
Assertion qus2idrng 
|- ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> U e. Rng )

Proof

Step Hyp Ref Expression
1 qus2idrng.u 
 |-  U = ( R /s ( R ~QG S ) )
2 qus2idrng.i 
 |-  I = ( 2Ideal ` R )
3 1 a1i 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> U = ( R /s ( R ~QG S ) ) )
4 eqidd 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( Base ` R ) = ( Base ` R ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 simp3 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> S e. ( SubGrp ` R ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( R ~QG S ) = ( R ~QG S )
10 8 9 eqger 
 |-  ( S e. ( SubGrp ` R ) -> ( R ~QG S ) Er ( Base ` R ) )
11 7 10 syl 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( R ~QG S ) Er ( Base ` R ) )
12 rngabl 
 |-  ( R e. Rng -> R e. Abel )
13 12 3ad2ant1 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> R e. Abel )
14 ablnsg 
 |-  ( R e. Abel -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
15 13 14 syl 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
16 7 15 eleqtrrd 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> S e. ( NrmSGrp ` R ) )
17 8 9 5 eqgcpbl 
 |-  ( S e. ( NrmSGrp ` R ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( +g ` R ) b ) ( R ~QG S ) ( c ( +g ` R ) d ) ) )
18 16 17 syl 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( +g ` R ) b ) ( R ~QG S ) ( c ( +g ` R ) d ) ) )
19 8 9 2 6 2idlcpblrng 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( .r ` R ) b ) ( R ~QG S ) ( c ( .r ` R ) d ) ) )
20 simp1 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> R e. Rng )
21 3 4 5 6 11 18 19 20 qusrng 
 |-  ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> U e. Rng )