Theorem oppreqg

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

	Ref	Expression
Hypotheses	oppreqg.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	oppreqg.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	oppreqg	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		oppreqg.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2		oppreqg.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
4		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
5		eqid	⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
6	2 3 4 5	eqgfval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑅 ~QG 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) } )
7	1	fvexi	⊢ 𝑂 ∈ V
8	1 2	opprbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
9	1 3	opprneg	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑂 )
10	1 4	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
11		eqid	⊢ ( 𝑂 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 )
12	8 9 10 11	eqgfval	⊢ ( ( 𝑂 ∈ V ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑂 ~QG 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) } )
13	7 12	mpan	⊢ ( 𝐼 ⊆ 𝐵 → ( 𝑂 ~QG 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) } )
14	13	adantl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑂 ~QG 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) } )
15	6 14	eqtr4d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑂 ~QG 𝐼 ) )