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 = ( SymGrp ` A )
	symginv.2	|- B = ( Base ` G )
	symginv.3	|- N = ( invg ` G )
Assertion	symginv	|- ( F e. B -> ( N ` F ) = `' F )

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	|- G = ( SymGrp ` A )
2		symginv.2	|- B = ( Base ` G )
3		symginv.3	|- N = ( invg ` G )
4	1 2	elsymgbas2	|- ( F e. B -> ( F e. B <-> F : A -1-1-onto-> A ) )
5	4	ibi	|- ( F e. B -> F : A -1-1-onto-> A )
6		f1ocnv	|- ( F : A -1-1-onto-> A -> `' F : A -1-1-onto-> A )
7	5 6	syl	|- ( F e. B -> `' F : A -1-1-onto-> A )
8		cnvexg	|- ( F e. B -> `' F e. _V )
9	1 2	elsymgbas2	|- ( `' F e. _V -> ( `' F e. B <-> `' F : A -1-1-onto-> A ) )
10	8 9	syl	|- ( F e. B -> ( `' F e. B <-> `' F : A -1-1-onto-> A ) )
11	7 10	mpbird	|- ( F e. B -> `' F e. B )
12		eqid	|- ( +g ` G ) = ( +g ` G )
13	1 2 12	symgov	|- ( ( F e. B /\ `' F e. B ) -> ( F ( +g ` G ) `' F ) = ( F o. `' F ) )
14	11 13	mpdan	|- ( F e. B -> ( F ( +g ` G ) `' F ) = ( F o. `' F ) )
15		f1ococnv2	|- ( F : A -1-1-onto-> A -> ( F o. `' F ) = ( _I |` A ) )
16	5 15	syl	|- ( F e. B -> ( F o. `' F ) = ( _I |` A ) )
17	1 2	elbasfv	|- ( F e. B -> A e. _V )
18	1	symgid	|- ( A e. _V -> ( _I |` A ) = ( 0g ` G ) )
19	17 18	syl	|- ( F e. B -> ( _I |` A ) = ( 0g ` G ) )
20	14 16 19	3eqtrd	|- ( F e. B -> ( F ( +g ` G ) `' F ) = ( 0g ` G ) )
21	1	symggrp	|- ( A e. _V -> G e. Grp )
22	17 21	syl	|- ( F e. B -> G e. Grp )
23		id	|- ( F e. B -> F e. B )
24		eqid	|- ( 0g ` G ) = ( 0g ` G )
25	2 12 24 3	grpinvid1	|- ( ( G e. Grp /\ F e. B /\ `' F e. B ) -> ( ( N ` F ) = `' F <-> ( F ( +g ` G ) `' F ) = ( 0g ` G ) ) )
26	22 23 11 25	syl3anc	|- ( F e. B -> ( ( N ` F ) = `' F <-> ( F ( +g ` G ) `' F ) = ( 0g ` G ) ) )
27	20 26	mpbird	|- ( F e. B -> ( N ` F ) = `' F )