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

Metamath Proof Explorer

Theorem qusmulrng

Description: Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng . Similar to qusmul2idl . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 28-Feb-2025)

Ref Expression
Hypotheses qusmulrng.e 
|- .~ = ( R ~QG S )
qusmulrng.h 
|- H = ( R /s .~ )
qusmulrng.b 
|- B = ( Base ` R )
qusmulrng.p 
|- .x. = ( .r ` R )
qusmulrng.a 
|- .xb = ( .r ` H )
Assertion qusmulrng 
|- ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )

Proof

Step Hyp Ref Expression
1 qusmulrng.e 
 |-  .~ = ( R ~QG S )
2 qusmulrng.h 
 |-  H = ( R /s .~ )
3 qusmulrng.b 
 |-  B = ( Base ` R )
4 qusmulrng.p 
 |-  .x. = ( .r ` R )
5 qusmulrng.a 
 |-  .xb = ( .r ` H )
6 2 a1i 
 |-  ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) -> H = ( R /s .~ ) )
7 3 a1i 
 |-  ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) -> B = ( Base ` R ) )
8 3 1 eqger 
 |-  ( S e. ( SubGrp ` R ) -> .~ Er B )
9 8 3ad2ant3 
 |-  ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) -> .~ Er B )
10 simp1 
 |-  ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) -> R e. Rng )
11 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
12 3 1 11 4 2idlcpblrng 
 |-  ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) -> ( ( a .~ b /\ c .~ d ) -> ( a .x. c ) .~ ( b .x. d ) ) )
13 10 anim1i 
 |-  ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( b e. B /\ d e. B ) ) -> ( R e. Rng /\ ( b e. B /\ d e. B ) ) )
14 3anass 
 |-  ( ( R e. Rng /\ b e. B /\ d e. B ) <-> ( R e. Rng /\ ( b e. B /\ d e. B ) ) )
15 13 14 sylibr 
 |-  ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( b e. B /\ d e. B ) ) -> ( R e. Rng /\ b e. B /\ d e. B ) )
16 3 4 rngcl 
 |-  ( ( R e. Rng /\ b e. B /\ d e. B ) -> ( b .x. d ) e. B )
17 15 16 syl 
 |-  ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( b e. B /\ d e. B ) ) -> ( b .x. d ) e. B )
18 6 7 9 10 12 17 4 5 qusmulval 
 |-  ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ X e. B /\ Y e. B ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
19 18 3expb 
 |-  ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )