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 𝐵 = ( Base ‘ 𝑅 )
opprqus.o 𝑂 = ( oppr𝑅 )
opprqus.q 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
opprqus.i ( 𝜑𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
Assertion opprqus0g ( 𝜑 → ( 0g ‘ ( oppr𝑄 ) ) = ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 opprqus.b 𝐵 = ( Base ‘ 𝑅 )
2 opprqus.o 𝑂 = ( oppr𝑅 )
3 opprqus.q 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
4 opprqus.i ( 𝜑𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
5 4 elfvexd ( 𝜑𝑅 ∈ V )
6 nsgsubg ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
7 1 subgss ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼𝐵 )
8 4 6 7 3syl ( 𝜑𝐼𝐵 )
9 1 2 3 5 8 opprqusbas ( 𝜑 → ( Base ‘ ( oppr𝑄 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
10 9 adantr ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( Base ‘ ( oppr𝑄 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )
11 4 ad2antrr ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
12 eqid ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
13 simpr ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) )
14 eqid ( oppr𝑄 ) = ( oppr𝑄 )
15 14 12 opprbas ( Base ‘ 𝑄 ) = ( Base ‘ ( oppr𝑄 ) )
16 15 eqcomi ( Base ‘ ( oppr𝑄 ) ) = ( Base ‘ 𝑄 )
17 13 16 eleqtrdi ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝑒 ∈ ( Base ‘ 𝑄 ) )
18 17 adantr ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝑒 ∈ ( Base ‘ 𝑄 ) )
19 simpr ( ( 𝜑𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) )
20 19 16 eleqtrdi ( ( 𝜑𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑄 ) )
21 20 adantlr ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑄 ) )
22 1 2 3 11 12 18 21 opprqusplusg ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) )
23 22 eqeq1d ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ↔ ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ) )
24 1 2 3 11 12 21 18 opprqusplusg ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) )
25 24 eqeq1d ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ↔ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) )
26 23 25 anbi12d ( ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) ∧ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) )
27 10 26 raleqbidva ( ( 𝜑𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) )
28 27 pm5.32da ( 𝜑 → ( ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) ) )
29 9 eleq2d ( 𝜑 → ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ↔ 𝑒 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ) )
30 29 anbi1d ( 𝜑 → ( ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) ) )
31 28 30 bitrd ( 𝜑 → ( ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) ) )
32 31 iotabidv ( 𝜑 → ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ) ) ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) ) )
33 eqid ( +g𝑄 ) = ( +g𝑄 )
34 14 33 oppradd ( +g𝑄 ) = ( +g ‘ ( oppr𝑄 ) )
35 34 eqcomi ( +g ‘ ( oppr𝑄 ) ) = ( +g𝑄 )
36 eqid ( 0g𝑄 ) = ( 0g𝑄 )
37 14 36 oppr0 ( 0g𝑄 ) = ( 0g ‘ ( oppr𝑄 ) )
38 37 eqcomi ( 0g ‘ ( oppr𝑄 ) ) = ( 0g𝑄 )
39 16 35 38 grpidval ( 0g ‘ ( oppr𝑄 ) ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ ( oppr𝑄 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( oppr𝑄 ) ) ( ( 𝑒 ( +g ‘ ( oppr𝑄 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( oppr𝑄 ) ) 𝑒 ) = 𝑥 ) ) )
40 eqid ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
41 eqid ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
42 eqid ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
43 40 41 42 grpidval ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) ( ( 𝑒 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑒 ) = 𝑥 ) ) )
44 32 39 43 3eqtr4g ( 𝜑 → ( 0g ‘ ( oppr𝑄 ) ) = ( 0g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) )