This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumsgrpccat

Description: Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat . (Contributed by AV, 26-Dec-2023)

Ref Expression
Hypotheses gsumwcl.b 
|- B = ( Base ` G )
gsumsgrpccat.p 
|- .+ = ( +g ` G )
Assertion gsumsgrpccat 
|- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )

Proof

Step Hyp Ref Expression
1 gsumwcl.b 
 |-  B = ( Base ` G )
2 gsumsgrpccat.p 
 |-  .+ = ( +g ` G )
3 simp1 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> G e. Smgrp )
4 sgrpmgm 
 |-  ( G e. Smgrp -> G e. Mgm )
5 1 2 mgmcl 
 |-  ( ( G e. Mgm /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
6 4 5 syl3an1 
 |-  ( ( G e. Smgrp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
7 6 3expb 
 |-  ( ( G e. Smgrp /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
8 3 7 sylan 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
9 1 2 sgrpass 
 |-  ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
10 3 9 sylan 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
11 lennncl 
 |-  ( ( W e. Word B /\ W =/= (/) ) -> ( # ` W ) e. NN )
12 11 ad2ant2r 
 |-  ( ( ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. NN )
13 12 3adant1 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. NN )
14 13 nnzd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ZZ )
15 14 uzidd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) )
16 lennncl 
 |-  ( ( X e. Word B /\ X =/= (/) ) -> ( # ` X ) e. NN )
17 16 ad2ant2l 
 |-  ( ( ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. NN )
18 17 3adant1 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. NN )
19 nnm1nn0 
 |-  ( ( # ` X ) e. NN -> ( ( # ` X ) - 1 ) e. NN0 )
20 18 19 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. NN0 )
21 uzaddcl 
 |-  ( ( ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) /\ ( ( # ` X ) - 1 ) e. NN0 ) -> ( ( # ` W ) + ( ( # ` X ) - 1 ) ) e. ( ZZ>= ` ( # ` W ) ) )
22 15 20 21 syl2anc 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( ( # ` X ) - 1 ) ) e. ( ZZ>= ` ( # ` W ) ) )
23 13 nncnd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. CC )
24 18 nncnd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. CC )
25 1cnd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> 1 e. CC )
26 23 24 25 addsubassd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( # ` W ) + ( ( # ` X ) - 1 ) ) )
27 ax-1cn 
 |-  1 e. CC
28 npcan 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
29 23 27 28 sylancl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
30 29 fveq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ZZ>= ` ( # ` W ) ) )
31 22 26 30 3eltr4d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) )
32 nnm1nn0 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
33 13 32 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
34 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
35 33 34 eleqtrdi 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
36 ccatcl 
 |-  ( ( W e. Word B /\ X e. Word B ) -> ( W ++ X ) e. Word B )
37 36 3ad2ant2 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) e. Word B )
38 wrdf 
 |-  ( ( W ++ X ) e. Word B -> ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B )
39 37 38 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B )
40 ccatlen 
 |-  ( ( W e. Word B /\ X e. Word B ) -> ( # ` ( W ++ X ) ) = ( ( # ` W ) + ( # ` X ) ) )
41 40 3ad2ant2 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` ( W ++ X ) ) = ( ( # ` W ) + ( # ` X ) ) )
42 41 oveq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) )
43 18 nnzd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. ZZ )
44 14 43 zaddcld 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. ZZ )
45 fzoval 
 |-  ( ( ( # ` W ) + ( # ` X ) ) e. ZZ -> ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
46 44 45 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
47 42 46 eqtrd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
48 47 feq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B <-> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B ) )
49 39 48 mpbid 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B )
50 49 ffvelcdmda 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) e. B )
51 8 10 31 35 50 seqsplit 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) .+ ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) )
52 simpl2l 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> W e. Word B )
53 simpl2r 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> X e. Word B )
54 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
55 14 54 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
56 55 eleq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` W ) ) <-> x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) )
57 56 biimpar 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) )
58 ccatval1 
 |-  ( ( W e. Word B /\ X e. Word B /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ X ) ` x ) = ( W ` x ) )
59 52 53 57 58 syl3anc 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) = ( W ` x ) )
60 35 59 seqfveq 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) )
61 23 addlidd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 + ( # ` W ) ) = ( # ` W ) )
62 29 61 eqtr4d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( 0 + ( # ` W ) ) )
63 62 seqeq1d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) = seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) )
64 23 24 addcomd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) = ( ( # ` X ) + ( # ` W ) ) )
65 64 oveq1d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) + ( # ` W ) ) - 1 ) )
66 24 23 25 addsubd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` X ) + ( # ` W ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) )
67 65 66 eqtrd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) )
68 63 67 fveq12d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) )
69 20 34 eleqtrdi 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. ( ZZ>= ` 0 ) )
70 simpl2l 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> W e. Word B )
71 simpl2r 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> X e. Word B )
72 fzoval 
 |-  ( ( # ` X ) e. ZZ -> ( 0 ..^ ( # ` X ) ) = ( 0 ... ( ( # ` X ) - 1 ) ) )
73 43 72 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` X ) ) = ( 0 ... ( ( # ` X ) - 1 ) ) )
74 73 eleq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` X ) ) <-> x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) )
75 74 biimpar 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` X ) ) )
76 ccatval3 
 |-  ( ( W e. Word B /\ X e. Word B /\ x e. ( 0 ..^ ( # ` X ) ) ) -> ( ( W ++ X ) ` ( x + ( # ` W ) ) ) = ( X ` x ) )
77 70 71 75 76 syl3anc 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( ( W ++ X ) ` ( x + ( # ` W ) ) ) = ( X ` x ) )
78 77 eqcomd 
 |-  ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( X ` x ) = ( ( W ++ X ) ` ( x + ( # ` W ) ) ) )
79 69 14 78 seqshft2 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) )
80 68 79 eqtr4d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) )
81 60 80 oveq12d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) .+ ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) )
82 51 81 eqtrd 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) )
83 13 18 nnaddcld 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. NN )
84 nnm1nn0 
 |-  ( ( ( # ` W ) + ( # ` X ) ) e. NN -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. NN0 )
85 83 84 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. NN0 )
86 85 34 eleqtrdi 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` 0 ) )
87 1 2 3 86 49 gsumval2 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
88 simp2l 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W e. Word B )
89 wrdf 
 |-  ( W e. Word B -> W : ( 0 ..^ ( # ` W ) ) --> B )
90 88 89 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> B )
91 55 feq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> B <-> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) )
92 90 91 mpbid 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B )
93 1 2 3 35 92 gsumval2 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum W ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) )
94 simp2r 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X e. Word B )
95 wrdf 
 |-  ( X e. Word B -> X : ( 0 ..^ ( # ` X ) ) --> B )
96 94 95 syl 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ..^ ( # ` X ) ) --> B )
97 73 feq2d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( X : ( 0 ..^ ( # ` X ) ) --> B <-> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B ) )
98 96 97 mpbid 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B )
99 1 2 3 69 98 gsumval2 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum X ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) )
100 93 99 oveq12d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( G gsum W ) .+ ( G gsum X ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) )
101 82 87 100 3eqtr4d 
 |-  ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )