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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
opprqus.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
opprqus.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
opprqus.i ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
opprqusplusg.e ⊢ 𝐸 = ( Base ‘ 𝑄 )
opprqusplusg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
opprqusplusg.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
Assertion opprqusplusg ( 𝜑 → ( 𝑋 ( +g ‘ ( oppr ‘ 𝑄 ) ) 𝑌 ) = ( 𝑋 ( +g ‘ ( 𝑂 /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 opprqusplusg.e ⊢ 𝐸 = ( Base ‘ 𝑄 )
6 opprqusplusg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
7 opprqusplusg.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
8 eqid ⊢ ( oppr ‘ 𝑄 ) = ( oppr ‘ 𝑄 )
9 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
10 8 9 oppradd ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ ( oppr ‘ 𝑄 ) )
11 10 oveqi ⊢ ( 𝑋 ( +g ‘ 𝑄 ) 𝑌 ) = ( 𝑋 ( +g ‘ ( oppr ‘ 𝑄 ) ) 𝑌 )
12 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
13 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑝 ∈ 𝐵 )
14 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑞 ∈ 𝐵 )
15 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
16 3 1 15 9 qusadd ⊢ ( ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ 𝑄 ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑅 ~QG 𝐼 ) )
17 12 13 14 16 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ 𝑄 ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑅 ~QG 𝐼 ) )
18 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) )
19 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) )
20 18 19 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( +g ‘ 𝑄 ) 𝑌 ) = ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ 𝑄 ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) )
21 4 elfvexd ⊢ ( 𝜑 → 𝑅 ∈ V )
22 nsgsubg ⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
23 1 subgss ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
24 4 22 23 3syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
25 2 1 oppreqg ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
26 21 24 25 syl2anc ⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
27 26 eceq2d ⊢ ( 𝜑 → [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) = [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) )
28 26 eceq2d ⊢ ( 𝜑 → [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) = [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) )
29 27 28 oveq12d ⊢ ( 𝜑 → ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) = ( [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) ) )
30 29 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) = ( [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) ) )
31 2 opprnsg ⊢ ( NrmSGrp ‘ 𝑅 ) = ( NrmSGrp ‘ 𝑂 )
32 4 31 eleqtrdi ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑂 ) )
33 32 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑂 ) )
34 13 1 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑝 ∈ ( Base ‘ 𝑅 ) )
35 14 1 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑞 ∈ ( Base ‘ 𝑅 ) )
36 eqid ⊢ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) = ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) )
37 2 1 opprbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
38 1 37 eqtr3i ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
39 2 15 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
40 eqid ⊢ ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) = ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) )
41 36 38 39 40 qusadd ⊢ ( ( 𝐼 ∈ ( NrmSGrp ‘ 𝑂 ) ∧ 𝑝 ∈ ( Base ‘ 𝑅 ) ∧ 𝑞 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
42 33 34 35 41 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑝 ] ( 𝑂 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑂 ~QG 𝐼 ) ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
43 30 42 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
44 18 19 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) = ( [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) )
45 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )
46 45 eceq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑅 ~QG 𝐼 ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑂 ~QG 𝐼 ) )
47 43 44 46 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) = [ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ] ( 𝑅 ~QG 𝐼 ) )
48 17 20 47 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( +g ‘ 𝑄 ) 𝑌 ) = ( 𝑋 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )
49 3 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
50 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
51 ovexd ⊢ ( 𝜑 → ( 𝑅 ~QG 𝐼 ) ∈ V )
52 49 50 51 21 qusbas ⊢ ( 𝜑 → ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
53 5 52 eqtr4id ⊢ ( 𝜑 → 𝐸 = ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
54 7 53 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑌 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
56 elqsi ⊢ ( 𝑌 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) )
57 55 56 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑞 ∈ 𝐵 𝑌 = [ 𝑞 ] ( 𝑅 ~QG 𝐼 ) )
58 48 57 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑋 ( +g ‘ 𝑄 ) 𝑌 ) = ( 𝑋 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )
59 6 53 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) )
60 elqsi ⊢ ( 𝑋 ∈ ( 𝐵 / ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑝 ∈ 𝐵 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) )
61 59 60 syl ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐵 𝑋 = [ 𝑝 ] ( 𝑅 ~QG 𝐼 ) )
62 58 61 r19.29a ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑄 ) 𝑌 ) = ( 𝑋 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )
63 11 62 eqtr3id ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ ( oppr ‘ 𝑄 ) ) 𝑌 ) = ( 𝑋 ( +g ‘ ( 𝑂 /s ( 𝑂 ~QG 𝐼 ) ) ) 𝑌 ) )