# 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}=\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}↔{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}↔{{F}}^{-1}:{A}\underset{1-1 onto}{⟶}{A}\right)$
10 8 9 syl ${⊢}{F}\in {B}\to \left({{F}}^{-1}\in {B}↔{{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}↾}_{{A}}$
16 5 15 syl ${⊢}{F}\in {B}\to {F}\circ {{F}}^{-1}={\mathrm{I}↾}_{{A}}$
17 1 2 elbasfv ${⊢}{F}\in {B}\to {A}\in \mathrm{V}$
18 1 symgid ${⊢}{A}\in \mathrm{V}\to {\mathrm{I}↾}_{{A}}={0}_{{G}}$
19 17 18 syl ${⊢}{F}\in {B}\to {\mathrm{I}↾}_{{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}↔{F}{+}_{{G}}{{F}}^{-1}={0}_{{G}}\right)$
26 22 23 11 25 syl3anc ${⊢}{F}\in {B}\to \left({N}\left({F}\right)={{F}}^{-1}↔{F}{+}_{{G}}{{F}}^{-1}={0}_{{G}}\right)$
27 20 26 mpbird ${⊢}{F}\in {B}\to {N}\left({F}\right)={{F}}^{-1}$