# Metamath Proof Explorer

## Theorem symgov

Description: The value of the group operation of the symmetric group on A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015) (Revised by AV, 30-Mar-2024)

Ref Expression
Hypotheses symgov.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
symgov.2 ${⊢}{B}={\mathrm{Base}}_{{G}}$
symgov.3
Assertion symgov

### Proof

Step Hyp Ref Expression
1 symgov.1 ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 symgov.2 ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 symgov.3
4 eqid ${⊢}{{A}}^{{A}}={{A}}^{{A}}$
5 1 4 3 symgplusg
6 5 a1i
7 simpl ${⊢}\left({f}={X}\wedge {g}={Y}\right)\to {f}={X}$
8 simpr ${⊢}\left({f}={X}\wedge {g}={Y}\right)\to {g}={Y}$
9 7 8 coeq12d ${⊢}\left({f}={X}\wedge {g}={Y}\right)\to {f}\circ {g}={X}\circ {Y}$
10 9 adantl ${⊢}\left(\left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({f}={X}\wedge {g}={Y}\right)\right)\to {f}\circ {g}={X}\circ {Y}$
11 1 2 symgbasmap ${⊢}{X}\in {B}\to {X}\in \left({{A}}^{{A}}\right)$
12 11 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in \left({{A}}^{{A}}\right)$
13 1 2 symgbasmap ${⊢}{Y}\in {B}\to {Y}\in \left({{A}}^{{A}}\right)$
14 13 adantl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in \left({{A}}^{{A}}\right)$
15 coexg ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}\circ {Y}\in \mathrm{V}$
16 6 10 12 14 15 ovmpod