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 ∈ V ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W ∘ Z

Proof

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