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 )

Metamath Proof Explorer

Theorem symginv

Proof