Metamath Proof Explorer

Theorem rngqiprnglinlem2

Description: Lemma 2 for rngqiprnglin . (Contributed by AV, 28-Feb-2025)

Ref Expression
Hypotheses rng2idlring.r 
|- ( ph -> R e. Rng )
rng2idlring.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rng2idlring.j 
|- J = ( R |`s I )
rng2idlring.u 
|- ( ph -> J e. Ring )
rng2idlring.b 
|- B = ( Base ` R )
rng2idlring.t 
|- .x. = ( .r ` R )
rng2idlring.1 
|- .1. = ( 1r ` J )
rngqiprngim.g 
|- .~ = ( R ~QG I )
rngqiprngim.q 
|- Q = ( R /s .~ )
Assertion rngqiprnglinlem2 
|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A .x. C ) ] .~ = ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r 
 |-  ( ph -> R e. Rng )
2 rng2idlring.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rng2idlring.j 
 |-  J = ( R |`s I )
4 rng2idlring.u 
 |-  ( ph -> J e. Ring )
5 rng2idlring.b 
 |-  B = ( Base ` R )
6 rng2idlring.t 
 |-  .x. = ( .r ` R )
7 rng2idlring.1 
 |-  .1. = ( 1r ` J )
8 rngqiprngim.g 
 |-  .~ = ( R ~QG I )
9 rngqiprngim.q 
 |-  Q = ( R /s .~ )
10 ringrng 
 |-  ( J e. Ring -> J e. Rng )
11 4 10 syl 
 |-  ( ph -> J e. Rng )
12 3 11 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
13 1 2 12 rng2idlsubrng 
 |-  ( ph -> I e. ( SubRng ` R ) )
14 subrngsubg 
 |-  ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) )
15 13 14 syl 
 |-  ( ph -> I e. ( SubGrp ` R ) )
16 1 2 15 3jca 
 |-  ( ph -> ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) )
17 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
18 8 oveq2i 
 |-  ( R /s .~ ) = ( R /s ( R ~QG I ) )
19 9 18 eqtri 
 |-  Q = ( R /s ( R ~QG I ) )
20 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
21 17 19 5 6 20 qusmulrng 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) /\ ( A e. B /\ C e. B ) ) -> ( [ A ] ( R ~QG I ) ( .r ` Q ) [ C ] ( R ~QG I ) ) = [ ( A .x. C ) ] ( R ~QG I ) )
22 16 21 sylan 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] ( R ~QG I ) ( .r ` Q ) [ C ] ( R ~QG I ) ) = [ ( A .x. C ) ] ( R ~QG I ) )
23 8 eceq2i 
 |-  [ A ] .~ = [ A ] ( R ~QG I )
24 8 eceq2i 
 |-  [ C ] .~ = [ C ] ( R ~QG I )
25 23 24 oveq12i 
 |-  ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) = ( [ A ] ( R ~QG I ) ( .r ` Q ) [ C ] ( R ~QG I ) )
26 8 eceq2i 
 |-  [ ( A .x. C ) ] .~ = [ ( A .x. C ) ] ( R ~QG I )
27 22 25 26 3eqtr4g 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) = [ ( A .x. C ) ] .~ )
28 27 eqcomd 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A .x. C ) ] .~ = ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) )