Step |
Hyp |
Ref |
Expression |
1 |
|
gsumccatsymgsn.g |
|- G = ( SymGrp ` A ) |
2 |
|
gsumccatsymgsn.b |
|- B = ( Base ` G ) |
3 |
1
|
symggrp |
|- ( A e. V -> G e. Grp ) |
4 |
|
grpmnd |
|- ( G e. Grp -> G e. Mnd ) |
5 |
3 4
|
syl |
|- ( A e. V -> G e. Mnd ) |
6 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
7 |
2 6
|
gsumccatsn |
|- ( ( G e. Mnd /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) ( +g ` G ) Z ) ) |
8 |
5 7
|
syl3an1 |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) ( +g ` G ) Z ) ) |
9 |
5
|
3ad2ant1 |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> G e. Mnd ) |
10 |
|
simp2 |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> W e. Word B ) |
11 |
2
|
gsumwcl |
|- ( ( G e. Mnd /\ W e. Word B ) -> ( G gsum W ) e. B ) |
12 |
9 10 11
|
syl2anc |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum W ) e. B ) |
13 |
|
simp3 |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> Z e. B ) |
14 |
1 2 6
|
symgov |
|- ( ( ( G gsum W ) e. B /\ Z e. B ) -> ( ( G gsum W ) ( +g ` G ) Z ) = ( ( G gsum W ) o. Z ) ) |
15 |
12 13 14
|
syl2anc |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( ( G gsum W ) ( +g ` G ) Z ) = ( ( G gsum W ) o. Z ) ) |
16 |
8 15
|
eqtrd |
|- ( ( A e. V /\ W e. Word B /\ Z e. B ) -> ( G gsum ( W ++ <" Z "> ) ) = ( ( G gsum W ) o. Z ) ) |