# Metamath Proof Explorer

## Theorem gsumws3

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

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

### Proof

Step Hyp Ref Expression
1 gsumws3.0 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumws3.1
3 s1s2 ${⊢}⟨“{S}{T}{U}”⟩=⟨“{S}”⟩\mathrm{++}⟨“{T}{U}”⟩$
4 3 a1i ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge {U}\in {B}\right)\right)\right)\to ⟨“{S}{T}{U}”⟩=⟨“{S}”⟩\mathrm{++}⟨“{T}{U}”⟩$
5 4 oveq2d ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge {U}\in {B}\right)\right)\right)\to {\sum }_{{G}}⟨“{S}{T}{U}”⟩={\sum }_{{G}}\left(⟨“{S}”⟩\mathrm{++}⟨“{T}{U}”⟩\right)$
6 simpl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge {U}\in {B}\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 {U}\in {B}\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 {U}\in {B}\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 {U}\in {B}\right)\right)\right)\to {T}\in {B}$
10 simprrr ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge {U}\in {B}\right)\right)\right)\to {U}\in {B}$
11 9 10 s2cld ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge {U}\in {B}\right)\right)\right)\to ⟨“{T}{U}”⟩\in \mathrm{Word}{B}$
12 1 2 gsumccat
13 6 8 11 12 syl3anc
14 1 gsumws1 ${⊢}{S}\in {B}\to {\sum }_{{G}}⟨“{S}”⟩={S}$
15 14 ad2antrl ${⊢}\left({G}\in \mathrm{Mnd}\wedge \left({S}\in {B}\wedge \left({T}\in {B}\wedge {U}\in {B}\right)\right)\right)\to {\sum }_{{G}}⟨“{S}”⟩={S}$
16 1 2 gsumws2
17 16 3expb