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

Proof

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