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 O = opp 𝑔 R
oppginv.2 I = inv g R
Assertion oppginv R Grp I = inv g O

Proof

Step Hyp Ref Expression
1 oppgbas.1 O = opp 𝑔 R
2 oppginv.2 I = inv g R
3 eqid Base R = Base R
4 3 2 grpinvf R Grp I : Base R Base R
5 eqid + R = + R
6 eqid + O = + O
7 5 1 6 oppgplus I x + O x = x + R I x
8 eqid 0 R = 0 R
9 3 5 8 2 grprinv R Grp x Base R x + R I x = 0 R
10 7 9 syl5eq R Grp x Base R I x + O x = 0 R
11 10 ralrimiva R Grp x Base R I x + O x = 0 R
12 1 oppggrp R Grp O Grp
13 1 3 oppgbas Base R = Base O
14 1 8 oppgid 0 R = 0 O
15 eqid inv g O = inv g O
16 13 6 14 15 isgrpinv O Grp I : Base R Base R x Base R I x + O x = 0 R inv g O = I
17 12 16 syl R Grp I : Base R Base R x Base R I x + O x = 0 R inv g O = I
18 4 11 17 mpbi2and R Grp inv g O = I
19 18 eqcomd R Grp I = inv g O