Metamath Proof Explorer

Theorem qusmul

Description: Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024)

Ref Expression
Hypotheses qusmul.h 
|- Q = ( R /s ( R ~QG I ) )
qusmul.v 
|- B = ( Base ` R )
qusmul.p 
|- .x. = ( .r ` R )
qusmul.a 
|- .X. = ( .r ` Q )
qusmul.r 
|- ( ph -> R e. CRing )
qusmul.i 
|- ( ph -> I e. ( LIdeal ` R ) )
qusmul.x 
|- ( ph -> X e. B )
qusmul.y 
|- ( ph -> Y e. B )
Assertion qusmul 
|- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )

Proof

Step Hyp Ref Expression
1 qusmul.h 
 |-  Q = ( R /s ( R ~QG I ) )
2 qusmul.v 
 |-  B = ( Base ` R )
3 qusmul.p 
 |-  .x. = ( .r ` R )
4 qusmul.a 
 |-  .X. = ( .r ` Q )
5 qusmul.r 
 |-  ( ph -> R e. CRing )
6 qusmul.i 
 |-  ( ph -> I e. ( LIdeal ` R ) )
7 qusmul.x 
 |-  ( ph -> X e. B )
8 qusmul.y 
 |-  ( ph -> Y e. B )
9 1 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG I ) ) )
10 2 a1i 
 |-  ( ph -> B = ( Base ` R ) )
11 5 crngringd 
 |-  ( ph -> R e. Ring )
12 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
13 12 lidlsubg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
14 11 6 13 syl2anc 
 |-  ( ph -> I e. ( SubGrp ` R ) )
15 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
16 2 15 eqger 
 |-  ( I e. ( SubGrp ` R ) -> ( R ~QG I ) Er B )
17 14 16 syl 
 |-  ( ph -> ( R ~QG I ) Er B )
18 12 crng2idl 
 |-  ( R e. CRing -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
19 5 18 syl 
 |-  ( ph -> ( LIdeal ` R ) = ( 2Ideal ` R ) )
20 6 19 eleqtrd 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
21 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
22 2 15 21 3 2idlcpbl 
 |-  ( ( R e. Ring /\ I e. ( 2Ideal ` R ) ) -> ( ( x ( R ~QG I ) y /\ z ( R ~QG I ) t ) -> ( x .x. z ) ( R ~QG I ) ( y .x. t ) ) )
23 11 20 22 syl2anc 
 |-  ( ph -> ( ( x ( R ~QG I ) y /\ z ( R ~QG I ) t ) -> ( x .x. z ) ( R ~QG I ) ( y .x. t ) ) )
24 2 3 ringcl 
 |-  ( ( R e. Ring /\ p e. B /\ q e. B ) -> ( p .x. q ) e. B )
25 24 3expb 
 |-  ( ( R e. Ring /\ ( p e. B /\ q e. B ) ) -> ( p .x. q ) e. B )
26 11 25 sylan 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p .x. q ) e. B )
27 26 caovclg 
 |-  ( ( ph /\ ( y e. B /\ t e. B ) ) -> ( y .x. t ) e. B )
28 9 10 17 5 23 27 3 4 qusmulval 
 |-  ( ( ph /\ X e. B /\ Y e. B ) -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )
29 7 8 28 mpd3an23 
 |-  ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )