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 ⊢ 𝑂 = ( 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 𝐼 ) )