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 ) )