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}=\mathrm{SymGrp}\left({A}\right)$
gsumccatsymgsn.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
Assertion gsumccatsymgsn ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {\sum }_{{G}}\left({W}\mathrm{++}⟨“{Z}”⟩\right)=\left({\sum }_{{G}},{W}\right)\circ {Z}$

Proof

Step Hyp Ref Expression
1 gsumccatsymgsn.g ${⊢}{G}=\mathrm{SymGrp}\left({A}\right)$
2 gsumccatsymgsn.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 1 symggrp ${⊢}{A}\in {V}\to {G}\in \mathrm{Grp}$
4 grpmnd ${⊢}{G}\in \mathrm{Grp}\to {G}\in \mathrm{Mnd}$
5 3 4 syl ${⊢}{A}\in {V}\to {G}\in \mathrm{Mnd}$
6 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
7 2 6 gsumccatsn ${⊢}\left({G}\in \mathrm{Mnd}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {\sum }_{{G}}\left({W}\mathrm{++}⟨“{Z}”⟩\right)=\left({\sum }_{{G}},{W}\right){+}_{{G}}{Z}$
8 5 7 syl3an1 ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {\sum }_{{G}}\left({W}\mathrm{++}⟨“{Z}”⟩\right)=\left({\sum }_{{G}},{W}\right){+}_{{G}}{Z}$
9 5 3ad2ant1 ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {G}\in \mathrm{Mnd}$
10 simp2 ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {W}\in \mathrm{Word}{B}$
11 2 gsumwcl ${⊢}\left({G}\in \mathrm{Mnd}\wedge {W}\in \mathrm{Word}{B}\right)\to {\sum }_{{G}}{W}\in {B}$
12 9 10 11 syl2anc ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {\sum }_{{G}}{W}\in {B}$
13 simp3 ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {Z}\in {B}$
14 1 2 6 symgov ${⊢}\left({\sum }_{{G}}{W}\in {B}\wedge {Z}\in {B}\right)\to \left({\sum }_{{G}},{W}\right){+}_{{G}}{Z}=\left({\sum }_{{G}},{W}\right)\circ {Z}$
15 12 13 14 syl2anc ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to \left({\sum }_{{G}},{W}\right){+}_{{G}}{Z}=\left({\sum }_{{G}},{W}\right)\circ {Z}$
16 8 15 eqtrd ${⊢}\left({A}\in {V}\wedge {W}\in \mathrm{Word}{B}\wedge {Z}\in {B}\right)\to {\sum }_{{G}}\left({W}\mathrm{++}⟨“{Z}”⟩\right)=\left({\sum }_{{G}},{W}\right)\circ {Z}$