Step | Hyp | Ref
| Expression |
1 | | oveq1 7180 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 ++ 𝑋) = (∅ ++ 𝑋)) |
2 | 1 | oveq2d 7189 |
. . 3
⊢ (𝑊 = ∅ → (𝐺 Σg
(𝑊 ++ 𝑋)) = (𝐺 Σg (∅ ++
𝑋))) |
3 | | oveq2 7181 |
. . . . 5
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) = (𝐺 Σg
∅)) |
4 | | eqid 2739 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | 4 | gsum0 18013 |
. . . . 5
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
6 | 3, 5 | eqtrdi 2790 |
. . . 4
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) =
(0g‘𝐺)) |
7 | 6 | oveq1d 7188 |
. . 3
⊢ (𝑊 = ∅ → ((𝐺 Σg
𝑊) + (𝐺 Σg 𝑋)) = ((0g‘𝐺) + (𝐺 Σg 𝑋))) |
8 | 2, 7 | eqeq12d 2755 |
. 2
⊢ (𝑊 = ∅ → ((𝐺 Σg
(𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (∅ ++
𝑋)) =
((0g‘𝐺)
+ (𝐺 Σg
𝑋)))) |
9 | | oveq2 7181 |
. . . . 5
⊢ (𝑋 = ∅ → (𝑊 ++ 𝑋) = (𝑊 ++ ∅)) |
10 | 9 | oveq2d 7189 |
. . . 4
⊢ (𝑋 = ∅ → (𝐺 Σg
(𝑊 ++ 𝑋)) = (𝐺 Σg (𝑊 ++ ∅))) |
11 | | oveq2 7181 |
. . . . . 6
⊢ (𝑋 = ∅ → (𝐺 Σg
𝑋) = (𝐺 Σg
∅)) |
12 | 11, 5 | eqtrdi 2790 |
. . . . 5
⊢ (𝑋 = ∅ → (𝐺 Σg
𝑋) =
(0g‘𝐺)) |
13 | 12 | oveq2d 7189 |
. . . 4
⊢ (𝑋 = ∅ → ((𝐺 Σg
𝑊) + (𝐺 Σg 𝑋)) = ((𝐺 Σg 𝑊) + (0g‘𝐺))) |
14 | 10, 13 | eqeq12d 2755 |
. . 3
⊢ (𝑋 = ∅ → ((𝐺 Σg
(𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg
𝑊) + (0g‘𝐺)))) |
15 | | gsumwcl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
16 | | gsumsgrpccat.p |
. . . . . 6
⊢ + =
(+g‘𝐺) |
17 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝐺 ∈ Mnd) |
18 | | lennncl 13978 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
19 | 18 | 3ad2antl2 1187 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
20 | 19 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℕ) |
21 | | lennncl 13978 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝑋 ≠ ∅) → (♯‘𝑋) ∈
ℕ) |
22 | 21 | 3ad2antl3 1188 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑋 ≠ ∅) → (♯‘𝑋) ∈
ℕ) |
23 | 22 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℕ) |
24 | 20, 23 | nnaddcld 11771 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) ∈
ℕ) |
25 | | nnm1nn0 12020 |
. . . . . . . 8
⊢
(((♯‘𝑊)
+ (♯‘𝑋)) ∈
ℕ → (((♯‘𝑊) + (♯‘𝑋)) − 1) ∈
ℕ0) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) ∈ ℕ0) |
27 | | nn0uz 12365 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
28 | 26, 27 | eleqtrdi 2844 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) ∈ (ℤ≥‘0)) |
29 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊 ∈ Word 𝐵) |
30 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋 ∈ Word 𝐵) |
31 | | ccatcl 14018 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝑊 ++ 𝑋) ∈ Word 𝐵) |
32 | 29, 30, 31 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋) ∈ Word 𝐵) |
33 | | wrdf 13963 |
. . . . . . . 8
⊢ ((𝑊 ++ 𝑋) ∈ Word 𝐵 → (𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵) |
35 | | ccatlen 14019 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (♯‘(𝑊 ++ 𝑋)) = ((♯‘𝑊) + (♯‘𝑋))) |
36 | 29, 30, 35 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘(𝑊 ++ 𝑋)) = ((♯‘𝑊) + (♯‘𝑋))) |
37 | 36 | oveq2d 7189 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘(𝑊 ++
𝑋))) =
(0..^((♯‘𝑊) +
(♯‘𝑋)))) |
38 | 20 | nnzd 12170 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℤ) |
39 | 23 | nnzd 12170 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℤ) |
40 | 38, 39 | zaddcld 12175 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) ∈
ℤ) |
41 | | fzoval 13133 |
. . . . . . . . . 10
⊢
(((♯‘𝑊)
+ (♯‘𝑋)) ∈
ℤ → (0..^((♯‘𝑊) + (♯‘𝑋))) = (0...(((♯‘𝑊) + (♯‘𝑋)) − 1))) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^((♯‘𝑊) +
(♯‘𝑋))) =
(0...(((♯‘𝑊) +
(♯‘𝑋)) −
1))) |
43 | 37, 42 | eqtrd 2774 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘(𝑊 ++
𝑋))) =
(0...(((♯‘𝑊) +
(♯‘𝑋)) −
1))) |
44 | 43 | feq2d 6491 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵 ↔ (𝑊 ++ 𝑋):(0...(((♯‘𝑊) + (♯‘𝑋)) − 1))⟶𝐵)) |
45 | 34, 44 | mpbid 235 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0...(((♯‘𝑊) + (♯‘𝑋)) − 1))⟶𝐵) |
46 | 15, 16, 17, 28, 45 | gsumval2 18015 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))) |
47 | | nnm1nn0 12020 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℕ0) |
48 | 20, 47 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) − 1) ∈
ℕ0) |
49 | 48, 27 | eleqtrdi 2844 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
50 | | wrdf 13963 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝐵 → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
51 | 29, 50 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
52 | | fzoval 13133 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
53 | 38, 52 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘𝑊)) =
(0...((♯‘𝑊)
− 1))) |
54 | 53 | feq2d 6491 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊:(0..^(♯‘𝑊))⟶𝐵 ↔ 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵)) |
55 | 51, 54 | mpbid 235 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵) |
56 | 15, 16, 17, 49, 55 | gsumval2 18015 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑊) = (seq0( + , 𝑊)‘((♯‘𝑊) − 1))) |
57 | | nnm1nn0 12020 |
. . . . . . . . . 10
⊢
((♯‘𝑋)
∈ ℕ → ((♯‘𝑋) − 1) ∈
ℕ0) |
58 | 23, 57 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑋) − 1) ∈
ℕ0) |
59 | 58, 27 | eleqtrdi 2844 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑋) − 1) ∈
(ℤ≥‘0)) |
60 | | wrdf 13963 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Word 𝐵 → 𝑋:(0..^(♯‘𝑋))⟶𝐵) |
61 | 30, 60 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0..^(♯‘𝑋))⟶𝐵) |
62 | | fzoval 13133 |
. . . . . . . . . . 11
⊢
((♯‘𝑋)
∈ ℤ → (0..^(♯‘𝑋)) = (0...((♯‘𝑋) − 1))) |
63 | 39, 62 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(0..^(♯‘𝑋)) =
(0...((♯‘𝑋)
− 1))) |
64 | 63 | feq2d 6491 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑋:(0..^(♯‘𝑋))⟶𝐵 ↔ 𝑋:(0...((♯‘𝑋) − 1))⟶𝐵)) |
65 | 61, 64 | mpbid 235 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0...((♯‘𝑋) − 1))⟶𝐵) |
66 | 15, 16, 17, 59, 65 | gsumval2 18015 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑋) = (seq0( + , 𝑋)‘((♯‘𝑋) − 1))) |
67 | 56, 66 | oveq12d 7191 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))) |
68 | 15, 16 | mndcl 18038 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
69 | 68 | 3expb 1121 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
70 | 17, 69 | sylan 583 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
71 | 15, 16 | mndass 18039 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
72 | 17, 71 | sylan 583 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
73 | | uzid 12342 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℤ → (♯‘𝑊) ∈
(ℤ≥‘(♯‘𝑊))) |
74 | 38, 73 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
(ℤ≥‘(♯‘𝑊))) |
75 | | uzaddcl 12389 |
. . . . . . . . . 10
⊢
(((♯‘𝑊)
∈ (ℤ≥‘(♯‘𝑊)) ∧ ((♯‘𝑋) − 1) ∈ ℕ0)
→ ((♯‘𝑊) +
((♯‘𝑋) −
1)) ∈ (ℤ≥‘(♯‘𝑊))) |
76 | 74, 58, 75 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + ((♯‘𝑋) − 1)) ∈
(ℤ≥‘(♯‘𝑊))) |
77 | 20 | nncnd 11735 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈
ℂ) |
78 | 23 | nncnd 11735 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈
ℂ) |
79 | | 1cnd 10717 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 1 ∈
ℂ) |
80 | 77, 78, 79 | addsubassd 11098 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) = ((♯‘𝑊) +
((♯‘𝑋) −
1))) |
81 | | ax-1cn 10676 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
82 | | npcan 10976 |
. . . . . . . . . . 11
⊢
(((♯‘𝑊)
∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑊) − 1) + 1) =
(♯‘𝑊)) |
83 | 77, 81, 82 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) −
1) + 1) = (♯‘𝑊)) |
84 | 83 | fveq2d 6681 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(ℤ≥‘(((♯‘𝑊) − 1) + 1)) =
(ℤ≥‘(♯‘𝑊))) |
85 | 76, 80, 84 | 3eltr4d 2849 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) ∈ (ℤ≥‘(((♯‘𝑊) − 1) + 1))) |
86 | 45 | ffvelrnda 6864 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...(((♯‘𝑊) + (♯‘𝑋)) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) ∈ 𝐵) |
87 | 70, 72, 85, 49, 86 | seqsplit 13498 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = ((seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) + (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)))) |
88 | | simpll2 1214 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝐵) |
89 | | simpll3 1215 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑋 ∈ Word 𝐵) |
90 | 53 | eleq2d 2819 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1)))) |
91 | 90 | biimpar 481 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑥 ∈
(0..^(♯‘𝑊))) |
92 | | ccatval1 14022 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊‘𝑥)) |
93 | 88, 89, 91, 92 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊‘𝑥)) |
94 | 49, 93 | seqfveq 13489 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) = (seq0( + , 𝑊)‘((♯‘𝑊) − 1))) |
95 | 77 | addid2d 10922 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0 +
(♯‘𝑊)) =
(♯‘𝑊)) |
96 | 83, 95 | eqtr4d 2777 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) −
1) + 1) = (0 + (♯‘𝑊))) |
97 | 96 | seqeq1d 13469 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
seq(((♯‘𝑊)
− 1) + 1)( + , (𝑊 ++ 𝑋)) = seq(0 + (♯‘𝑊))( + , (𝑊 ++ 𝑋))) |
98 | 77, 78 | addcomd 10923 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) = ((♯‘𝑋) + (♯‘𝑊))) |
99 | 98 | oveq1d 7188 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) = (((♯‘𝑋) +
(♯‘𝑊)) −
1)) |
100 | 78, 77, 79 | addsubd 11099 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑋) +
(♯‘𝑊)) −
1) = (((♯‘𝑋)
− 1) + (♯‘𝑊))) |
101 | 99, 100 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(((♯‘𝑊) +
(♯‘𝑋)) −
1) = (((♯‘𝑋)
− 1) + (♯‘𝑊))) |
102 | 97, 101 | fveq12d 6684 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(seq(((♯‘𝑊)
− 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = (seq(0 +
(♯‘𝑊))( + , (𝑊 ++ 𝑋))‘(((♯‘𝑋) − 1) + (♯‘𝑊)))) |
103 | | simpll2 1214 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑊 ∈ Word 𝐵) |
104 | | simpll3 1215 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑋 ∈ Word 𝐵) |
105 | 63 | eleq2d 2819 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(♯‘𝑋)) ↔ 𝑥 ∈ (0...((♯‘𝑋) − 1)))) |
106 | 105 | biimpar 481 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑥 ∈
(0..^(♯‘𝑋))) |
107 | | ccatval3 14025 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑋))) → ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))) = (𝑋‘𝑥)) |
108 | 103, 104,
106, 107 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))) = (𝑋‘𝑥)) |
109 | 108 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → (𝑋‘𝑥) = ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊)))) |
110 | 59, 38, 109 | seqshft2 13491 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , 𝑋)‘((♯‘𝑋) − 1)) = (seq(0 +
(♯‘𝑊))( + , (𝑊 ++ 𝑋))‘(((♯‘𝑋) − 1) + (♯‘𝑊)))) |
111 | 102, 110 | eqtr4d 2777 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) →
(seq(((♯‘𝑊)
− 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = (seq0( + , 𝑋)‘((♯‘𝑋) − 1))) |
112 | 94, 111 | oveq12d 7191 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) + (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))) |
113 | 87, 112 | eqtrd 2774 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))) |
114 | 67, 113 | eqtr4d 2777 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))) |
115 | 46, 114 | eqtr4d 2777 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
116 | 115 | anassrs 471 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
117 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝐵) |
118 | | ccatrid 14033 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐵 → (𝑊 ++ ∅) = 𝑊) |
119 | 117, 118 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊 ++ ∅) = 𝑊) |
120 | 119 | oveq2d 7189 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = (𝐺 Σg
𝑊)) |
121 | | simpl1 1192 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐺 ∈ Mnd) |
122 | 15 | gsumwcl 18122 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
123 | 122 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
124 | 123 | adantr 484 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) ∈ 𝐵) |
125 | 15, 16, 4 | mndrid 18051 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝐺 Σg
𝑊) ∈ 𝐵) → ((𝐺 Σg 𝑊) + (0g‘𝐺)) = (𝐺 Σg 𝑊)) |
126 | 121, 124,
125 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((𝐺 Σg 𝑊) + (0g‘𝐺)) = (𝐺 Σg 𝑊)) |
127 | 120, 126 | eqtr4d 2777 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg
𝑊) + (0g‘𝐺))) |
128 | 14, 116, 127 | pm2.61ne 3020 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
129 | | ccatlid 14032 |
. . . . 5
⊢ (𝑋 ∈ Word 𝐵 → (∅ ++ 𝑋) = 𝑋) |
130 | 129 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (∅ ++ 𝑋) = 𝑋) |
131 | 130 | oveq2d 7189 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++
𝑋)) = (𝐺 Σg 𝑋)) |
132 | | simp1 1137 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → 𝐺 ∈ Mnd) |
133 | 15 | gsumwcl 18122 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵) |
134 | 15, 16, 4 | mndlid 18050 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝐺 Σg
𝑋) ∈ 𝐵) → ((0g‘𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋)) |
135 | 132, 133,
134 | 3imp3i2an 1346 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → ((0g‘𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋)) |
136 | 131, 135 | eqtr4d 2777 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++
𝑋)) =
((0g‘𝐺)
+ (𝐺 Σg
𝑋))) |
137 | 8, 128, 136 | pm2.61ne 3020 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |