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 \in Grp \to O \in Grp$

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 \in Grp \to {Base}_{R} = {Base}_{O}$
5		eqidd	$⊢ R \in Grp \to +_{O} = +_{O}$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	1 6	oppgid	$⊢ 0_{R} = 0_{O}$
8	7	a1i	$⊢ R \in Grp \to 0_{R} = 0_{O}$
9		grpmnd	$⊢ R \in Grp \to R \in Mnd$
10	1	oppgmnd	$⊢ R \in Mnd \to O \in Mnd$
11	9 10	syl	$⊢ R \in Grp \to O \in Mnd$
12		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
13	2 12	grpinvcl	$⊢ (R \in Grp \land x \in {Base}_{R}) \to {inv}_{g} (R) (x) \in {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 \in Grp \land x \in {Base}_{R}) \to x +_{R} {inv}_{g} (R) (x) = 0_{R}$
18	16 17	eqtrid	$⊢ (R \in Grp \land x \in {Base}_{R}) \to {inv}_{g} (R) (x) +_{O} x = 0_{R}$
19	4 5 8 11 13 18	isgrpd2	$⊢ R \in Grp \to O \in Grp$

Metamath Proof Explorer