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 = Base G
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 = Base G
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 ”⟩ ∈ Word B
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 ”⟩ ∈ Word B
12 1 2 gsumccat ⊢ G ∈ Mnd ∧ ⟨“ S ”⟩ ∈ Word B ∧ ⟨“ TU ”⟩ ∈ Word B → ∑ 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