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=BaseG
Assertion gsumccatsymgsn ⊢A∈V∧W∈WordB∧Z∈B→∑GW++⟨“Z”⟩=∑GW∘Z

Proof

Step Hyp Ref Expression
1 gsumccatsymgsn.g ⊢G=SymGrp⁡A
2 gsumccatsymgsn.b ⊢B=BaseG
3 1 symggrp ⊢A∈V→G∈Grp
4 3 grpmndd ⊢A∈V→G∈Mnd
5 eqid ⊢+G=+G
6 2 5 gsumccatsn ⊢G∈Mnd∧W∈WordB∧Z∈B→∑GW++⟨“Z”⟩=∑GW+GZ
7 4 6 syl3an1 ⊢A∈V∧W∈WordB∧Z∈B→∑GW++⟨“Z”⟩=∑GW+GZ
8 4 3ad2ant1 ⊢A∈V∧W∈WordB∧Z∈B→G∈Mnd
9 simp2 ⊢A∈V∧W∈WordB∧Z∈B→W∈WordB
10 2 gsumwcl ⊢G∈Mnd∧W∈WordB→∑GW∈B
11 8 9 10 syl2anc ⊢A∈V∧W∈WordB∧Z∈B→∑GW∈B
12 simp3 ⊢A∈V∧W∈WordB∧Z∈B→Z∈B
13 1 2 5 symgov ⊢∑GW∈B∧Z∈B→∑GW+GZ=∑GW∘Z
14 11 12 13 syl2anc ⊢A∈V∧W∈WordB∧Z∈B→∑GW+GZ=∑GW∘Z
15 7 14 eqtrd ⊢A∈V∧W∈WordB∧Z∈B→∑GW++⟨“Z”⟩=∑GW∘Z