Metamath Proof Explorer

Theorem opprqusmulr

Description: The multiplication operation of the quotient of the opposite ring is the same as the multiplication operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses opprqus.b 
|- B = ( Base ` R )
opprqus.o 
|- O = ( oppR ` R )
opprqus.q 
|- Q = ( R /s ( R ~QG I ) )
opprqus1r.r 
|- ( ph -> R e. Ring )
opprqus1r.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
opprqusmulr.e 
|- E = ( Base ` Q )
opprqusmulr.x 
|- ( ph -> X e. E )
opprqusmulr.y 
|- ( ph -> Y e. E )
Assertion opprqusmulr 
|- ( ph -> ( X ( .r ` ( oppR ` Q ) ) Y ) = ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) )

Proof

Step Hyp Ref Expression
1 opprqus.b 
 |-  B = ( Base ` R )
2 opprqus.o 
 |-  O = ( oppR ` R )
3 opprqus.q 
 |-  Q = ( R /s ( R ~QG I ) )
4 opprqus1r.r 
 |-  ( ph -> R e. Ring )
5 opprqus1r.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
6 opprqusmulr.e 
 |-  E = ( Base ` Q )
7 opprqusmulr.x 
 |-  ( ph -> X e. E )
8 opprqusmulr.y 
 |-  ( ph -> Y e. E )
9 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
10 eqid 
 |-  ( oppR ` Q ) = ( oppR ` Q )
11 eqid 
 |-  ( .r ` ( oppR ` Q ) ) = ( .r ` ( oppR ` Q ) )
12 6 9 10 11 opprmul 
 |-  ( X ( .r ` ( oppR ` Q ) ) Y ) = ( Y ( .r ` Q ) X )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 4 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> R e. Ring )
15 5 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> I e. ( 2Ideal ` R ) )
16 simplr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> q e. B )
17 simp-4r 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> p e. B )
18 3 1 13 9 14 15 16 17 qusmul2 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( [ q ] ( R ~QG I ) ( .r ` Q ) [ p ] ( R ~QG I ) ) = [ ( q ( .r ` R ) p ) ] ( R ~QG I ) )
19 simpr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> Y = [ q ] ( R ~QG I ) )
20 simpllr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> X = [ p ] ( R ~QG I ) )
21 19 20 oveq12d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( Y ( .r ` Q ) X ) = ( [ q ] ( R ~QG I ) ( .r ` Q ) [ p ] ( R ~QG I ) ) )
22 eqid 
 |-  ( O /s ( O ~QG I ) ) = ( O /s ( O ~QG I ) )
23 2 1 opprbas 
 |-  B = ( Base ` O )
24 eqid 
 |-  ( .r ` O ) = ( .r ` O )
25 eqid 
 |-  ( .r ` ( O /s ( O ~QG I ) ) ) = ( .r ` ( O /s ( O ~QG I ) ) )
26 2 opprring 
 |-  ( R e. Ring -> O e. Ring )
27 4 26 syl 
 |-  ( ph -> O e. Ring )
28 27 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> O e. Ring )
29 2 4 oppr2idl 
 |-  ( ph -> ( 2Ideal ` R ) = ( 2Ideal ` O ) )
30 5 29 eleqtrd 
 |-  ( ph -> I e. ( 2Ideal ` O ) )
31 30 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> I e. ( 2Ideal ` O ) )
32 22 23 24 25 28 31 17 16 qusmul2 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( [ p ] ( O ~QG I ) ( .r ` ( O /s ( O ~QG I ) ) ) [ q ] ( O ~QG I ) ) = [ ( p ( .r ` O ) q ) ] ( O ~QG I ) )
33 5 2idllidld 
 |-  ( ph -> I e. ( LIdeal ` R ) )
34 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
35 1 34 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
36 33 35 syl 
 |-  ( ph -> I C_ B )
37 2 1 oppreqg 
 |-  ( ( R e. Ring /\ I C_ B ) -> ( R ~QG I ) = ( O ~QG I ) )
38 4 36 37 syl2anc 
 |-  ( ph -> ( R ~QG I ) = ( O ~QG I ) )
39 38 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( R ~QG I ) = ( O ~QG I ) )
40 39 eceq2d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> [ p ] ( R ~QG I ) = [ p ] ( O ~QG I ) )
41 20 40 eqtrd 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> X = [ p ] ( O ~QG I ) )
42 39 eceq2d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> [ q ] ( R ~QG I ) = [ q ] ( O ~QG I ) )
43 19 42 eqtrd 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> Y = [ q ] ( O ~QG I ) )
44 41 43 oveq12d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) = ( [ p ] ( O ~QG I ) ( .r ` ( O /s ( O ~QG I ) ) ) [ q ] ( O ~QG I ) ) )
45 1 13 2 24 opprmul 
 |-  ( p ( .r ` O ) q ) = ( q ( .r ` R ) p )
46 45 a1i 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( p ( .r ` O ) q ) = ( q ( .r ` R ) p ) )
47 46 eceq1d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> [ ( p ( .r ` O ) q ) ] ( R ~QG I ) = [ ( q ( .r ` R ) p ) ] ( R ~QG I ) )
48 39 eceq2d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> [ ( p ( .r ` O ) q ) ] ( R ~QG I ) = [ ( p ( .r ` O ) q ) ] ( O ~QG I ) )
49 47 48 eqtr3d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> [ ( q ( .r ` R ) p ) ] ( R ~QG I ) = [ ( p ( .r ` O ) q ) ] ( O ~QG I ) )
50 32 44 49 3eqtr4d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) = [ ( q ( .r ` R ) p ) ] ( R ~QG I ) )
51 18 21 50 3eqtr4d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( Y ( .r ` Q ) X ) = ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) )
52 10 6 opprbas 
 |-  E = ( Base ` ( oppR ` Q ) )
53 8 52 eleqtrdi 
 |-  ( ph -> Y e. ( Base ` ( oppR ` Q ) ) )
54 53 ad2antrr 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> Y e. ( Base ` ( oppR ` Q ) ) )
55 3 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG I ) ) )
56 1 a1i 
 |-  ( ph -> B = ( Base ` R ) )
57 ovexd 
 |-  ( ph -> ( R ~QG I ) e. _V )
58 55 56 57 4 qusbas 
 |-  ( ph -> ( B /. ( R ~QG I ) ) = ( Base ` Q ) )
59 6 52 eqtr3i 
 |-  ( Base ` Q ) = ( Base ` ( oppR ` Q ) )
60 58 59 eqtr2di 
 |-  ( ph -> ( Base ` ( oppR ` Q ) ) = ( B /. ( R ~QG I ) ) )
61 60 ad2antrr 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> ( Base ` ( oppR ` Q ) ) = ( B /. ( R ~QG I ) ) )
62 54 61 eleqtrd 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> Y e. ( B /. ( R ~QG I ) ) )
63 elqsi 
 |-  ( Y e. ( B /. ( R ~QG I ) ) -> E. q e. B Y = [ q ] ( R ~QG I ) )
64 62 63 syl 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> E. q e. B Y = [ q ] ( R ~QG I ) )
65 51 64 r19.29a 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> ( Y ( .r ` Q ) X ) = ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) )
66 7 52 eleqtrdi 
 |-  ( ph -> X e. ( Base ` ( oppR ` Q ) ) )
67 66 60 eleqtrd 
 |-  ( ph -> X e. ( B /. ( R ~QG I ) ) )
68 elqsi 
 |-  ( X e. ( B /. ( R ~QG I ) ) -> E. p e. B X = [ p ] ( R ~QG I ) )
69 67 68 syl 
 |-  ( ph -> E. p e. B X = [ p ] ( R ~QG I ) )
70 65 69 r19.29a 
 |-  ( ph -> ( Y ( .r ` Q ) X ) = ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) )
71 12 70 eqtrid 
 |-  ( ph -> ( X ( .r ` ( oppR ` Q ) ) Y ) = ( X ( .r ` ( O /s ( O ~QG I ) ) ) Y ) )