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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumws4.1 ⊢ + = ( +g ‘ 𝐺 )
Assertion gsumws4 ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 𝑈 𝑉 ”⟩ ) = ( 𝑆 + ( 𝑇 + ( 𝑈 + 𝑉 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumws4.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumws4.1 ⊢ + = ( +g ‘ 𝐺 )
3 s1s3 ⊢ ⟨“ 𝑆 𝑇 𝑈 𝑉 ”⟩ = ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 𝑉 ”⟩ )
4 3 a1i ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ⟨“ 𝑆 𝑇 𝑈 𝑉 ”⟩ = ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) )
5 4 oveq2d ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 𝑈 𝑉 ”⟩ ) = ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) ) )
6 simpl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → 𝐺 ∈ Mnd )
7 simprl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → 𝑆 ∈ 𝐵 )
8 7 s1cld ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ⟨“ 𝑆 ”⟩ ∈ Word 𝐵 )
9 simprrl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → 𝑇 ∈ 𝐵 )
10 simprrl ⊢ ( ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) → 𝑈 ∈ 𝐵 )
11 10 adantl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → 𝑈 ∈ 𝐵 )
12 simprrr ⊢ ( ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) → 𝑉 ∈ 𝐵 )
13 12 adantl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → 𝑉 ∈ 𝐵 )
14 9 11 13 s3cld ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ⟨“ 𝑇 𝑈 𝑉 ”⟩ ∈ Word 𝐵 )
15 1 2 gsumccat ⊢ ( ( 𝐺 ∈ Mnd ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝐵 ∧ ⟨“ 𝑇 𝑈 𝑉 ”⟩ ∈ Word 𝐵 ) → ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) ) = ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) ) )
16 6 8 14 15 syl3anc ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) ) = ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) ) )
17 1 gsumws1 ⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )
18 17 ad2antrl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )
19 1 2 gsumws3 ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) → ( 𝐺 Σg ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) = ( 𝑇 + ( 𝑈 + 𝑉 ) ) )
20 19 adantrl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) = ( 𝑇 + ( 𝑈 + 𝑉 ) ) )
21 18 20 oveq12d ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 𝑈 𝑉 ”⟩ ) ) = ( 𝑆 + ( 𝑇 + ( 𝑈 + 𝑉 ) ) ) )
22 5 16 21 3eqtrd ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) ) ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 𝑈 𝑉 ”⟩ ) = ( 𝑆 + ( 𝑇 + ( 𝑈 + 𝑉 ) ) ) )