This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐼 ) ) ) )