Theorem gsumccatsn

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

	Ref	Expression
Hypotheses	gsumccat.b	$$⊢B={\mathrm{Base}}_G$$
	gsumccat.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	gsumccatsn	$$⊢\left(G\in \mathrm{Mnd}\wedge W\in \mathrm{Word}B\wedge Z\in B\right)\to {\sum }_G\left(W\mathrm{++}⟨“Z”⟩\right)=\left({\sum }_G,W\right)\underset{\dot{}}{+}Z$$

Proof

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