Metamath Proof Explorer

Theorem gsumccatOLD

Description: Obsolete version of gsumccat as of 13-Jan-2024. Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses gsumwcl.b 
|- B = ( Base ` G )
gsumsgrpccat.p 
|- .+ = ( +g ` G )
Assertion gsumccatOLD 
|- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( 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 oveq1 
 |-  ( W = (/) -> ( W ++ X ) = ( (/) ++ X ) )
4 3 oveq2d 
 |-  ( W = (/) -> ( G gsum ( W ++ X ) ) = ( G gsum ( (/) ++ X ) ) )
5 oveq2 
 |-  ( W = (/) -> ( G gsum W ) = ( G gsum (/) ) )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 6 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
8 5 7 eqtrdi 
 |-  ( W = (/) -> ( G gsum W ) = ( 0g ` G ) )
9 8 oveq1d 
 |-  ( W = (/) -> ( ( G gsum W ) .+ ( G gsum X ) ) = ( ( 0g ` G ) .+ ( G gsum X ) ) )
10 4 9 eqeq12d 
 |-  ( W = (/) -> ( ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) <-> ( G gsum ( (/) ++ X ) ) = ( ( 0g ` G ) .+ ( G gsum X ) ) ) )
11 oveq2 
 |-  ( X = (/) -> ( W ++ X ) = ( W ++ (/) ) )
12 11 oveq2d 
 |-  ( X = (/) -> ( G gsum ( W ++ X ) ) = ( G gsum ( W ++ (/) ) ) )
13 oveq2 
 |-  ( X = (/) -> ( G gsum X ) = ( G gsum (/) ) )
14 13 7 eqtrdi 
 |-  ( X = (/) -> ( G gsum X ) = ( 0g ` G ) )
15 14 oveq2d 
 |-  ( X = (/) -> ( ( G gsum W ) .+ ( G gsum X ) ) = ( ( G gsum W ) .+ ( 0g ` G ) ) )
16 12 15 eqeq12d 
 |-  ( X = (/) -> ( ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) <-> ( G gsum ( W ++ (/) ) ) = ( ( G gsum W ) .+ ( 0g ` G ) ) ) )
17 simpl1 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> G e. Mnd )
18 lennncl 
 |-  ( ( W e. Word B /\ W =/= (/) ) -> ( # ` W ) e. NN )
19 18 3ad2antl2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( # ` W ) e. NN )
20 19 adantrr 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. NN )
21 lennncl 
 |-  ( ( X e. Word B /\ X =/= (/) ) -> ( # ` X ) e. NN )
22 21 3ad2antl3 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ X =/= (/) ) -> ( # ` X ) e. NN )
23 22 adantrl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. NN )
24 20 23 nnaddcld 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. NN )
25 nnm1nn0 
 |-  ( ( ( # ` W ) + ( # ` X ) ) e. NN -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. NN0 )
26 24 25 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. NN0 )
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 26 27 eleqtrdi 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` 0 ) )
29 simpl2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W e. Word B )
30 simpl3 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X e. Word B )
31 ccatcl 
 |-  ( ( W e. Word B /\ X e. Word B ) -> ( W ++ X ) e. Word B )
32 29 30 31 syl2anc 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) e. Word B )
33 wrdf 
 |-  ( ( W ++ X ) e. Word B -> ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B )
34 32 33 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B )
35 ccatlen 
 |-  ( ( W e. Word B /\ X e. Word B ) -> ( # ` ( W ++ X ) ) = ( ( # ` W ) + ( # ` X ) ) )
36 29 30 35 syl2anc 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` ( W ++ X ) ) = ( ( # ` W ) + ( # ` X ) ) )
37 36 oveq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) )
38 20 nnzd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ZZ )
39 23 nnzd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. ZZ )
40 38 39 zaddcld 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. ZZ )
41 fzoval 
 |-  ( ( ( # ` W ) + ( # ` X ) ) e. ZZ -> ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
42 40 41 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
43 37 42 eqtrd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
44 43 feq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B <-> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B ) )
45 34 44 mpbid 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B )
46 1 2 17 28 45 gsumval2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
47 nnm1nn0 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
48 20 47 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
49 48 27 eleqtrdi 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
50 wrdf 
 |-  ( W e. Word B -> W : ( 0 ..^ ( # ` W ) ) --> B )
51 29 50 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> B )
52 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
53 38 52 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
54 53 feq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> B <-> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) )
55 51 54 mpbid 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B )
56 1 2 17 49 55 gsumval2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum W ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) )
57 nnm1nn0 
 |-  ( ( # ` X ) e. NN -> ( ( # ` X ) - 1 ) e. NN0 )
58 23 57 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. NN0 )
59 58 27 eleqtrdi 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. ( ZZ>= ` 0 ) )
60 wrdf 
 |-  ( X e. Word B -> X : ( 0 ..^ ( # ` X ) ) --> B )
61 30 60 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ..^ ( # ` X ) ) --> B )
62 fzoval 
 |-  ( ( # ` X ) e. ZZ -> ( 0 ..^ ( # ` X ) ) = ( 0 ... ( ( # ` X ) - 1 ) ) )
63 39 62 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` X ) ) = ( 0 ... ( ( # ` X ) - 1 ) ) )
64 63 feq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( X : ( 0 ..^ ( # ` X ) ) --> B <-> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B ) )
65 61 64 mpbid 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B )
66 1 2 17 59 65 gsumval2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum X ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) )
67 56 66 oveq12d 
 |-  ( ( ( G e. Mnd /\ 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 ) ) ) )
68 1 2 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
69 68 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
70 17 69 sylan 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
71 1 2 mndass 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
72 17 71 sylan 
 |-  ( ( ( ( G e. Mnd /\ 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 ) ) )
73 uzid 
 |-  ( ( # ` W ) e. ZZ -> ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) )
74 38 73 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) )
75 uzaddcl 
 |-  ( ( ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) /\ ( ( # ` X ) - 1 ) e. NN0 ) -> ( ( # ` W ) + ( ( # ` X ) - 1 ) ) e. ( ZZ>= ` ( # ` W ) ) )
76 74 58 75 syl2anc 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( ( # ` X ) - 1 ) ) e. ( ZZ>= ` ( # ` W ) ) )
77 20 nncnd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. CC )
78 23 nncnd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. CC )
79 1cnd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> 1 e. CC )
80 77 78 79 addsubassd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( # ` W ) + ( ( # ` X ) - 1 ) ) )
81 ax-1cn 
 |-  1 e. CC
82 npcan 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
83 77 81 82 sylancl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
84 83 fveq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ZZ>= ` ( # ` W ) ) )
85 76 80 84 3eltr4d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) )
86 45 ffvelrnda 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) e. B )
87 70 72 85 49 86 seqsplit 
 |-  ( ( ( G e. Mnd /\ 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 ) ) ) )
88 simpll2 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> W e. Word B )
89 simpll3 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> X e. Word B )
90 53 eleq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` W ) ) <-> x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) )
91 90 biimpar 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) )
92 ccatval1 
 |-  ( ( W e. Word B /\ X e. Word B /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ X ) ` x ) = ( W ` x ) )
93 88 89 91 92 syl3anc 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) = ( W ` x ) )
94 49 93 seqfveq 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) )
95 77 addid2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 + ( # ` W ) ) = ( # ` W ) )
96 83 95 eqtr4d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( 0 + ( # ` W ) ) )
97 96 seqeq1d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) = seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) )
98 77 78 addcomd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) = ( ( # ` X ) + ( # ` W ) ) )
99 98 oveq1d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) + ( # ` W ) ) - 1 ) )
100 78 77 79 addsubd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` X ) + ( # ` W ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) )
101 99 100 eqtrd 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) )
102 97 101 fveq12d 
 |-  ( ( ( G e. Mnd /\ 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 ) ) ) )
103 simpll2 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> W e. Word B )
104 simpll3 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> X e. Word B )
105 63 eleq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` X ) ) <-> x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) )
106 105 biimpar 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` X ) ) )
107 ccatval3 
 |-  ( ( W e. Word B /\ X e. Word B /\ x e. ( 0 ..^ ( # ` X ) ) ) -> ( ( W ++ X ) ` ( x + ( # ` W ) ) ) = ( X ` x ) )
108 103 104 106 107 syl3anc 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( ( W ++ X ) ` ( x + ( # ` W ) ) ) = ( X ` x ) )
109 108 eqcomd 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( X ` x ) = ( ( W ++ X ) ` ( x + ( # ` W ) ) ) )
110 59 38 109 seqshft2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) )
111 102 110 eqtr4d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) )
112 94 111 oveq12d 
 |-  ( ( ( G e. Mnd /\ 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 ) ) ) )
113 87 112 eqtrd 
 |-  ( ( ( G e. Mnd /\ 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 ) ) ) )
114 67 113 eqtr4d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( G gsum W ) .+ ( G gsum X ) ) = ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) )
115 46 114 eqtr4d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )
116 115 anassrs 
 |-  ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) /\ X =/= (/) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )
117 simpl2 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> W e. Word B )
118 ccatrid 
 |-  ( W e. Word B -> ( W ++ (/) ) = W )
119 117 118 syl 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( W ++ (/) ) = W )
120 119 oveq2d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( G gsum ( W ++ (/) ) ) = ( G gsum W ) )
121 simpl1 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> G e. Mnd )
122 1 gsumwcl 
 |-  ( ( G e. Mnd /\ W e. Word B ) -> ( G gsum W ) e. B )
123 122 3adant3 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( G gsum W ) e. B )
124 123 adantr 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( G gsum W ) e. B )
125 1 2 6 mndrid 
 |-  ( ( G e. Mnd /\ ( G gsum W ) e. B ) -> ( ( G gsum W ) .+ ( 0g ` G ) ) = ( G gsum W ) )
126 121 124 125 syl2anc 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( ( G gsum W ) .+ ( 0g ` G ) ) = ( G gsum W ) )
127 120 126 eqtr4d 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( G gsum ( W ++ (/) ) ) = ( ( G gsum W ) .+ ( 0g ` G ) ) )
128 16 116 127 pm2.61ne 
 |-  ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )
129 ccatlid 
 |-  ( X e. Word B -> ( (/) ++ X ) = X )
130 129 3ad2ant3 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( (/) ++ X ) = X )
131 130 oveq2d 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( G gsum ( (/) ++ X ) ) = ( G gsum X ) )
132 simp1 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> G e. Mnd )
133 1 gsumwcl 
 |-  ( ( G e. Mnd /\ X e. Word B ) -> ( G gsum X ) e. B )
134 1 2 6 mndlid 
 |-  ( ( G e. Mnd /\ ( G gsum X ) e. B ) -> ( ( 0g ` G ) .+ ( G gsum X ) ) = ( G gsum X ) )
135 132 133 134 3imp3i2an 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( ( 0g ` G ) .+ ( G gsum X ) ) = ( G gsum X ) )
136 131 135 eqtr4d 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( G gsum ( (/) ++ X ) ) = ( ( 0g ` G ) .+ ( G gsum X ) ) )
137 10 128 136 pm2.61ne 
 |-  ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )