Metamath Proof Explorer

Theorem opprqus0g

Description: The group identity element of the quotient of the opposite ring is the same as the group identity element 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 ) )
Assertion opprqus0g 
|- ( ph -> ( 0g ` ( oppR ` Q ) ) = ( 0g ` ( O /s ( O ~QG I ) ) ) )

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 4 elfvexd 
 |-  ( ph -> R e. _V )
6 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
7 1 subgss 
 |-  ( I e. ( SubGrp ` R ) -> I C_ B )
8 4 6 7 3syl 
 |-  ( ph -> I C_ B )
9 1 2 3 5 8 opprqusbas 
 |-  ( ph -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
10 9 adantr 
 |-  ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) -> ( Base ` ( oppR ` Q ) ) = ( Base ` ( O /s ( O ~QG I ) ) ) )
11 4 ad2antrr 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> I e. ( NrmSGrp ` R ) )
12 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
13 simpr 
 |-  ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) -> e e. ( Base ` ( oppR ` Q ) ) )
14 eqid 
 |-  ( oppR ` Q ) = ( oppR ` Q )
15 14 12 opprbas 
 |-  ( Base ` Q ) = ( Base ` ( oppR ` Q ) )
16 15 eqcomi 
 |-  ( Base ` ( oppR ` Q ) ) = ( Base ` Q )
17 13 16 eleqtrdi 
 |-  ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) -> e e. ( Base ` Q ) )
18 17 adantr 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> e e. ( Base ` Q ) )
19 simpr 
 |-  ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) -> x e. ( Base ` ( oppR ` Q ) ) )
20 19 16 eleqtrdi 
 |-  ( ( ph /\ x e. ( Base ` ( oppR ` Q ) ) ) -> x e. ( Base ` Q ) )
21 20 adantlr 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> x e. ( Base ` Q ) )
22 1 2 3 11 12 18 21 opprqusplusg 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> ( e ( +g ` ( oppR ` Q ) ) x ) = ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) )
23 22 eqeq1d 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> ( ( e ( +g ` ( oppR ` Q ) ) x ) = x <-> ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x ) )
24 1 2 3 11 12 21 18 opprqusplusg 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> ( x ( +g ` ( oppR ` Q ) ) e ) = ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) )
25 24 eqeq1d 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> ( ( x ( +g ` ( oppR ` Q ) ) e ) = x <-> ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) )
26 23 25 anbi12d 
 |-  ( ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) /\ x e. ( Base ` ( oppR ` Q ) ) ) -> ( ( ( e ( +g ` ( oppR ` Q ) ) x ) = x /\ ( x ( +g ` ( oppR ` Q ) ) e ) = x ) <-> ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) )
27 10 26 raleqbidva 
 |-  ( ( ph /\ e e. ( Base ` ( oppR ` Q ) ) ) -> ( A. x e. ( Base ` ( oppR ` Q ) ) ( ( e ( +g ` ( oppR ` Q ) ) x ) = x /\ ( x ( +g ` ( oppR ` Q ) ) e ) = x ) <-> A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) )
28 27 pm5.32da 
 |-  ( ph -> ( ( e e. ( Base ` ( oppR ` Q ) ) /\ A. x e. ( Base ` ( oppR ` Q ) ) ( ( e ( +g ` ( oppR ` Q ) ) x ) = x /\ ( x ( +g ` ( oppR ` Q ) ) e ) = x ) ) <-> ( e e. ( Base ` ( oppR ` Q ) ) /\ A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) ) )
29 9 eleq2d 
 |-  ( ph -> ( e e. ( Base ` ( oppR ` Q ) ) <-> e e. ( Base ` ( O /s ( O ~QG I ) ) ) ) )
30 29 anbi1d 
 |-  ( ph -> ( ( e e. ( Base ` ( oppR ` Q ) ) /\ A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) <-> ( e e. ( Base ` ( O /s ( O ~QG I ) ) ) /\ A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) ) )
31 28 30 bitrd 
 |-  ( ph -> ( ( e e. ( Base ` ( oppR ` Q ) ) /\ A. x e. ( Base ` ( oppR ` Q ) ) ( ( e ( +g ` ( oppR ` Q ) ) x ) = x /\ ( x ( +g ` ( oppR ` Q ) ) e ) = x ) ) <-> ( e e. ( Base ` ( O /s ( O ~QG I ) ) ) /\ A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) ) )
32 31 iotabidv 
 |-  ( ph -> ( iota e ( e e. ( Base ` ( oppR ` Q ) ) /\ A. x e. ( Base ` ( oppR ` Q ) ) ( ( e ( +g ` ( oppR ` Q ) ) x ) = x /\ ( x ( +g ` ( oppR ` Q ) ) e ) = x ) ) ) = ( iota e ( e e. ( Base ` ( O /s ( O ~QG I ) ) ) /\ A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) ) )
33 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
34 14 33 oppradd 
 |-  ( +g ` Q ) = ( +g ` ( oppR ` Q ) )
35 34 eqcomi 
 |-  ( +g ` ( oppR ` Q ) ) = ( +g ` Q )
36 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
37 14 36 oppr0 
 |-  ( 0g ` Q ) = ( 0g ` ( oppR ` Q ) )
38 37 eqcomi 
 |-  ( 0g ` ( oppR ` Q ) ) = ( 0g ` Q )
39 16 35 38 grpidval 
 |-  ( 0g ` ( oppR ` Q ) ) = ( iota e ( e e. ( Base ` ( oppR ` Q ) ) /\ A. x e. ( Base ` ( oppR ` Q ) ) ( ( e ( +g ` ( oppR ` Q ) ) x ) = x /\ ( x ( +g ` ( oppR ` Q ) ) e ) = x ) ) )
40 eqid 
 |-  ( Base ` ( O /s ( O ~QG I ) ) ) = ( Base ` ( O /s ( O ~QG I ) ) )
41 eqid 
 |-  ( +g ` ( O /s ( O ~QG I ) ) ) = ( +g ` ( O /s ( O ~QG I ) ) )
42 eqid 
 |-  ( 0g ` ( O /s ( O ~QG I ) ) ) = ( 0g ` ( O /s ( O ~QG I ) ) )
43 40 41 42 grpidval 
 |-  ( 0g ` ( O /s ( O ~QG I ) ) ) = ( iota e ( e e. ( Base ` ( O /s ( O ~QG I ) ) ) /\ A. x e. ( Base ` ( O /s ( O ~QG I ) ) ) ( ( e ( +g ` ( O /s ( O ~QG I ) ) ) x ) = x /\ ( x ( +g ` ( O /s ( O ~QG I ) ) ) e ) = x ) ) )
44 32 39 43 3eqtr4g 
 |-  ( ph -> ( 0g ` ( oppR ` Q ) ) = ( 0g ` ( O /s ( O ~QG I ) ) ) )