# Metamath Proof Explorer

## Theorem gsumws4

Description: Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020)

Ref Expression
Hypotheses gsumws4.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumws4.1
Assertion gsumws4

### Proof

Step Hyp Ref Expression
1 gsumws4.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumws4.1
3 s1s3 ${⊢}⟨“{S}{T}{U}{V}”⟩=⟨“{S}”⟩\mathrm{++}⟨“{T}{U}{V}”⟩$
4 3 a1i ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to ⟨“{S}{T}{U}{V}”⟩=⟨“{S}”⟩\mathrm{++}⟨“{T}{U}{V}”⟩$
5 4 oveq2d ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {\sum }_{{G}}⟨“{S}{T}{U}{V}”⟩={\sum }_{{G}}\left(⟨“{S}”⟩\mathrm{++}⟨“{T}{U}{V}”⟩\right)$
6 simpl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {G}\in \mathrm{Mnd}$
7 simprl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {S}\in {B}$
8 7 s1cld ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to ⟨“{S}”⟩\in \mathrm{Word}{B}$
9 simprrl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {T}\in {B}$
10 simprrl ${⊢}\left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\to {U}\in {B}$
11 10 adantl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {U}\in {B}$
12 simprrr ${⊢}\left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\to {V}\in {B}$
13 12 adantl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {V}\in {B}$
14 9 11 13 s3cld ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to ⟨“{T}{U}{V}”⟩\in \mathrm{Word}{B}$
15 1 2 gsumccat
16 6 8 14 15 syl3anc
17 1 gsumws1 ${⊢}{S}\in {B}\to {\sum }_{{G}}⟨“{S}”⟩={S}$
18 17 ad2antrl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge \left({U}\in {B}\wedge {V}\in {B}\right)\right)\right)\right)\to {\sum }_{{G}}⟨“{S}”⟩={S}$
19 1 2 gsumws3