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

Metamath Proof Explorer

Theorem oppreqg

Description: Group coset equivalence relation for the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses oppreqg.o ⊢ O = opp r ⁡ R
oppreqg.b ⊢ B = Base R
Assertion oppreqg ⊢ R ∈ V ∧ I ⊆ B → R ~ QG I = O ~ QG I

Proof

Step Hyp Ref Expression
1 oppreqg.o ⊢ O = opp r ⁡ R
2 oppreqg.b ⊢ B = Base R
3 eqid ⊢ inv g ⁡ R = inv g ⁡ R
4 eqid ⊢ + R = + R
5 eqid ⊢ R ~ QG I = R ~ QG I
6 2 3 4 5 eqgfval ⊢ R ∈ V ∧ I ⊆ B → R ~ QG I = x y | x y ⊆ B ∧ inv g ⁡ R ⁡ x + R y ∈ I
7 1 fvexi ⊢ O ∈ V
8 1 2 opprbas ⊢ B = Base O
9 1 3 opprneg ⊢ inv g ⁡ R = inv g ⁡ O
10 1 4 oppradd ⊢ + R = + O
11 eqid ⊢ O ~ QG I = O ~ QG I
12 8 9 10 11 eqgfval ⊢ O ∈ V ∧ I ⊆ B → O ~ QG I = x y | x y ⊆ B ∧ inv g ⁡ R ⁡ x + R y ∈ I
13 7 12 mpan ⊢ I ⊆ B → O ~ QG I = x y | x y ⊆ B ∧ inv g ⁡ R ⁡ x + R y ∈ I
14 13 adantl ⊢ R ∈ V ∧ I ⊆ B → O ~ QG I = x y | x y ⊆ B ∧ inv g ⁡ R ⁡ x + R y ∈ I
15 6 14 eqtr4d ⊢ R ∈ V ∧ I ⊆ B → R ~ QG I = O ~ QG I