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