Theorem oppggrpb

Description: Bidirectional form of oppggrp . (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypothesis	oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
Assertion	oppggrpb	$$⊢R\in \mathrm{Grp}\leftrightarrow O\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
2	1	oppggrp	$$⊢R\in \mathrm{Grp}\to O\in \mathrm{Grp}$$
3		eqid	$$⊢{opp}_{𝑔}\left(O\right)={opp}_{𝑔}\left(O\right)$$
4	3	oppggrp	$$⊢O\in \mathrm{Grp}\to {opp}_{𝑔}\left(O\right)\in \mathrm{Grp}$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	1 5	oppgbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
7	3 6	oppgbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_{𝑔}\left(O\right)}$$
8	7	a1i	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_{𝑔}\left(O\right)}$$
9		eqidd	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
10		eqid	$$⊢{+}_O={+}_O$$
11		eqid	$$⊢{+}_{{opp}_{𝑔}\left(O\right)}={+}_{{opp}_{𝑔}\left(O\right)}$$
12	10 3 11	oppgplus	$$⊢x{+}_{{opp}_{𝑔}\left(O\right)}y=y{+}_{O}x$$
13		eqid	$$⊢{+}_R={+}_R$$
14	13 1 10	oppgplus	$$⊢y{+}_{O}x=x{+}_{R}y$$
15	12 14	eqtri	$$⊢x{+}_{{opp}_{𝑔}\left(O\right)}y=x{+}_{R}y$$
16	15	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{+}_{{opp}_{𝑔}\left(O\right)}y=x{+}_{R}y$$
17	8 9 16	grppropd	$$⊢\top \to \left({opp}_{𝑔}\left(O\right)\in \mathrm{Grp}\leftrightarrow R\in \mathrm{Grp}\right)$$
18	17	mptru	$$⊢{opp}_{𝑔}\left(O\right)\in \mathrm{Grp}\leftrightarrow R\in \mathrm{Grp}$$
19	4 18	sylib	$$⊢O\in \mathrm{Grp}\to R\in \mathrm{Grp}$$
20	2 19	impbii	$$⊢R\in \mathrm{Grp}\leftrightarrow O\in \mathrm{Grp}$$