Theorem invoppggim

Description: The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypotheses	invoppggim.o	$$⊢O={opp}_{𝑔}\left(G\right)$$
	invoppggim.i	$$⊢I={inv}_g\left(G\right)$$
Assertion	invoppggim	$$⊢G\in \mathrm{Grp}\to I\in \left(G\mathrm{GrpIso}O\right)$$

Proof

Step	Hyp	Ref	Expression
1		invoppggim.o	$$⊢O={opp}_{𝑔}\left(G\right)$$
2		invoppggim.i	$$⊢I={inv}_g\left(G\right)$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	1 3	oppgbas	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_O$$
5		eqid	$$⊢{+}_G={+}_G$$
6		eqid	$$⊢{+}_O={+}_O$$
7		id	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Grp}$$
8	1	oppggrp	$$⊢G\in \mathrm{Grp}\to O\in \mathrm{Grp}$$
9	3 2	grpinvf	$$⊢G\in \mathrm{Grp}\to I:{\mathrm{Base}}_G⟶{\mathrm{Base}}_G$$
10	3 5 2	grpinvadd	$$⊢\left(G\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\to I\left(x{+}_{G}y\right)=I\left(y\right){+}_{G}I\left(x\right)$$
11	10	3expb	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to I\left(x{+}_{G}y\right)=I\left(y\right){+}_{G}I\left(x\right)$$
12	5 1 6	oppgplus	$$⊢I\left(x\right){+}_{O}I\left(y\right)=I\left(y\right){+}_{G}I\left(x\right)$$
13	11 12	eqtr4di	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to I\left(x{+}_{G}y\right)=I\left(x\right){+}_{O}I\left(y\right)$$
14	3 4 5 6 7 8 9 13	isghmd	$$⊢G\in \mathrm{Grp}\to I\in \left(G\mathrm{GrpHom}O\right)$$
15	3 2 7	grpinvf1o	$$⊢G\in \mathrm{Grp}\to I:{\mathrm{Base}}_G\underset{1-1\; onto}{⟶}{\mathrm{Base}}_G$$
16	3 4	isgim	$$⊢I\in \left(G\mathrm{GrpIso}O\right)\leftrightarrow \left(I\in \left(G\mathrm{GrpHom}O\right)\wedge I:{\mathrm{Base}}_G\underset{1-1\; onto}{⟶}{\mathrm{Base}}_G\right)$$
17	14 15 16	sylanbrc	$$⊢G\in \mathrm{Grp}\to I\in \left(G\mathrm{GrpIso}O\right)$$