Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 ++ 𝑋) = (∅ ++ 𝑋)) |
2 | 1 | oveq2d 6666 |
. . 3
⊢ (𝑊 = ∅ → (𝐺 Σg
(𝑊 ++ 𝑋)) = (𝐺 Σg (∅ ++
𝑋))) |
3 | | oveq2 6658 |
. . . . 5
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) = (𝐺 Σg
∅)) |
4 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | 4 | gsum0 17278 |
. . . . 5
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
6 | 3, 5 | syl6eq 2672 |
. . . 4
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) =
(0g‘𝐺)) |
7 | 6 | oveq1d 6665 |
. . 3
⊢ (𝑊 = ∅ → ((𝐺 Σg
𝑊) + (𝐺 Σg 𝑋)) = ((0g‘𝐺) + (𝐺 Σg 𝑋))) |
8 | 2, 7 | eqeq12d 2637 |
. 2
⊢ (𝑊 = ∅ → ((𝐺 Σg
(𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (∅ ++
𝑋)) =
((0g‘𝐺)
+ (𝐺 Σg
𝑋)))) |
9 | | oveq2 6658 |
. . . . 5
⊢ (𝑋 = ∅ → (𝑊 ++ 𝑋) = (𝑊 ++ ∅)) |
10 | 9 | oveq2d 6666 |
. . . 4
⊢ (𝑋 = ∅ → (𝐺 Σg
(𝑊 ++ 𝑋)) = (𝐺 Σg (𝑊 ++ ∅))) |
11 | | oveq2 6658 |
. . . . . 6
⊢ (𝑋 = ∅ → (𝐺 Σg
𝑋) = (𝐺 Σg
∅)) |
12 | 11, 5 | syl6eq 2672 |
. . . . 5
⊢ (𝑋 = ∅ → (𝐺 Σg
𝑋) =
(0g‘𝐺)) |
13 | 12 | oveq2d 6666 |
. . . 4
⊢ (𝑋 = ∅ → ((𝐺 Σg
𝑊) + (𝐺 Σg 𝑋)) = ((𝐺 Σg 𝑊) + (0g‘𝐺))) |
14 | 10, 13 | eqeq12d 2637 |
. . 3
⊢ (𝑋 = ∅ → ((𝐺 Σg
(𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg
𝑊) + (0g‘𝐺)))) |
15 | | gsumwcl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
16 | | gsumccat.p |
. . . . . 6
⊢ + =
(+g‘𝐺) |
17 | | simpl1 1064 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝐺 ∈ Mnd) |
18 | | lennncl 13325 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
19 | 18 | 3ad2antl2 1224 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
20 | 19 | adantrr 753 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈
ℕ) |
21 | | lennncl 13325 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝑋 ≠ ∅) → (#‘𝑋) ∈
ℕ) |
22 | 21 | 3ad2antl3 1225 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑋 ≠ ∅) → (#‘𝑋) ∈
ℕ) |
23 | 22 | adantrl 752 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑋) ∈
ℕ) |
24 | 20, 23 | nnaddcld 11067 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + (#‘𝑋)) ∈ ℕ) |
25 | | nnm1nn0 11334 |
. . . . . . . 8
⊢
(((#‘𝑊) +
(#‘𝑋)) ∈ ℕ
→ (((#‘𝑊) +
(#‘𝑋)) − 1)
∈ ℕ0) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) ∈
ℕ0) |
27 | | nn0uz 11722 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
28 | 26, 27 | syl6eleq 2711 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) ∈
(ℤ≥‘0)) |
29 | | simpl2 1065 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊 ∈ Word 𝐵) |
30 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋 ∈ Word 𝐵) |
31 | | ccatcl 13359 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝑊 ++ 𝑋) ∈ Word 𝐵) |
32 | 29, 30, 31 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋) ∈ Word 𝐵) |
33 | | wrdf 13310 |
. . . . . . . 8
⊢ ((𝑊 ++ 𝑋) ∈ Word 𝐵 → (𝑊 ++ 𝑋):(0..^(#‘(𝑊 ++ 𝑋)))⟶𝐵) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0..^(#‘(𝑊 ++ 𝑋)))⟶𝐵) |
35 | | ccatlen 13360 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (#‘(𝑊 ++ 𝑋)) = ((#‘𝑊) + (#‘𝑋))) |
36 | 29, 30, 35 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘(𝑊 ++ 𝑋)) = ((#‘𝑊) + (#‘𝑋))) |
37 | 36 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘(𝑊 ++ 𝑋))) = (0..^((#‘𝑊) + (#‘𝑋)))) |
38 | 20 | nnzd 11481 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈
ℤ) |
39 | 23 | nnzd 11481 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑋) ∈
ℤ) |
40 | 38, 39 | zaddcld 11486 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + (#‘𝑋)) ∈ ℤ) |
41 | | fzoval 12471 |
. . . . . . . . . 10
⊢
(((#‘𝑊) +
(#‘𝑋)) ∈ ℤ
→ (0..^((#‘𝑊) +
(#‘𝑋))) =
(0...(((#‘𝑊) +
(#‘𝑋)) −
1))) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^((#‘𝑊) + (#‘𝑋))) = (0...(((#‘𝑊) + (#‘𝑋)) − 1))) |
43 | 37, 42 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘(𝑊 ++ 𝑋))) = (0...(((#‘𝑊) + (#‘𝑋)) − 1))) |
44 | 43 | feq2d 6031 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝑊 ++ 𝑋):(0..^(#‘(𝑊 ++ 𝑋)))⟶𝐵 ↔ (𝑊 ++ 𝑋):(0...(((#‘𝑊) + (#‘𝑋)) − 1))⟶𝐵)) |
45 | 34, 44 | mpbid 222 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0...(((#‘𝑊) + (#‘𝑋)) − 1))⟶𝐵) |
46 | 15, 16, 17, 28, 45 | gsumval2 17280 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1))) |
47 | | nnm1nn0 11334 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ ℕ0) |
48 | 20, 47 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) − 1) ∈
ℕ0) |
49 | 48, 27 | syl6eleq 2711 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) − 1) ∈
(ℤ≥‘0)) |
50 | | wrdf 13310 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐵 → 𝑊:(0..^(#‘𝑊))⟶𝐵) |
51 | 29, 50 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0..^(#‘𝑊))⟶𝐵) |
52 | | fzoval 12471 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℤ → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
53 | 38, 52 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
54 | 53 | feq2d 6031 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊:(0..^(#‘𝑊))⟶𝐵 ↔ 𝑊:(0...((#‘𝑊) − 1))⟶𝐵)) |
55 | 51, 54 | mpbid 222 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0...((#‘𝑊) − 1))⟶𝐵) |
56 | 15, 16, 17, 49, 55 | gsumval2 17280 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑊) = (seq0( + , 𝑊)‘((#‘𝑊) − 1))) |
57 | | nnm1nn0 11334 |
. . . . . . . . . 10
⊢
((#‘𝑋) ∈
ℕ → ((#‘𝑋)
− 1) ∈ ℕ0) |
58 | 23, 57 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑋) − 1) ∈
ℕ0) |
59 | 58, 27 | syl6eleq 2711 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑋) − 1) ∈
(ℤ≥‘0)) |
60 | | wrdf 13310 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Word 𝐵 → 𝑋:(0..^(#‘𝑋))⟶𝐵) |
61 | 30, 60 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0..^(#‘𝑋))⟶𝐵) |
62 | | fzoval 12471 |
. . . . . . . . . . 11
⊢
((#‘𝑋) ∈
ℤ → (0..^(#‘𝑋)) = (0...((#‘𝑋) − 1))) |
63 | 39, 62 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘𝑋)) = (0...((#‘𝑋) − 1))) |
64 | 63 | feq2d 6031 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑋:(0..^(#‘𝑋))⟶𝐵 ↔ 𝑋:(0...((#‘𝑋) − 1))⟶𝐵)) |
65 | 61, 64 | mpbid 222 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0...((#‘𝑋) − 1))⟶𝐵) |
66 | 15, 16, 17, 59, 65 | gsumval2 17280 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑋) = (seq0( + , 𝑋)‘((#‘𝑋) − 1))) |
67 | 56, 66 | oveq12d 6668 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((seq0( + , 𝑊)‘((#‘𝑊) − 1)) + (seq0( + , 𝑋)‘((#‘𝑋) − 1)))) |
68 | 15, 16 | mndcl 17301 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
69 | 68 | 3expb 1266 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
70 | 17, 69 | sylan 488 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
71 | 15, 16 | mndass 17302 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
72 | 17, 71 | sylan 488 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
73 | | uzid 11702 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℤ → (#‘𝑊)
∈ (ℤ≥‘(#‘𝑊))) |
74 | 38, 73 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈
(ℤ≥‘(#‘𝑊))) |
75 | | uzaddcl 11744 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
(ℤ≥‘(#‘𝑊)) ∧ ((#‘𝑋) − 1) ∈ ℕ0)
→ ((#‘𝑊) +
((#‘𝑋) − 1))
∈ (ℤ≥‘(#‘𝑊))) |
76 | 74, 58, 75 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + ((#‘𝑋) − 1)) ∈
(ℤ≥‘(#‘𝑊))) |
77 | 20 | nncnd 11036 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈
ℂ) |
78 | 23 | nncnd 11036 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑋) ∈
ℂ) |
79 | | 1cnd 10056 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 1 ∈
ℂ) |
80 | 77, 78, 79 | addsubassd 10412 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) = ((#‘𝑊) + ((#‘𝑋) − 1))) |
81 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
82 | | npcan 10290 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℂ ∧ 1 ∈ ℂ) → (((#‘𝑊) − 1) + 1) = (#‘𝑊)) |
83 | 77, 81, 82 | sylancl 694 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) − 1) + 1) =
(#‘𝑊)) |
84 | 83 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(ℤ≥‘(((#‘𝑊) − 1) + 1)) =
(ℤ≥‘(#‘𝑊))) |
85 | 76, 80, 84 | 3eltr4d 2716 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) ∈
(ℤ≥‘(((#‘𝑊) − 1) + 1))) |
86 | 45 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...(((#‘𝑊) + (#‘𝑋)) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) ∈ 𝐵) |
87 | 70, 72, 85, 49, 86 | seqsplit 12834 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = ((seq0( + , (𝑊 ++ 𝑋))‘((#‘𝑊) − 1)) + (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)))) |
88 | | simpll2 1101 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → 𝑊 ∈ Word 𝐵) |
89 | | simpll3 1102 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → 𝑋 ∈ Word 𝐵) |
90 | 53 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(#‘𝑊)) ↔ 𝑥 ∈ (0...((#‘𝑊) − 1)))) |
91 | 90 | biimpar 502 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → 𝑥 ∈ (0..^(#‘𝑊))) |
92 | | ccatval1 13361 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊‘𝑥)) |
93 | 88, 89, 91, 92 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊‘𝑥)) |
94 | 49, 93 | seqfveq 12825 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘((#‘𝑊) − 1)) = (seq0( + , 𝑊)‘((#‘𝑊) − 1))) |
95 | 77 | addid2d 10237 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0 + (#‘𝑊)) = (#‘𝑊)) |
96 | 83, 95 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) − 1) + 1) = (0 +
(#‘𝑊))) |
97 | 96 | seqeq1d 12807 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋)) = seq(0 + (#‘𝑊))( + , (𝑊 ++ 𝑋))) |
98 | 77, 78 | addcomd 10238 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + (#‘𝑋)) = ((#‘𝑋) + (#‘𝑊))) |
99 | 98 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) = (((#‘𝑋) + (#‘𝑊)) − 1)) |
100 | 78, 77, 79 | addsubd 10413 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑋) + (#‘𝑊)) − 1) = (((#‘𝑋) − 1) + (#‘𝑊))) |
101 | 99, 100 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) = (((#‘𝑋) − 1) + (#‘𝑊))) |
102 | 97, 101 | fveq12d 6197 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = (seq(0 + (#‘𝑊))( + , (𝑊 ++ 𝑋))‘(((#‘𝑋) − 1) + (#‘𝑊)))) |
103 | | simpll2 1101 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → 𝑊 ∈ Word 𝐵) |
104 | | simpll3 1102 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → 𝑋 ∈ Word 𝐵) |
105 | 63 | eleq2d 2687 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(#‘𝑋)) ↔ 𝑥 ∈ (0...((#‘𝑋) − 1)))) |
106 | 105 | biimpar 502 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → 𝑥 ∈ (0..^(#‘𝑋))) |
107 | | ccatval3 13363 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘𝑋))) → ((𝑊 ++ 𝑋)‘(𝑥 + (#‘𝑊))) = (𝑋‘𝑥)) |
108 | 103, 104,
106, 107 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → ((𝑊 ++ 𝑋)‘(𝑥 + (#‘𝑊))) = (𝑋‘𝑥)) |
109 | 108 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → (𝑋‘𝑥) = ((𝑊 ++ 𝑋)‘(𝑥 + (#‘𝑊)))) |
110 | 59, 38, 109 | seqshft2 12827 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , 𝑋)‘((#‘𝑋) − 1)) = (seq(0 +
(#‘𝑊))( + , (𝑊 ++ 𝑋))‘(((#‘𝑋) − 1) + (#‘𝑊)))) |
111 | 102, 110 | eqtr4d 2659 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = (seq0( + , 𝑋)‘((#‘𝑋) − 1))) |
112 | 94, 111 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((seq0( + , (𝑊 ++ 𝑋))‘((#‘𝑊) − 1)) + (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1))) = ((seq0( + , 𝑊)‘((#‘𝑊) − 1)) + (seq0( + , 𝑋)‘((#‘𝑋) − 1)))) |
113 | 87, 112 | eqtrd 2656 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = ((seq0( + , 𝑊)‘((#‘𝑊) − 1)) + (seq0( + , 𝑋)‘((#‘𝑋) − 1)))) |
114 | 67, 113 | eqtr4d 2659 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1))) |
115 | 46, 114 | eqtr4d 2659 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
116 | 115 | anassrs 680 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
117 | | simpl2 1065 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝐵) |
118 | | ccatrid 13370 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐵 → (𝑊 ++ ∅) = 𝑊) |
119 | 117, 118 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊 ++ ∅) = 𝑊) |
120 | 119 | oveq2d 6666 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = (𝐺 Σg
𝑊)) |
121 | | simpl1 1064 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐺 ∈ Mnd) |
122 | 15 | gsumwcl 17377 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
123 | 122 | 3adant3 1081 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
124 | 123 | adantr 481 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) ∈ 𝐵) |
125 | 15, 16, 4 | mndrid 17312 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝐺 Σg
𝑊) ∈ 𝐵) → ((𝐺 Σg 𝑊) + (0g‘𝐺)) = (𝐺 Σg 𝑊)) |
126 | 121, 124,
125 | syl2anc 693 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((𝐺 Σg 𝑊) + (0g‘𝐺)) = (𝐺 Σg 𝑊)) |
127 | 120, 126 | eqtr4d 2659 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg
𝑊) + (0g‘𝐺))) |
128 | 14, 116, 127 | pm2.61ne 2879 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
129 | | ccatlid 13369 |
. . . . 5
⊢ (𝑋 ∈ Word 𝐵 → (∅ ++ 𝑋) = 𝑋) |
130 | 129 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (∅ ++ 𝑋) = 𝑋) |
131 | 130 | oveq2d 6666 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++
𝑋)) = (𝐺 Σg 𝑋)) |
132 | | simp1 1061 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → 𝐺 ∈ Mnd) |
133 | 15 | gsumwcl 17377 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵) |
134 | 133 | 3adant2 1080 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵) |
135 | 15, 16, 4 | mndlid 17311 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝐺 Σg
𝑋) ∈ 𝐵) → ((0g‘𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋)) |
136 | 132, 134,
135 | syl2anc 693 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → ((0g‘𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋)) |
137 | 131, 136 | eqtr4d 2659 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++
𝑋)) =
((0g‘𝐺)
+ (𝐺 Σg
𝑋))) |
138 | 8, 128, 137 | pm2.61ne 2879 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |