Metamath Proof Explorer

Theorem opprqusplusg

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

Ref Expression
Hypotheses opprqus.b 
|- B = ( Base ` R )
opprqus.o 
|- O = ( oppR ` R )
opprqus.q 
|- Q = ( R /s ( R ~QG I ) )
opprqus.i 
|- ( ph -> I e. ( NrmSGrp ` R ) )
opprqusplusg.e 
|- E = ( Base ` Q )
opprqusplusg.x 
|- ( ph -> X e. E )
opprqusplusg.y 
|- ( ph -> Y e. E )
Assertion opprqusplusg 
|- ( ph -> ( X ( +g ` ( oppR ` Q ) ) Y ) = ( X ( +g ` ( 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 opprqus.i 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
5 opprqusplusg.e 
 |-  E = ( Base ` Q )
6 opprqusplusg.x 
 |-  ( ph -> X e. E )
7 opprqusplusg.y 
 |-  ( ph -> Y e. E )
8 eqid 
 |-  ( oppR ` Q ) = ( oppR ` Q )
9 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
10 8 9 oppradd 
 |-  ( +g ` Q ) = ( +g ` ( oppR ` Q ) )
11 10 oveqi 
 |-  ( X ( +g ` Q ) Y ) = ( X ( +g ` ( oppR ` Q ) ) Y )
12 4 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> I e. ( NrmSGrp ` R ) )
13 simp-4r 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> p e. B )
14 simplr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> q e. B )
15 eqid 
 |-  ( +g ` R ) = ( +g ` R )
16 3 1 15 9 qusadd 
 |-  ( ( I e. ( NrmSGrp ` R ) /\ p e. B /\ q e. B ) -> ( [ p ] ( R ~QG I ) ( +g ` Q ) [ q ] ( R ~QG I ) ) = [ ( p ( +g ` R ) q ) ] ( R ~QG I ) )
17 12 13 14 16 syl3anc 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( [ p ] ( R ~QG I ) ( +g ` Q ) [ q ] ( R ~QG I ) ) = [ ( p ( +g ` R ) q ) ] ( R ~QG I ) )
18 simpllr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> X = [ 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 18 19 oveq12d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( X ( +g ` Q ) Y ) = ( [ p ] ( R ~QG I ) ( +g ` Q ) [ q ] ( R ~QG I ) ) )
21 4 elfvexd 
 |-  ( ph -> R e. _V )
22 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
23 1 subgss 
 |-  ( I e. ( SubGrp ` R ) -> I C_ B )
24 4 22 23 3syl 
 |-  ( ph -> I C_ B )
25 2 1 oppreqg 
 |-  ( ( R e. _V /\ I C_ B ) -> ( R ~QG I ) = ( O ~QG I ) )
26 21 24 25 syl2anc 
 |-  ( ph -> ( R ~QG I ) = ( O ~QG I ) )
27 26 eceq2d 
 |-  ( ph -> [ p ] ( R ~QG I ) = [ p ] ( O ~QG I ) )
28 26 eceq2d 
 |-  ( ph -> [ q ] ( R ~QG I ) = [ q ] ( O ~QG I ) )
29 27 28 oveq12d 
 |-  ( ph -> ( [ p ] ( R ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( R ~QG I ) ) = ( [ p ] ( O ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( O ~QG I ) ) )
30 29 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( [ p ] ( R ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( R ~QG I ) ) = ( [ p ] ( O ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( O ~QG I ) ) )
31 2 opprnsg 
 |-  ( NrmSGrp ` R ) = ( NrmSGrp ` O )
32 4 31 eleqtrdi 
 |-  ( ph -> I e. ( NrmSGrp ` O ) )
33 32 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> I e. ( NrmSGrp ` O ) )
34 13 1 eleqtrdi 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> p e. ( Base ` R ) )
35 14 1 eleqtrdi 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> q e. ( Base ` R ) )
36 eqid 
 |-  ( O /s ( O ~QG I ) ) = ( O /s ( O ~QG I ) )
37 2 1 opprbas 
 |-  B = ( Base ` O )
38 1 37 eqtr3i 
 |-  ( Base ` R ) = ( Base ` O )
39 2 15 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
40 eqid 
 |-  ( +g ` ( O /s ( O ~QG I ) ) ) = ( +g ` ( O /s ( O ~QG I ) ) )
41 36 38 39 40 qusadd 
 |-  ( ( I e. ( NrmSGrp ` O ) /\ p e. ( Base ` R ) /\ q e. ( Base ` R ) ) -> ( [ p ] ( O ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( O ~QG I ) ) = [ ( p ( +g ` R ) q ) ] ( O ~QG I ) )
42 33 34 35 41 syl3anc 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( [ p ] ( O ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( O ~QG I ) ) = [ ( p ( +g ` R ) q ) ] ( O ~QG I ) )
43 30 42 eqtrd 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( [ p ] ( R ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( R ~QG I ) ) = [ ( p ( +g ` R ) q ) ] ( O ~QG I ) )
44 18 19 oveq12d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( X ( +g ` ( O /s ( O ~QG I ) ) ) Y ) = ( [ p ] ( R ~QG I ) ( +g ` ( O /s ( O ~QG I ) ) ) [ q ] ( R ~QG I ) ) )
45 26 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( R ~QG I ) = ( O ~QG I ) )
46 45 eceq2d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> [ ( p ( +g ` R ) q ) ] ( R ~QG I ) = [ ( p ( +g ` R ) q ) ] ( O ~QG I ) )
47 43 44 46 3eqtr4d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( X ( +g ` ( O /s ( O ~QG I ) ) ) Y ) = [ ( p ( +g ` R ) q ) ] ( R ~QG I ) )
48 17 20 47 3eqtr4d 
 |-  ( ( ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) /\ q e. B ) /\ Y = [ q ] ( R ~QG I ) ) -> ( X ( +g ` Q ) Y ) = ( X ( +g ` ( O /s ( O ~QG I ) ) ) Y ) )
49 3 a1i 
 |-  ( ph -> Q = ( R /s ( R ~QG I ) ) )
50 1 a1i 
 |-  ( ph -> B = ( Base ` R ) )
51 ovexd 
 |-  ( ph -> ( R ~QG I ) e. _V )
52 49 50 51 21 qusbas 
 |-  ( ph -> ( B /. ( R ~QG I ) ) = ( Base ` Q ) )
53 5 52 eqtr4id 
 |-  ( ph -> E = ( B /. ( R ~QG I ) ) )
54 7 53 eleqtrd 
 |-  ( ph -> Y e. ( B /. ( R ~QG I ) ) )
55 54 ad2antrr 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> Y e. ( B /. ( R ~QG I ) ) )
56 elqsi 
 |-  ( Y e. ( B /. ( R ~QG I ) ) -> E. q e. B Y = [ q ] ( R ~QG I ) )
57 55 56 syl 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> E. q e. B Y = [ q ] ( R ~QG I ) )
58 48 57 r19.29a 
 |-  ( ( ( ph /\ p e. B ) /\ X = [ p ] ( R ~QG I ) ) -> ( X ( +g ` Q ) Y ) = ( X ( +g ` ( O /s ( O ~QG I ) ) ) Y ) )
59 6 53 eleqtrd 
 |-  ( ph -> X e. ( B /. ( R ~QG I ) ) )
60 elqsi 
 |-  ( X e. ( B /. ( R ~QG I ) ) -> E. p e. B X = [ p ] ( R ~QG I ) )
61 59 60 syl 
 |-  ( ph -> E. p e. B X = [ p ] ( R ~QG I ) )
62 58 61 r19.29a 
 |-  ( ph -> ( X ( +g ` Q ) Y ) = ( X ( +g ` ( O /s ( O ~QG I ) ) ) Y ) )
63 11 62 eqtr3id 
 |-  ( ph -> ( X ( +g ` ( oppR ` Q ) ) Y ) = ( X ( +g ` ( O /s ( O ~QG I ) ) ) Y ) )