Theorem symginv

Description: The group inverse in the symmetric group corresponds to the functional inverse. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symginv.2	$$⊢B={\mathrm{Base}}_G$$
	symginv.3	$$⊢N={inv}_g\left(G\right)$$
Assertion	symginv	$$⊢F\in B\to N\left(F\right)=F^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symginv.2	$$⊢B={\mathrm{Base}}_G$$
3		symginv.3	$$⊢N={inv}_g\left(G\right)$$
4	1 2	elsymgbas2	$$⊢F\in B\to \left(F\in B\leftrightarrow F:A\underset{1-1\; onto}{⟶}A\right)$$
5	4	ibi	$$⊢F\in B\to F:A\underset{1-1\; onto}{⟶}A$$
6		f1ocnv	$$⊢F:A\underset{1-1\; onto}{⟶}A\to F^{-1}:A\underset{1-1\; onto}{⟶}A$$
7	5 6	syl	$$⊢F\in B\to F^{-1}:A\underset{1-1\; onto}{⟶}A$$
8		cnvexg	$$⊢F\in B\to F^{-1}\in \mathrm{V}$$
9	1 2	elsymgbas2	$$⊢F^{-1}\in \mathrm{V}\to \left(F^{-1}\in B\leftrightarrow F^{-1}:A\underset{1-1\; onto}{⟶}A\right)$$
10	8 9	syl	$$⊢F\in B\to \left(F^{-1}\in B\leftrightarrow F^{-1}:A\underset{1-1\; onto}{⟶}A\right)$$
11	7 10	mpbird	$$⊢F\in B\to F^{-1}\in B$$
12		eqid	$$⊢{+}_G={+}_G$$
13	1 2 12	symgov	$$⊢\left(F\in B\wedge F^{-1}\in B\right)\to F{+}_G{F}^{-1}=F\circ F^{-1}$$
14	11 13	mpdan	$$⊢F\in B\to F{+}_G{F}^{-1}=F\circ F^{-1}$$
15		f1ococnv2	$$⊢F:A\underset{1-1\; onto}{⟶}A\to F\circ F^{-1}={\mathrm{I}\upharpoonright }_A$$
16	5 15	syl	$$⊢F\in B\to F\circ F^{-1}={\mathrm{I}\upharpoonright }_A$$
17	1 2	elbasfv	$$⊢F\in B\to A\in \mathrm{V}$$
18	1	symgid	$$⊢A\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_A=0_G$$
19	17 18	syl	$$⊢F\in B\to {\mathrm{I}\upharpoonright }_A=0_G$$
20	14 16 19	3eqtrd	$$⊢F\in B\to F{+}_G{F}^{-1}=0_G$$
21	1	symggrp	$$⊢A\in \mathrm{V}\to G\in \mathrm{Grp}$$
22	17 21	syl	$$⊢F\in B\to G\in \mathrm{Grp}$$
23		id	$$⊢F\in B\to F\in B$$
24		eqid	$$⊢0_G=0_G$$
25	2 12 24 3	grpinvid1	$$⊢\left(G\in \mathrm{Grp}\wedge F\in B\wedge F^{-1}\in B\right)\to \left(N\left(F\right)=F^{-1}\leftrightarrow F{+}_G{F}^{-1}=0_G\right)$$
26	22 23 11 25	syl3anc	$$⊢F\in B\to \left(N\left(F\right)=F^{-1}\leftrightarrow F{+}_G{F}^{-1}=0_G\right)$$
27	20 26	mpbird	$$⊢F\in B\to N\left(F\right)=F^{-1}$$