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 𝐵 = ( Base ‘ 𝐺 )
gsumsgrpccat.p + = ( +g𝐺 )
Assertion gsumccatOLD ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) )

Proof

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