This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumws2

Description: Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses gsumccat.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumccat.p ⊢ + = ( +g ‘ 𝐺 )
Assertion gsumws2 ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 ”⟩ ) = ( 𝑆 + 𝑇 ) )

Proof

Step Hyp Ref Expression
1 gsumccat.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumccat.p ⊢ + = ( +g ‘ 𝐺 )
3 df-s2 ⊢ ⟨“ 𝑆 𝑇 ”⟩ = ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ )
4 3 a1i ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ⟨“ 𝑆 𝑇 ”⟩ = ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ ) )
5 4 oveq2d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 ”⟩ ) = ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ ) ) )
6 id ⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Mnd )
7 s1cl ⊢ ( 𝑆 ∈ 𝐵 → ⟨“ 𝑆 ”⟩ ∈ Word 𝐵 )
8 s1cl ⊢ ( 𝑇 ∈ 𝐵 → ⟨“ 𝑇 ”⟩ ∈ Word 𝐵 )
9 1 2 gsumccat ⊢ ( ( 𝐺 ∈ Mnd ∧ ⟨“ 𝑆 ”⟩ ∈ Word 𝐵 ∧ ⟨“ 𝑇 ”⟩ ∈ Word 𝐵 ) → ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ ) ) = ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 ”⟩ ) ) )
10 6 7 8 9 syl3an ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( 𝐺 Σg ( ⟨“ 𝑆 ”⟩ ++ ⟨“ 𝑇 ”⟩ ) ) = ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 ”⟩ ) ) )
11 1 gsumws1 ⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )
12 1 gsumws1 ⊢ ( 𝑇 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑇 ”⟩ ) = 𝑇 )
13 11 12 oveqan12d ⊢ ( ( 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 ”⟩ ) ) = ( 𝑆 + 𝑇 ) )
14 13 3adant1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) + ( 𝐺 Σg ⟨“ 𝑇 ”⟩ ) ) = ( 𝑆 + 𝑇 ) )
15 5 10 14 3eqtrd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( 𝐺 Σg ⟨“ 𝑆 𝑇 ”⟩ ) = ( 𝑆 + 𝑇 ) )