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 ` G )
Assertion gsumccatsn
|- ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) .+ Z ) )

Proof

Step Hyp Ref Expression
1 gsumccat.b
 |-  B = ( Base ` G )
2 gsumccat.p
 |-  .+ = ( +g ` G )
3 s1cl
 |-  ( Z e. B -> <" Z "> e. Word B )
4 1 2 gsumccat
 |-  ( ( G e. Mnd /\ W e. Word B /\ <" Z "> e. Word B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) .+ ( G gsum <" Z "> ) ) )
5 3 4 syl3an3
 |-  ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) .+ ( G gsum <" Z "> ) ) )
6 1 gsumws1
 |-  ( Z e. B -> ( G gsum <" Z "> ) = Z )
7 6 3ad2ant3
 |-  ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum <" Z "> ) = Z )
8 7 oveq2d
 |-  ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( ( G gsum W ) .+ ( G gsum <" Z "> ) ) = ( ( G gsum W ) .+ Z ) )
9 5 8 eqtrd
 |-  ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) .+ Z ) )