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}_{𝑔}\left(R\right)$$
Assertion	oppggrp	$$⊢R\in \mathrm{Grp}\to O\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3	1 2	oppgbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
4	3	a1i	$$⊢R\in \mathrm{Grp}\to {\mathrm{Base}}_R={\mathrm{Base}}_O$$
5		eqidd	$$⊢R\in \mathrm{Grp}\to {+}_O={+}_O$$
6		eqid	$$⊢0_R=0_R$$
7	1 6	oppgid	$$⊢0_R=0_O$$
8	7	a1i	$$⊢R\in \mathrm{Grp}\to 0_R=0_O$$
9		grpmnd	$$⊢R\in \mathrm{Grp}\to R\in \mathrm{Mnd}$$
10	1	oppgmnd	$$⊢R\in \mathrm{Mnd}\to O\in \mathrm{Mnd}$$
11	9 10	syl	$$⊢R\in \mathrm{Grp}\to O\in \mathrm{Mnd}$$
12		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
13	2 12	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to {inv}_g\left(R\right)\left(x\right)\in {\mathrm{Base}}_R$$
14		eqid	$$⊢{+}_R={+}_R$$
15		eqid	$$⊢{+}_O={+}_O$$
16	14 1 15	oppgplus	$$⊢{inv}_g\left(R\right)\left(x\right){+}_{O}x=x{+}_R{inv}_g\left(R\right)\left(x\right)$$
17	2 14 6 12	grprinv	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to x{+}_R{inv}_g\left(R\right)\left(x\right)=0_R$$
18	16 17	syl5eq	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to {inv}_g\left(R\right)\left(x\right){+}_{O}x=0_R$$
19	4 5 8 11 13 18	isgrpd2	$$⊢R\in \mathrm{Grp}\to O\in \mathrm{Grp}$$