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	3	grpmndd	|- ( A e. V -> G e. Mnd )
5		eqid	|- ( +g ` G ) = ( +g ` G )
6	2 5	gsumccatsn	|- ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) ( +g ` G ) Z ) )
7	4 6	syl3an1	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) ( +g ` G ) Z ) )
8	4	3ad2ant1	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> G e. Mnd )
9		simp2	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> W e. Word B )
10	2	gsumwcl	|- ( ( G e. Mnd /\ W e. Word B ) -> ( G gsum W ) e. B )
11	8 9 10	syl2anc	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum W ) e. B )
12		simp3	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> Z e. B )
13	1 2 5	symgov	|- ( ( ( G gsum W ) e. B /\ Z e. B ) -> ( ( G gsum W ) ( +g ` G ) Z ) = ( ( G gsum W ) o. Z ) )
14	11 12 13	syl2anc	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( ( G gsum W ) ( +g ` G ) Z ) = ( ( G gsum W ) o. Z ) )
15	7 14	eqtrd	|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) o. Z ) )