# Metamath Proof Explorer

## Theorem symggrp

Description: The symmetric group on a set A is a group. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 28-Jan-2024)

Ref Expression
Hypothesis symggrp.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
Assertion symggrp ${⊢}{A}\in {V}\to {G}\in \mathrm{Grp}$

### Proof

Step Hyp Ref Expression
1 symggrp.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 eqidd ${⊢}{A}\in {V}\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
3 eqidd ${⊢}{A}\in {V}\to {+}_{{G}}={+}_{{G}}$
4 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
5 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
6 1 4 5 symgcl ${⊢}\left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}{+}_{{G}}{y}\in {\mathrm{Base}}_{{G}}$
7 6 3adant1 ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\to {x}{+}_{{G}}{y}\in {\mathrm{Base}}_{{G}}$
8 1 4 5 symgcl ${⊢}\left({f}\in {\mathrm{Base}}_{{G}}\wedge {g}\in {\mathrm{Base}}_{{G}}\right)\to {f}{+}_{{G}}{g}\in {\mathrm{Base}}_{{G}}$
9 1 4 5 symgov ${⊢}\left({f}\in {\mathrm{Base}}_{{G}}\wedge {g}\in {\mathrm{Base}}_{{G}}\right)\to {f}{+}_{{G}}{g}={f}\circ {g}$
10 8 9 symggrplem ${⊢}\left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\to \left({x}{+}_{{G}}{y}\right){+}_{{G}}{z}={x}{+}_{{G}}\left({y}{+}_{{G}}{z}\right)$
11 10 adantl ${⊢}\left({A}\in {V}\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\wedge {z}\in {\mathrm{Base}}_{{G}}\right)\right)\to \left({x}{+}_{{G}}{y}\right){+}_{{G}}{z}={x}{+}_{{G}}\left({y}{+}_{{G}}{z}\right)$
12 1 idresperm ${⊢}{A}\in {V}\to {\mathrm{I}↾}_{{A}}\in {\mathrm{Base}}_{{G}}$
13 1 4 5 symgov ${⊢}\left({\mathrm{I}↾}_{{A}}\in {\mathrm{Base}}_{{G}}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to \left({\mathrm{I}↾}_{{A}}\right){+}_{{G}}{x}=\left({\mathrm{I}↾}_{{A}}\right)\circ {x}$
14 12 13 sylan ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to \left({\mathrm{I}↾}_{{A}}\right){+}_{{G}}{x}=\left({\mathrm{I}↾}_{{A}}\right)\circ {x}$
15 1 4 elsymgbas ${⊢}{A}\in {V}\to \left({x}\in {\mathrm{Base}}_{{G}}↔{x}:{A}\underset{1-1 onto}{⟶}{A}\right)$
16 15 biimpa ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {x}:{A}\underset{1-1 onto}{⟶}{A}$
17 f1of ${⊢}{x}:{A}\underset{1-1 onto}{⟶}{A}\to {x}:{A}⟶{A}$
18 fcoi2 ${⊢}{x}:{A}⟶{A}\to \left({\mathrm{I}↾}_{{A}}\right)\circ {x}={x}$
19 16 17 18 3syl ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to \left({\mathrm{I}↾}_{{A}}\right)\circ {x}={x}$
20 14 19 eqtrd ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to \left({\mathrm{I}↾}_{{A}}\right){+}_{{G}}{x}={x}$
21 f1ocnv ${⊢}{x}:{A}\underset{1-1 onto}{⟶}{A}\to {{x}}^{-1}:{A}\underset{1-1 onto}{⟶}{A}$
22 21 a1i ${⊢}{A}\in {V}\to \left({x}:{A}\underset{1-1 onto}{⟶}{A}\to {{x}}^{-1}:{A}\underset{1-1 onto}{⟶}{A}\right)$
23 1 4 elsymgbas ${⊢}{A}\in {V}\to \left({{x}}^{-1}\in {\mathrm{Base}}_{{G}}↔{{x}}^{-1}:{A}\underset{1-1 onto}{⟶}{A}\right)$
24 22 15 23 3imtr4d ${⊢}{A}\in {V}\to \left({x}\in {\mathrm{Base}}_{{G}}\to {{x}}^{-1}\in {\mathrm{Base}}_{{G}}\right)$
25 24 imp ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {{x}}^{-1}\in {\mathrm{Base}}_{{G}}$
26 1 4 5 symgov ${⊢}\left({{x}}^{-1}\in {\mathrm{Base}}_{{G}}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {{x}}^{-1}{+}_{{G}}{x}={{x}}^{-1}\circ {x}$
27 25 26 sylancom ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {{x}}^{-1}{+}_{{G}}{x}={{x}}^{-1}\circ {x}$
28 f1ococnv1 ${⊢}{x}:{A}\underset{1-1 onto}{⟶}{A}\to {{x}}^{-1}\circ {x}={\mathrm{I}↾}_{{A}}$
29 16 28 syl ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {{x}}^{-1}\circ {x}={\mathrm{I}↾}_{{A}}$
30 27 29 eqtrd ${⊢}\left({A}\in {V}\wedge {x}\in {\mathrm{Base}}_{{G}}\right)\to {{x}}^{-1}{+}_{{G}}{x}={\mathrm{I}↾}_{{A}}$
31 2 3 7 11 12 20 25 30 isgrpd ${⊢}{A}\in {V}\to {G}\in \mathrm{Grp}$