Metamath Proof Explorer

Theorem qusmul2

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

Ref Expression
Hypotheses qusmul2.h 
|- Q = ( R /s ( R ~QG I ) )
qusmul2.v 
|- B = ( Base ` R )
qusmul2.p 
|- .x. = ( .r ` R )
qusmul2.a 
|- .X. = ( .r ` Q )
qusmul2.1 
|- ( ph -> R e. Ring )
qusmul2.2 
|- ( ph -> I e. ( 2Ideal ` R ) )
qusmul2.3 
|- ( ph -> X e. B )
qusmul2.4 
|- ( ph -> Y e. B )
Assertion qusmul2 
|- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )

Proof

Step Hyp Ref Expression
1 qusmul2.h 
 |-  Q = ( R /s ( R ~QG I ) )
2 qusmul2.v 
 |-  B = ( Base ` R )
3 qusmul2.p 
 |-  .x. = ( .r ` R )
4 qusmul2.a 
 |-  .X. = ( .r ` Q )
5 qusmul2.1 
 |-  ( ph -> R e. Ring )
6 qusmul2.2 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
7 qusmul2.3 
 |-  ( ph -> X e. B )
8 qusmul2.4 
 |-  ( ph -> Y e. B )
9 1 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG I ) ) )
10 2 a1i 
 |-  ( ph -> B = ( Base ` R ) )
11 6 2idllidld 
 |-  ( ph -> I e. ( LIdeal ` R ) )
12 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
13 12 lidlsubg 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
14 5 11 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 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
19 2 15 18 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 ) ) )
20 5 6 19 syl2anc 
 |-  ( ph -> ( ( x ( R ~QG I ) y /\ z ( R ~QG I ) t ) -> ( x .x. z ) ( R ~QG I ) ( y .x. t ) ) )
21 2 3 ringcl 
 |-  ( ( R e. Ring /\ p e. B /\ q e. B ) -> ( p .x. q ) e. B )
22 21 3expb 
 |-  ( ( R e. Ring /\ ( p e. B /\ q e. B ) ) -> ( p .x. q ) e. B )
23 5 22 sylan 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p .x. q ) e. B )
24 23 caovclg 
 |-  ( ( ph /\ ( y e. B /\ t e. B ) ) -> ( y .x. t ) e. B )
25 9 10 17 5 20 24 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 ) )
26 7 8 25 mpd3an23 
 |-  ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )