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 ⟨“ 𝑆 𝑇 ”⟩ ) = ( 𝑆 + 𝑇 ) )