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	$⊢ B = {Base}_{G}$
	gsumccat.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	gsumws2	$⊢ (G \in Mnd \land S \in B \land T \in B) \to \sum_{G} ⟨“ S T ”⟩ = S \underset{˙}{+} T$

Step	Hyp	Ref	Expression
1		gsumccat.b	$⊢ B = {Base}_{G}$
2		gsumccat.p	$⊢ \underset{˙}{+} = +_{G}$
3		df-s2	$⊢ ⟨“ S T ”⟩ = ⟨“ S ”⟩ ++ ⟨“ T ”⟩$
4	3	a1i	$⊢ (G \in Mnd \land S \in B \land T \in B) \to ⟨“ S T ”⟩ = ⟨“ S ”⟩ ++ ⟨“ T ”⟩$
5	4	oveq2d	$⊢ (G \in Mnd \land S \in B \land T \in B) \to \sum_{G} ⟨“ S T ”⟩ = \sum_{G} (⟨“ S ”⟩ ++ ⟨“ T ”⟩)$
6		id	$⊢ G \in Mnd \to G \in Mnd$
7		s1cl	$⊢ S \in B \to ⟨“ S ”⟩ \in Word B$
8		s1cl	$⊢ T \in B \to ⟨“ T ”⟩ \in Word B$
9	1 2	gsumccat	$⊢ (G \in Mnd \land ⟨“ S ”⟩ \in Word B \land ⟨“ T ”⟩ \in Word B) \to \sum_{G} (⟨“ S ”⟩ ++ ⟨“ T ”⟩) = (\sum_{G}, ⟨“ S ”⟩) \underset{˙}{+} (\sum_{G}, ⟨“ T ”⟩)$
10	6 7 8 9	syl3an	$⊢ (G \in Mnd \land S \in B \land T \in B) \to \sum_{G} (⟨“ S ”⟩ ++ ⟨“ T ”⟩) = (\sum_{G}, ⟨“ S ”⟩) \underset{˙}{+} (\sum_{G}, ⟨“ T ”⟩)$
11	1	gsumws1	$⊢ S \in B \to \sum_{G} ⟨“ S ”⟩ = S$
12	1	gsumws1	$⊢ T \in B \to \sum_{G} ⟨“ T ”⟩ = T$
13	11 12	oveqan12d	$⊢ (S \in B \land T \in B) \to (\sum_{G}, ⟨“ S ”⟩) \underset{˙}{+} (\sum_{G}, ⟨“ T ”⟩) = S \underset{˙}{+} T$
14	13	3adant1	$⊢ (G \in Mnd \land S \in B \land T \in B) \to (\sum_{G}, ⟨“ S ”⟩) \underset{˙}{+} (\sum_{G}, ⟨“ T ”⟩) = S \underset{˙}{+} T$
15	5 10 14	3eqtrd	$⊢ (G \in Mnd \land S \in B \land T \in B) \to \sum_{G} ⟨“ S T ”⟩ = S \underset{˙}{+} T$

Metamath Proof Explorer