gsumccatsn

Description: Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019)

	Ref	Expression
Hypotheses	gsumccat.b	$⊢ B = {Base}_{G}$
	gsumccat.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	gsumccatsn	$⊢ (G \in Mnd \land W \in Word B \land Z \in B) \to \sum_{G} (W ++ ⟨“ Z ”⟩) = (\sum_{G}, W) \underset{˙}{+} Z$

Step	Hyp	Ref	Expression
1		gsumccat.b	$⊢ B = {Base}_{G}$
2		gsumccat.p	$⊢ \underset{˙}{+} = +_{G}$
3		s1cl	$⊢ Z \in B \to ⟨“ Z ”⟩ \in Word B$
4	1 2	gsumccat	$⊢ (G \in Mnd \land W \in Word B \land ⟨“ Z ”⟩ \in Word B) \to \sum_{G} (W ++ ⟨“ Z ”⟩) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, ⟨“ Z ”⟩)$
5	3 4	syl3an3	$⊢ (G \in Mnd \land W \in Word B \land Z \in B) \to \sum_{G} (W ++ ⟨“ Z ”⟩) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, ⟨“ Z ”⟩)$
6	1	gsumws1	$⊢ Z \in B \to \sum_{G} ⟨“ Z ”⟩ = Z$
7	6	3ad2ant3	$⊢ (G \in Mnd \land W \in Word B \land Z \in B) \to \sum_{G} ⟨“ Z ”⟩ = Z$
8	7	oveq2d	$⊢ (G \in Mnd \land W \in Word B \land Z \in B) \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, ⟨“ Z ”⟩) = (\sum_{G}, W) \underset{˙}{+} Z$
9	5 8	eqtrd	$⊢ (G \in Mnd \land W \in Word B \land Z \in B) \to \sum_{G} (W ++ ⟨“ Z ”⟩) = (\sum_{G}, W) \underset{˙}{+} Z$

Metamath Proof Explorer