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 ∈ 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 3 grpmndd ⊢ A ∈ V → G ∈ Mnd
5 eqid ⊢ + G = + G
6 2 5 gsumccatsn ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W + G Z
7 4 6 syl3an1 ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W + G Z
8 4 3ad2ant1 ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → G ∈ Mnd
9 simp2 ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → W ∈ Word B
10 2 gsumwcl ⊢ G ∈ Mnd ∧ W ∈ Word B → ∑ G W ∈ B
11 8 9 10 syl2anc ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ∈ B
12 simp3 ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → Z ∈ B
13 1 2 5 symgov ⊢ ∑ G W ∈ B ∧ Z ∈ B → ∑ G W + G Z = ∑ G W ∘ Z
14 11 12 13 syl2anc ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W + G Z = ∑ G W ∘ Z
15 7 14 eqtrd ⊢ A ∈ V ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W ∘ Z