# Metamath Proof Explorer

## Theorem gsumccatsymgsn

Description: Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsumccatsymgsn.g
`|- G = ( SymGrp ` A )`
gsumccatsymgsn.b
`|- B = ( Base ` G )`
Assertion gsumccatsymgsn
`|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) o. Z ) )`

### Proof

Step Hyp Ref Expression
1 gsumccatsymgsn.g
` |-  G = ( SymGrp ` A )`
2 gsumccatsymgsn.b
` |-  B = ( Base ` G )`
3 1 symggrp
` |-  ( A e. V -> G e. Grp )`
4 grpmnd
` |-  ( G e. Grp -> G e. Mnd )`
5 3 4 syl
` |-  ( A e. V -> G e. Mnd )`
6 eqid
` |-  ( +g ` G ) = ( +g ` G )`
7 2 6 gsumccatsn
` |-  ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) ( +g ` G ) Z ) )`
8 5 7 syl3an1
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) ( +g ` G ) Z ) )`
9 5 3ad2ant1
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> G e. Mnd )`
10 simp2
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> W e. Word B )`
11 2 gsumwcl
` |-  ( ( G e. Mnd /\ W e. Word B ) -> ( G gsum W ) e. B )`
12 9 10 11 syl2anc
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum W ) e. B )`
13 simp3
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> Z e. B )`
14 1 2 6 symgov
` |-  ( ( ( G gsum W ) e. B /\ Z e. B ) -> ( ( G gsum W ) ( +g ` G ) Z ) = ( ( G gsum W ) o. Z ) )`
15 12 13 14 syl2anc
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( ( G gsum W ) ( +g ` G ) Z ) = ( ( G gsum W ) o. Z ) )`
16 8 15 eqtrd
` |-  ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) o. Z ) )`