Metamath Proof Explorer

Theorem 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 ⊢ + ˙ = + G
Assertion gsumccatsn ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W + ˙ Z

Proof

Step Hyp Ref Expression
1 gsumccat.b ⊢ B = Base G
2 gsumccat.p ⊢ + ˙ = + G
3 s1cl ⊢ Z ∈ B → ⟨“ Z ”⟩ ∈ Word B
4 1 2 gsumccat ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ ⟨“ Z ”⟩ ∈ Word B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W + ˙ ∑ G ⟨“ Z ”⟩
5 3 4 syl3an3 ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W + ˙ ∑ G ⟨“ Z ”⟩
6 1 gsumws1 ⊢ Z ∈ B → ∑ G ⟨“ Z ”⟩ = Z
7 6 3ad2ant3 ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ Z ∈ B → ∑ G ⟨“ Z ”⟩ = Z
8 7 oveq2d ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W + ˙ ∑ G ⟨“ Z ”⟩ = ∑ G W + ˙ Z
9 5 8 eqtrd ⊢ G ∈ Mnd ∧ W ∈ Word B ∧ Z ∈ B → ∑ G W ++ ⟨“ Z ”⟩ = ∑ G W + ˙ Z