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