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}_{𝑔}\left(R\right)$$
	oppginv.2	$$⊢I={inv}_g\left(R\right)$$
Assertion	oppginv	$$⊢R\in \mathrm{Grp}\to I={inv}_g\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
2		oppginv.2	$$⊢I={inv}_g\left(R\right)$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3 2	grpinvf	$$⊢R\in \mathrm{Grp}\to I:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
5		eqid	$$⊢{+}_R={+}_R$$
6		eqid	$$⊢{+}_O={+}_O$$
7	5 1 6	oppgplus	$$⊢I\left(x\right){+}_{O}x=x{+}_{R}I\left(x\right)$$
8		eqid	$$⊢0_R=0_R$$
9	3 5 8 2	grprinv	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to x{+}_{R}I\left(x\right)=0_R$$
10	7 9	syl5eq	$$⊢\left(R\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_R\right)\to I\left(x\right){+}_{O}x=0_R$$
11	10	ralrimiva	$$⊢R\in \mathrm{Grp}\to \forall x\in {\mathrm{Base}}_{R}I\left(x\right){+}_{O}x=0_R$$
12	1	oppggrp	$$⊢R\in \mathrm{Grp}\to O\in \mathrm{Grp}$$
13	1 3	oppgbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
14	1 8	oppgid	$$⊢0_R=0_O$$
15		eqid	$$⊢{inv}_g\left(O\right)={inv}_g\left(O\right)$$
16	13 6 14 15	isgrpinv	$$⊢O\in \mathrm{Grp}\to \left(\left(I:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_{R}I\left(x\right){+}_{O}x=0_R\right)\leftrightarrow {inv}_g\left(O\right)=I\right)$$
17	12 16	syl	$$⊢R\in \mathrm{Grp}\to \left(\left(I:{\mathrm{Base}}_R⟶{\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_{R}I\left(x\right){+}_{O}x=0_R\right)\leftrightarrow {inv}_g\left(O\right)=I\right)$$
18	4 11 17	mpbi2and	$$⊢R\in \mathrm{Grp}\to {inv}_g\left(O\right)=I$$
19	18	eqcomd	$$⊢R\in \mathrm{Grp}\to I={inv}_g\left(O\right)$$