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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symginv.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
	symginv.3	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	symginv	⊢ ( 𝐹 ∈ 𝐵 → ( 𝑁 ‘ 𝐹 ) = ◡ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symginv.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		symginv.3	⊢ 𝑁 = ( invg ‘ 𝐺 )
4	1 2	elsymgbas2	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )
5	4	ibi	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
6		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
7	5 6	syl	⊢ ( 𝐹 ∈ 𝐵 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
8		cnvexg	⊢ ( 𝐹 ∈ 𝐵 → ◡ 𝐹 ∈ V )
9	1 2	elsymgbas2	⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 ∈ 𝐵 ↔ ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )
10	8 9	syl	⊢ ( 𝐹 ∈ 𝐵 → ( ◡ 𝐹 ∈ 𝐵 ↔ ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )
11	7 10	mpbird	⊢ ( 𝐹 ∈ 𝐵 → ◡ 𝐹 ∈ 𝐵 )
12		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13	1 2 12	symgov	⊢ ( ( 𝐹 ∈ 𝐵 ∧ ◡ 𝐹 ∈ 𝐵 ) → ( 𝐹 ( +g ‘ 𝐺 ) ◡ 𝐹 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
14	11 13	mpdan	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ( +g ‘ 𝐺 ) ◡ 𝐹 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
15		f1ococnv2	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝐴 ) )
16	5 15	syl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝐴 ) )
17	1 2	elbasfv	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 ∈ V )
18	1	symgid	⊢ ( 𝐴 ∈ V → ( I ↾ 𝐴 ) = ( 0g ‘ 𝐺 ) )
19	17 18	syl	⊢ ( 𝐹 ∈ 𝐵 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝐺 ) )
20	14 16 19	3eqtrd	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐹 ( +g ‘ 𝐺 ) ◡ 𝐹 ) = ( 0g ‘ 𝐺 ) )
21	1	symggrp	⊢ ( 𝐴 ∈ V → 𝐺 ∈ Grp )
22	17 21	syl	⊢ ( 𝐹 ∈ 𝐵 → 𝐺 ∈ Grp )
23		id	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 )
24		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
25	2 12 24 3	grpinvid1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ ◡ 𝐹 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝐹 ) = ◡ 𝐹 ↔ ( 𝐹 ( +g ‘ 𝐺 ) ◡ 𝐹 ) = ( 0g ‘ 𝐺 ) ) )
26	22 23 11 25	syl3anc	⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑁 ‘ 𝐹 ) = ◡ 𝐹 ↔ ( 𝐹 ( +g ‘ 𝐺 ) ◡ 𝐹 ) = ( 0g ‘ 𝐺 ) ) )
27	20 26	mpbird	⊢ ( 𝐹 ∈ 𝐵 → ( 𝑁 ‘ 𝐹 ) = ◡ 𝐹 )