# 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 = ( SymGrp ` A )`
symgov.2
`|- B = ( Base ` G )`
symgov.3
`|- .+ = ( +g ` G )`
Assertion symgov
`|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )`

### Proof

Step Hyp Ref Expression
1 symgov.1
` |-  G = ( SymGrp ` A )`
2 symgov.2
` |-  B = ( Base ` G )`
3 symgov.3
` |-  .+ = ( +g ` G )`
4 eqid
` |-  ( A ^m A ) = ( A ^m A )`
5 1 4 3 symgplusg
` |-  .+ = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) )`
6 5 a1i
` |-  ( ( X e. B /\ Y e. B ) -> .+ = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) )`
7 simpl
` |-  ( ( f = X /\ g = Y ) -> f = X )`
8 simpr
` |-  ( ( f = X /\ g = Y ) -> g = Y )`
9 7 8 coeq12d
` |-  ( ( f = X /\ g = Y ) -> ( f o. g ) = ( X o. Y ) )`
` |-  ( ( ( X e. B /\ Y e. B ) /\ ( f = X /\ g = Y ) ) -> ( f o. g ) = ( X o. Y ) )`
` |-  ( X e. B -> X e. ( A ^m A ) )`
` |-  ( ( X e. B /\ Y e. B ) -> X e. ( A ^m A ) )`
` |-  ( Y e. B -> Y e. ( A ^m A ) )`
` |-  ( ( X e. B /\ Y e. B ) -> Y e. ( A ^m A ) )`
` |-  ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )`
` |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )`