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\left(R\right)$$
	oppreqg.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	oppreqg	$$⊢\left(R\in V\wedge I\subseteq B\right)\to R{~}_{\mathit{QG}}I=O{~}_{\mathit{QG}}I$$

Proof

Step	Hyp	Ref	Expression
1		oppreqg.o	$$⊢O={opp}_r\left(R\right)$$
2		oppreqg.b	$$⊢B={\mathrm{Base}}_R$$
3		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
4		eqid	$$⊢{+}_R={+}_R$$
5		eqid	$$⊢R{~}_{\mathit{QG}}I=R{~}_{\mathit{QG}}I$$
6	2 3 4 5	eqgfval	$$⊢\left(R\in V\wedge I\subseteq B\right)\to R{~}_{\mathit{QG}}I=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge {inv}_g\left(R\right)\left(x\right){+}_{R}y\in I\right)\right\}$$
7	1	fvexi	$$⊢O\in \mathrm{V}$$
8	1 2	opprbas	$$⊢B={\mathrm{Base}}_O$$
9	1 3	opprneg	$$⊢{inv}_g\left(R\right)={inv}_g\left(O\right)$$
10	1 4	oppradd	$$⊢{+}_R={+}_O$$
11		eqid	$$⊢O{~}_{\mathit{QG}}I=O{~}_{\mathit{QG}}I$$
12	8 9 10 11	eqgfval	$$⊢\left(O\in \mathrm{V}\wedge I\subseteq B\right)\to O{~}_{\mathit{QG}}I=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge {inv}_g\left(R\right)\left(x\right){+}_{R}y\in I\right)\right\}$$
13	7 12	mpan	$$⊢I\subseteq B\to O{~}_{\mathit{QG}}I=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge {inv}_g\left(R\right)\left(x\right){+}_{R}y\in I\right)\right\}$$
14	13	adantl	$$⊢\left(R\in V\wedge I\subseteq B\right)\to O{~}_{\mathit{QG}}I=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge {inv}_g\left(R\right)\left(x\right){+}_{R}y\in I\right)\right\}$$
15	6 14	eqtr4d	$$⊢\left(R\in V\wedge I\subseteq B\right)\to R{~}_{\mathit{QG}}I=O{~}_{\mathit{QG}}I$$