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

Proof

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