This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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