This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = inv g ⁡ G
Assertion symginv ⊢ F ∈ B → N ⁡ F = F -1

Proof

Step Hyp Ref Expression
1 symggrp.1 ⊢ G = SymGrp ⁡ A
2 symginv.2 ⊢ B = Base G
3 symginv.3 ⊢ N = inv g ⁡ G
4 1 2 elsymgbas2 ⊢ F ∈ B → F ∈ B ↔ F : A ⟶ 1-1 onto A
5 4 ibi ⊢ F ∈ B → F : A ⟶ 1-1 onto A
6 f1ocnv ⊢ F : A ⟶ 1-1 onto A → F -1 : A ⟶ 1-1 onto A
7 5 6 syl ⊢ F ∈ B → F -1 : A ⟶ 1-1 onto A
8 cnvexg ⊢ F ∈ B → F -1 ∈ V
9 1 2 elsymgbas2 ⊢ F -1 ∈ V → F -1 ∈ B ↔ F -1 : A ⟶ 1-1 onto A
10 8 9 syl ⊢ F ∈ B → F -1 ∈ B ↔ F -1 : A ⟶ 1-1 onto A
11 7 10 mpbird ⊢ F ∈ B → F -1 ∈ B
12 eqid ⊢ + G = + G
13 1 2 12 symgov ⊢ F ∈ B ∧ F -1 ∈ B → F + G F -1 = F ∘ F -1
14 11 13 mpdan ⊢ F ∈ B → F + G F -1 = F ∘ F -1
15 f1ococnv2 ⊢ F : A ⟶ 1-1 onto A → F ∘ F -1 = I ↾ A
16 5 15 syl ⊢ F ∈ B → F ∘ F -1 = I ↾ A
17 1 2 elbasfv ⊢ F ∈ B → A ∈ V
18 1 symgid ⊢ A ∈ V → I ↾ A = 0 G
19 17 18 syl ⊢ F ∈ B → I ↾ A = 0 G
20 14 16 19 3eqtrd ⊢ F ∈ B → F + G F -1 = 0 G
21 1 symggrp ⊢ A ∈ V → G ∈ Grp
22 17 21 syl ⊢ F ∈ B → G ∈ Grp
23 id ⊢ F ∈ B → F ∈ B
24 eqid ⊢ 0 G = 0 G
25 2 12 24 3 grpinvid1 ⊢ G ∈ Grp ∧ F ∈ B ∧ F -1 ∈ B → N ⁡ F = F -1 ↔ F + G F -1 = 0 G
26 22 23 11 25 syl3anc ⊢ F ∈ B → N ⁡ F = F -1 ↔ F + G F -1 = 0 G
27 20 26 mpbird ⊢ F ∈ B → N ⁡ F = F -1