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

Metamath Proof Explorer

Theorem oppginv

Description: Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypotheses oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
oppginv.2 ⊢ 𝐼 = ( invg ‘ 𝑅 )
Assertion oppginv ( 𝑅 ∈ Grp → 𝐼 = ( invg ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
2 oppginv.2 ⊢ 𝐼 = ( invg ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 3 2 grpinvf ⊢ ( 𝑅 ∈ Grp → 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
7 5 1 6 oppgplus ⊢ ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑥 ) )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 3 5 8 2 grprinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) ( 𝐼 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
10 7 9 eqtrid ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
11 10 ralrimiva ⊢ ( 𝑅 ∈ Grp → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
12 1 oppggrp ⊢ ( 𝑅 ∈ Grp → 𝑂 ∈ Grp )
13 1 3 oppgbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
14 1 8 oppgid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑂 )
15 eqid ⊢ ( invg ‘ 𝑂 ) = ( invg ‘ 𝑂 )
16 13 6 14 15 isgrpinv ⊢ ( 𝑂 ∈ Grp → ( ( 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( invg ‘ 𝑂 ) = 𝐼 ) )
17 12 16 syl ⊢ ( 𝑅 ∈ Grp → ( ( 𝐼 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( invg ‘ 𝑂 ) = 𝐼 ) )
18 4 11 17 mpbi2and ⊢ ( 𝑅 ∈ Grp → ( invg ‘ 𝑂 ) = 𝐼 )
19 18 eqcomd ⊢ ( 𝑅 ∈ Grp → 𝐼 = ( invg ‘ 𝑂 ) )