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=BaseG
gsumws4.1 ⊢+˙=+G
Assertion gsumws4 ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“STUV”⟩=S+˙T+˙U+˙V

Proof

Step Hyp Ref Expression
1 gsumws4.0 ⊢B=BaseG
2 gsumws4.1 ⊢+˙=+G
3 s1s3 ⊢⟨“STUV”⟩=⟨“S”⟩++⟨“TUV”⟩
4 3 a1i ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→⟨“STUV”⟩=⟨“S”⟩++⟨“TUV”⟩
5 4 oveq2d ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“STUV”⟩=∑G⟨“S”⟩++⟨“TUV”⟩
6 simpl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→G∈Mnd
7 simprl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→S∈B
8 7 s1cld ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→⟨“S”⟩∈WordB
9 simprrl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→T∈B
10 simprrl ⊢S∈B∧T∈B∧U∈B∧V∈B→U∈B
11 10 adantl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→U∈B
12 simprrr ⊢S∈B∧T∈B∧U∈B∧V∈B→V∈B
13 12 adantl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→V∈B
14 9 11 13 s3cld ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→⟨“TUV”⟩∈WordB
15 1 2 gsumccat ⊢G∈Mnd∧⟨“S”⟩∈WordB∧⟨“TUV”⟩∈WordB→∑G⟨“S”⟩++⟨“TUV”⟩=∑G⟨“S”⟩+˙∑G⟨“TUV”⟩
16 6 8 14 15 syl3anc ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“S”⟩++⟨“TUV”⟩=∑G⟨“S”⟩+˙∑G⟨“TUV”⟩
17 1 gsumws1 ⊢S∈B→∑G⟨“S”⟩=S
18 17 ad2antrl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“S”⟩=S
19 1 2 gsumws3 ⊢G∈Mnd∧T∈B∧U∈B∧V∈B→∑G⟨“TUV”⟩=T+˙U+˙V
20 19 adantrl ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“TUV”⟩=T+˙U+˙V
21 18 20 oveq12d ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“S”⟩+˙∑G⟨“TUV”⟩=S+˙T+˙U+˙V
22 5 16 21 3eqtrd ⊢G∈Mnd∧S∈B∧T∈B∧U∈B∧V∈B→∑G⟨“STUV”⟩=S+˙T+˙U+˙V