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 ) )