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

Proof

Step Hyp Ref Expression
1 gsumws3.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumws3.1 ⊢ + = ( +g ‘ 𝐺 )
3 s1s2 ⊢ ⟨“ 𝑆 𝑇 𝑈 ”⟩ = ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 ”⟩ )
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 simprrr ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → 𝑈 ∈ 𝐵 )
11 9 10 s2cld ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → ⟨“ 𝑇 𝑈 ”⟩ ∈ Word 𝐵 )
12 1 2 gsumccat ⊢ ( ( 𝐺 ∈ Mnd ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝐵 ∧ ⟨“ 𝑇 𝑈 ”⟩ ∈ Word 𝐵 ) → ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 ”⟩ ) ) = ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 𝑈 ”⟩ ) ) )
13 6 8 11 12 syl3anc ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 𝑈 ”⟩ ) ) = ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 𝑈 ”⟩ ) ) )
14 1 gsumws1 ⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )
15 14 ad2antrl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )
16 1 2 gsumws2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) → ( 𝐺 Σg ⟨“ 𝑇 𝑈 ”⟩ ) = ( 𝑇 + 𝑈 ) )
17 16 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) → ( 𝐺 Σg ⟨“ 𝑇 𝑈 ”⟩ ) = ( 𝑇 + 𝑈 ) )
18 17 adantrl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → ( 𝐺 Σg ⟨“ 𝑇 𝑈 ”⟩ ) = ( 𝑇 + 𝑈 ) )
19 15 18 oveq12d ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 𝑈 ”⟩ ) ) = ( 𝑆 + ( 𝑇 + 𝑈 ) ) )
20 5 13 19 3eqtrd ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑆 ∈ 𝐵 ∧ ( 𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ) ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 𝑈 ”⟩ ) = ( 𝑆 + ( 𝑇 + 𝑈 ) ) )