Metamath Proof Explorer


Theorem oppggrp

Description: The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypothesis oppgbas.1 O = opp 𝑔 R
Assertion oppggrp R Grp O Grp

Proof

Step Hyp Ref Expression
1 oppgbas.1 O = opp 𝑔 R
2 eqid Base R = Base R
3 1 2 oppgbas Base R = Base O
4 3 a1i R Grp Base R = Base O
5 eqidd R Grp + O = + O
6 eqid 0 R = 0 R
7 1 6 oppgid 0 R = 0 O
8 7 a1i R Grp 0 R = 0 O
9 grpmnd R Grp R Mnd
10 1 oppgmnd R Mnd O Mnd
11 9 10 syl R Grp O Mnd
12 eqid inv g R = inv g R
13 2 12 grpinvcl R Grp x Base R inv g R x Base R
14 eqid + R = + R
15 eqid + O = + O
16 14 1 15 oppgplus inv g R x + O x = x + R inv g R x
17 2 14 6 12 grprinv R Grp x Base R x + R inv g R x = 0 R
18 16 17 syl5eq R Grp x Base R inv g R x + O x = 0 R
19 4 5 8 11 13 18 isgrpd2 R Grp O Grp