Proof of Theorem gsmsymgrfixlem1
Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝐵 → (#‘𝑊) ∈
ℕ0) |
2 | | elnn0uz 11725 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℕ0 ↔ (#‘𝑊) ∈
(ℤ≥‘0)) |
3 | 1, 2 | sylib 208 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐵 → (#‘𝑊) ∈
(ℤ≥‘0)) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → (#‘𝑊) ∈
(ℤ≥‘0)) |
5 | 4 | 3ad2ant1 1082 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (#‘𝑊) ∈
(ℤ≥‘0)) |
6 | | fzosplitsn 12576 |
. . . . 5
⊢
((#‘𝑊) ∈
(ℤ≥‘0) → (0..^((#‘𝑊) + 1)) = ((0..^(#‘𝑊)) ∪ {(#‘𝑊)})) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (0..^((#‘𝑊) + 1)) = ((0..^(#‘𝑊)) ∪ {(#‘𝑊)})) |
8 | 7 | raleqdv 3144 |
. . 3
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((#‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ ((0..^(#‘𝑊)) ∪ {(#‘𝑊)})(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) |
9 | 1 | adantr 481 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → (#‘𝑊) ∈
ℕ0) |
10 | 9 | 3ad2ant1 1082 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (#‘𝑊) ∈
ℕ0) |
11 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑖 = (#‘𝑊) → ((𝑊 ++ 〈“𝑃”〉)‘𝑖) = ((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))) |
12 | 11 | fveq1d 6193 |
. . . . . 6
⊢ (𝑖 = (#‘𝑊) → (((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾)) |
13 | 12 | eqeq1d 2624 |
. . . . 5
⊢ (𝑖 = (#‘𝑊) → ((((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾)) |
14 | 13 | ralunsn 4422 |
. . . 4
⊢
((#‘𝑊) ∈
ℕ0 → (∀𝑖 ∈ ((0..^(#‘𝑊)) ∪ {(#‘𝑊)})(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ∧ (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾))) |
15 | 10, 14 | syl 17 |
. . 3
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ ((0..^(#‘𝑊)) ∪ {(#‘𝑊)})(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ∧ (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾))) |
16 | 8, 15 | bitrd 268 |
. 2
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((#‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ∧ (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾))) |
17 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → 𝑊 ∈ Word 𝐵) |
18 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → 𝑃 ∈ 𝐵) |
19 | | eqidd 2623 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → (#‘𝑊) = (#‘𝑊)) |
20 | 17, 18, 19 | 3jca 1242 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ (#‘𝑊) = (#‘𝑊))) |
21 | 20 | adantr 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → (𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ (#‘𝑊) = (#‘𝑊))) |
22 | | ccats1val2 13404 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ (#‘𝑊) = (#‘𝑊)) → ((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊)) = 𝑃) |
23 | 22 | fveq1d 6193 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ (#‘𝑊) = (#‘𝑊)) → (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = (𝑃‘𝐾)) |
24 | 23 | eqeq1d 2624 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ (#‘𝑊) = (#‘𝑊)) → ((((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾 ↔ (𝑃‘𝐾) = 𝐾)) |
25 | 21, 24 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → ((((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾 ↔ (𝑃‘𝐾) = 𝐾)) |
26 | 25 | 3adant3 1081 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → ((((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾 ↔ (𝑃‘𝐾) = 𝐾)) |
27 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → 𝑁 ∈ Fin) |
28 | 27 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → 𝑁 ∈ Fin) |
29 | 17 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → 𝑊 ∈ Word 𝐵) |
30 | 18 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → 𝑃 ∈ 𝐵) |
31 | 28, 29, 30 | 3jca 1242 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵)) |
32 | 31 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵)) |
33 | 32 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → (𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵)) |
34 | | gsmsymgrfix.s |
. . . . . . . . . 10
⊢ 𝑆 = (SymGrp‘𝑁) |
35 | | gsmsymgrfix.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑆) |
36 | 34, 35 | gsumccatsymgsn 17846 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → (𝑆 Σg (𝑊 ++ 〈“𝑃”〉)) = ((𝑆 Σg
𝑊) ∘ 𝑃)) |
37 | 36 | fveq1d 6193 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = (((𝑆 Σg 𝑊) ∘ 𝑃)‘𝐾)) |
38 | 33, 37 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = (((𝑆 Σg 𝑊) ∘ 𝑃)‘𝐾)) |
39 | 34, 35 | symgbasf 17804 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ 𝐵 → 𝑃:𝑁⟶𝑁) |
40 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝑃:𝑁⟶𝑁 → 𝑃 Fn 𝑁) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ 𝐵 → 𝑃 Fn 𝑁) |
42 | 41 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) → 𝑃 Fn 𝑁) |
43 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → 𝐾 ∈ 𝑁) |
44 | 42, 43 | anim12i 590 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → (𝑃 Fn 𝑁 ∧ 𝐾 ∈ 𝑁)) |
45 | 44 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (𝑃 Fn 𝑁 ∧ 𝐾 ∈ 𝑁)) |
46 | 45 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → (𝑃 Fn 𝑁 ∧ 𝐾 ∈ 𝑁)) |
47 | | fvco2 6273 |
. . . . . . . 8
⊢ ((𝑃 Fn 𝑁 ∧ 𝐾 ∈ 𝑁) → (((𝑆 Σg 𝑊) ∘ 𝑃)‘𝐾) = ((𝑆 Σg 𝑊)‘(𝑃‘𝐾))) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → (((𝑆 Σg 𝑊) ∘ 𝑃)‘𝐾) = ((𝑆 Σg 𝑊)‘(𝑃‘𝐾))) |
49 | | fveq2 6191 |
. . . . . . . . . 10
⊢ ((𝑃‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘(𝑃‘𝐾)) = ((𝑆 Σg 𝑊)‘𝐾)) |
50 | 49 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾) → ((𝑆 Σg 𝑊)‘(𝑃‘𝐾)) = ((𝑆 Σg 𝑊)‘𝐾)) |
51 | 50 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → ((𝑆 Σg 𝑊)‘(𝑃‘𝐾)) = ((𝑆 Σg 𝑊)‘𝐾)) |
52 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑊 ∈ Word 𝐵) |
53 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑃 ∈ 𝐵) |
54 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑖 ∈ (0..^(#‘𝑊))) |
55 | | ccats1val1 13403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 〈“𝑃”〉)‘𝑖) = (𝑊‘𝑖)) |
56 | 52, 53, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 〈“𝑃”〉)‘𝑖) = (𝑊‘𝑖)) |
57 | 56 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = ((𝑊‘𝑖)‘𝐾)) |
58 | 57 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ((𝑊‘𝑖)‘𝐾) = 𝐾)) |
59 | 58 | ralbidva 2985 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾)) |
60 | 59 | biimpd 219 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾)) |
61 | 60 | adantld 483 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁)) → (((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾) → ∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾)) |
62 | 61 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾) → ∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾)) |
63 | | simp3 1063 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) |
64 | 62, 63 | syld 47 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾) → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) |
65 | 64 | imp 445 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾) |
66 | 51, 65 | eqtrd 2656 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → ((𝑆 Σg 𝑊)‘(𝑃‘𝐾)) = 𝐾) |
67 | 38, 48, 66 | 3eqtrd 2660 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) ∧ ((𝑃‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾)) → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾) |
68 | 67 | exp32 631 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → ((𝑃‘𝐾) = 𝐾 → (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾))) |
69 | 26, 68 | sylbid 230 |
. . . 4
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → ((((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾 → (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾))) |
70 | 69 | com23 86 |
. . 3
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾))) |
71 | 70 | impd 447 |
. 2
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → ((∀𝑖 ∈ (0..^(#‘𝑊))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 ∧ (((𝑊 ++ 〈“𝑃”〉)‘(#‘𝑊))‘𝐾) = 𝐾) → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾)) |
72 | 16, 71 | sylbid 230 |
1
⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((#‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾)) |