| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝐺 ∈ Smgrp) |
| 2 | | sgrpmgm 18737 |
. . . . . . 7
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) |
| 3 | | gsumwcl.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
| 4 | | gsumsgrpccat.p |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
| 5 | 3, 4 | mgmcl 18656 |
. . . . . . 7
⊢ ((𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
| 6 | 2, 5 | syl3an1 1164 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
| 7 | 6 | 3expb 1121 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
| 8 | 1, 7 | sylan 580 |
. . . 4
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
| 9 | 3, 4 | sgrpass 18738 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 10 | 1, 9 | sylan 580 |
. . . 4
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 11 | | lennncl 14572 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
| 12 | 11 | ad2ant2r 747 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℕ) |
| 13 | 12 | 3adant1 1131 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℕ) |
| 14 | 13 | nnzd 12640 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℤ) |
| 15 | 14 | uzidd 12894 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
(ℤ≥‘(♯‘𝑊))) |
| 16 | | lennncl 14572 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝑋 ≠ ∅) → (♯‘𝑋) ∈
ℕ) |
| 17 | 16 | ad2ant2l 746 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℕ) |
| 18 | 17 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℕ) |
| 19 | | nnm1nn0 12567 |
. . . . . . 7
⊢
((♯‘𝑋)
∈ ℕ → ((♯‘𝑋) − 1) ∈
ℕ0) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑋) − 1) ∈
ℕ0) |
| 21 | | uzaddcl 12946 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ (ℤ≥‘(♯‘𝑊)) ∧ ((♯‘𝑋) − 1) ∈ ℕ0)
→ ((♯‘𝑊) +
((♯‘𝑋) −
1)) ∈ (ℤ≥‘(♯‘𝑊))) |
| 22 | 15, 20, 21 | syl2anc 584 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + ((♯‘𝑋) − 1)) ∈
(ℤ≥‘(♯‘𝑊))) |
| 23 | 13 | nncnd 12282 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℂ) |
| 24 | 18 | nncnd 12282 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℂ) |
| 25 | | 1cnd 11256 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 1 ∈
ℂ) |
| 26 | 23, 24, 25 | addsubassd 11640 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) = ((♯‘𝑊) +
((♯‘𝑋) −
1))) |
| 27 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 28 | | npcan 11517 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑊) − 1) + 1) =
(♯‘𝑊)) |
| 29 | 23, 27, 28 | sylancl 586 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) −
1) + 1) = (♯‘𝑊)) |
| 30 | 29 | fveq2d 6910 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(ℤ≥‘(((♯‘𝑊) − 1) + 1)) =
(ℤ≥‘(♯‘𝑊))) |
| 31 | 22, 26, 30 | 3eltr4d 2856 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) ∈ (ℤ≥‘(((♯‘𝑊) − 1) + 1))) |
| 32 | | nnm1nn0 12567 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℕ0) |
| 33 | 13, 32 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) − 1) ∈
ℕ0) |
| 34 | | nn0uz 12920 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
| 35 | 33, 34 | eleqtrdi 2851 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
| 36 | | ccatcl 14612 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝑊 ++ 𝑋) ∈ Word 𝐵) |
| 37 | 36 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋) ∈ Word 𝐵) |
| 38 | | wrdf 14557 |
. . . . . . 7
⊢ ((𝑊 ++ 𝑋) ∈ Word 𝐵 → (𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵) |
| 39 | 37, 38 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵) |
| 40 | | ccatlen 14613 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (♯‘(𝑊 ++ 𝑋)) = ((♯‘𝑊) + (♯‘𝑋))) |
| 41 | 40 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘(𝑊 ++ 𝑋)) = ((♯‘𝑊) + (♯‘𝑋))) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘(𝑊 ++
𝑋))) =
(0..^((♯‘𝑊) +
(♯‘𝑋)))) |
| 43 | 18 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℤ) |
| 44 | 14, 43 | zaddcld 12726 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) ∈
ℤ) |
| 45 | | fzoval 13700 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
+ (♯‘𝑋)) ∈
ℤ → (0..^((♯‘𝑊) + (♯‘𝑋))) = (0...(((♯‘𝑊) + (♯‘𝑋)) − 1))) |
| 46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^((♯‘𝑊) +
(♯‘𝑋))) =
(0...(((♯‘𝑊) +
(♯‘𝑋)) −
1))) |
| 47 | 42, 46 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘(𝑊 ++
𝑋))) =
(0...(((♯‘𝑊) +
(♯‘𝑋)) −
1))) |
| 48 | 47 | feq2d 6722 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵 ↔ (𝑊 ++ 𝑋):(0...(((♯‘𝑊) + (♯‘𝑋)) − 1))⟶𝐵)) |
| 49 | 39, 48 | mpbid 232 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0...(((♯‘𝑊) + (♯‘𝑋)) − 1))⟶𝐵) |
| 50 | 49 | ffvelcdmda 7104 |
. . . 4
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...(((♯‘𝑊) + (♯‘𝑋)) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) ∈ 𝐵) |
| 51 | 8, 10, 31, 35, 50 | seqsplit 14076 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = ((seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) + (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)))) |
| 52 | | simpl2l 1227 |
. . . . . 6
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝐵) |
| 53 | | simpl2r 1228 |
. . . . . 6
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑋 ∈ Word 𝐵) |
| 54 | | fzoval 13700 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
| 55 | 14, 54 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘𝑊)) =
(0...((♯‘𝑊)
− 1))) |
| 56 | 55 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1)))) |
| 57 | 56 | biimpar 477 |
. . . . . 6
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑥 ∈
(0..^(♯‘𝑊))) |
| 58 | | ccatval1 14615 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊‘𝑥)) |
| 59 | 52, 53, 57, 58 | syl3anc 1373 |
. . . . 5
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊‘𝑥)) |
| 60 | 35, 59 | seqfveq 14067 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) = (seq0( + , 𝑊)‘((♯‘𝑊) − 1))) |
| 61 | 23 | addlidd 11462 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0 +
(♯‘𝑊)) =
(♯‘𝑊)) |
| 62 | 29, 61 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) −
1) + 1) = (0 + (♯‘𝑊))) |
| 63 | 62 | seqeq1d 14048 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
seq(((♯‘𝑊)
− 1) + 1)( + , (𝑊 ++ 𝑋)) = seq(0 + (♯‘𝑊))( + , (𝑊 ++ 𝑋))) |
| 64 | 23, 24 | addcomd 11463 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) = ((♯‘𝑋) + (♯‘𝑊))) |
| 65 | 64 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) = (((♯‘𝑋) +
(♯‘𝑊)) −
1)) |
| 66 | 24, 23, 25 | addsubd 11641 |
. . . . . . 7
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑋) +
(♯‘𝑊)) −
1) = (((♯‘𝑋)
− 1) + (♯‘𝑊))) |
| 67 | 65, 66 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) = (((♯‘𝑋)
− 1) + (♯‘𝑊))) |
| 68 | 63, 67 | fveq12d 6913 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(seq(((♯‘𝑊)
− 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = (seq(0 +
(♯‘𝑊))( + , (𝑊 ++ 𝑋))‘(((♯‘𝑋) − 1) + (♯‘𝑊)))) |
| 69 | 20, 34 | eleqtrdi 2851 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑋) − 1) ∈
(ℤ≥‘0)) |
| 70 | | simpl2l 1227 |
. . . . . . . 8
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑊 ∈ Word 𝐵) |
| 71 | | simpl2r 1228 |
. . . . . . . 8
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑋 ∈ Word 𝐵) |
| 72 | | fzoval 13700 |
. . . . . . . . . . 11
⊢
((♯‘𝑋)
∈ ℤ → (0..^(♯‘𝑋)) = (0...((♯‘𝑋) − 1))) |
| 73 | 43, 72 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘𝑋)) =
(0...((♯‘𝑋)
− 1))) |
| 74 | 73 | eleq2d 2827 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(♯‘𝑋)) ↔ 𝑥 ∈ (0...((♯‘𝑋) − 1)))) |
| 75 | 74 | biimpar 477 |
. . . . . . . 8
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑥 ∈
(0..^(♯‘𝑋))) |
| 76 | | ccatval3 14617 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑋))) → ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))) = (𝑋‘𝑥)) |
| 77 | 70, 71, 75, 76 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))) = (𝑋‘𝑥)) |
| 78 | 77 | eqcomd 2743 |
. . . . . 6
⊢ (((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → (𝑋‘𝑥) = ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊)))) |
| 79 | 69, 14, 78 | seqshft2 14069 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , 𝑋)‘((♯‘𝑋) − 1)) = (seq(0 +
(♯‘𝑊))( + , (𝑊 ++ 𝑋))‘(((♯‘𝑋) − 1) + (♯‘𝑊)))) |
| 80 | 68, 79 | eqtr4d 2780 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(seq(((♯‘𝑊)
− 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = (seq0( + , 𝑋)‘((♯‘𝑋) − 1))) |
| 81 | 60, 80 | oveq12d 7449 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) + (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))) |
| 82 | 51, 81 | eqtrd 2777 |
. 2
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))) |
| 83 | 13, 18 | nnaddcld 12318 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) ∈
ℕ) |
| 84 | | nnm1nn0 12567 |
. . . . 5
⊢
(((♯‘𝑊)
+ (♯‘𝑋)) ∈
ℕ → (((♯‘𝑊) + (♯‘𝑋)) − 1) ∈
ℕ0) |
| 85 | 83, 84 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) ∈ ℕ0) |
| 86 | 85, 34 | eleqtrdi 2851 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) ∈ (ℤ≥‘0)) |
| 87 | 3, 4, 1, 86, 49 | gsumval2 18699 |
. 2
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))) |
| 88 | | simp2l 1200 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊 ∈ Word 𝐵) |
| 89 | | wrdf 14557 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐵 → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
| 90 | 88, 89 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
| 91 | 55 | feq2d 6722 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊:(0..^(♯‘𝑊))⟶𝐵 ↔ 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵)) |
| 92 | 90, 91 | mpbid 232 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵) |
| 93 | 3, 4, 1, 35, 92 | gsumval2 18699 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑊) = (seq0( + , 𝑊)‘((♯‘𝑊) − 1))) |
| 94 | | simp2r 1201 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋 ∈ Word 𝐵) |
| 95 | | wrdf 14557 |
. . . . . 6
⊢ (𝑋 ∈ Word 𝐵 → 𝑋:(0..^(♯‘𝑋))⟶𝐵) |
| 96 | 94, 95 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0..^(♯‘𝑋))⟶𝐵) |
| 97 | 73 | feq2d 6722 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑋:(0..^(♯‘𝑋))⟶𝐵 ↔ 𝑋:(0...((♯‘𝑋) − 1))⟶𝐵)) |
| 98 | 96, 97 | mpbid 232 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0...((♯‘𝑋) − 1))⟶𝐵) |
| 99 | 3, 4, 1, 69, 98 | gsumval2 18699 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑋) = (seq0( + , 𝑋)‘((♯‘𝑋) − 1))) |
| 100 | 93, 99 | oveq12d 7449 |
. 2
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))) |
| 101 | 82, 87, 100 | 3eqtr4d 2787 |
1
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |