Step |
Hyp |
Ref |
Expression |
1 |
|
gsmsymgrfix.s |
⊢ 𝑆 = ( SymGrp ‘ 𝑁 ) |
2 |
|
gsmsymgrfix.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
3 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝐵 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
4 |
|
elnn0uz |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) ) |
5 |
3 4
|
sylib |
⊢ ( 𝑊 ∈ Word 𝐵 → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) ) |
7 |
6
|
3ad2ant1 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) ) |
8 |
|
fzosplitsn |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ) |
9 |
7 8
|
syl |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ) |
10 |
9
|
raleqdv |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) |
11 |
3
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
12 |
11
|
3ad2ant1 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
13 |
|
fveq2 |
⊢ ( 𝑖 = ( ♯ ‘ 𝑊 ) → ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) = ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ) |
14 |
13
|
fveq1d |
⊢ ( 𝑖 = ( ♯ ‘ 𝑊 ) → ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) ) |
15 |
14
|
eqeq1d |
⊢ ( 𝑖 = ( ♯ ‘ 𝑊 ) → ( ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) |
16 |
15
|
ralunsn |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) ) |
17 |
12 16
|
syl |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∪ { ( ♯ ‘ 𝑊 ) } ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) ) |
18 |
10 17
|
bitrd |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) ) ) |
19 |
|
eqidd |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) |
20 |
|
ccats1val2 |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) = 𝑃 ) |
21 |
20
|
fveq1d |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = ( 𝑃 ‘ 𝐾 ) ) |
22 |
21
|
eqeq1d |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) → ( ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ↔ ( 𝑃 ‘ 𝐾 ) = 𝐾 ) ) |
23 |
19 22
|
mpd3an3 |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ↔ ( 𝑃 ‘ 𝐾 ) = 𝐾 ) ) |
24 |
23
|
3ad2ant1 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ↔ ( 𝑃 ‘ 𝐾 ) = 𝐾 ) ) |
25 |
|
simprl |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → 𝑁 ∈ Fin ) |
26 |
|
simpll |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → 𝑊 ∈ Word 𝐵 ) |
27 |
|
simplr |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → 𝑃 ∈ 𝐵 ) |
28 |
1 2
|
gsumccatsymgsn |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) = ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ) |
29 |
28
|
fveq1d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) ) |
30 |
25 26 27 29
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) ) |
31 |
30
|
3adant3 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) ) |
32 |
31
|
adantr |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) ) |
33 |
1 2
|
symgbasf |
⊢ ( 𝑃 ∈ 𝐵 → 𝑃 : 𝑁 ⟶ 𝑁 ) |
34 |
33
|
ffnd |
⊢ ( 𝑃 ∈ 𝐵 → 𝑃 Fn 𝑁 ) |
35 |
34
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) → 𝑃 Fn 𝑁 ) |
36 |
|
simpr |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → 𝐾 ∈ 𝑁 ) |
37 |
|
fvco2 |
⊢ ( ( 𝑃 Fn 𝑁 ∧ 𝐾 ∈ 𝑁 ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) ) |
38 |
35 36 37
|
syl2an |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) ) |
39 |
38
|
3adant3 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) ) |
40 |
39
|
adantr |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑆 Σg 𝑊 ) ∘ 𝑃 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) ) |
41 |
|
fveq2 |
⊢ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) ) |
42 |
41
|
ad2antrl |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) ) |
43 |
|
ccats1val1 |
⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
44 |
43
|
ad4ant14 |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
45 |
44
|
fveq1d |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) ) |
46 |
45
|
eqeq1d |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) |
47 |
46
|
ralbidva |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) |
48 |
47
|
biimpd |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) |
49 |
48
|
adantld |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) |
50 |
49
|
3adant3 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) |
51 |
|
simp3 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) |
52 |
50 51
|
syld |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) |
53 |
52
|
imp |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) |
54 |
42 53
|
eqtrd |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg 𝑊 ) ‘ ( 𝑃 ‘ 𝐾 ) ) = 𝐾 ) |
55 |
32 40 54
|
3eqtrd |
⊢ ( ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ∧ ( ( 𝑃 ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = 𝐾 ) |
56 |
55
|
exp32 |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑃 ‘ 𝐾 ) = 𝐾 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = 𝐾 ) ) ) |
57 |
24 56
|
sylbid |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = 𝐾 ) ) ) |
58 |
57
|
impcomd |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ ( ♯ ‘ 𝑊 ) ) ‘ 𝐾 ) = 𝐾 ) → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = 𝐾 ) ) |
59 |
18 58
|
sylbid |
⊢ ( ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) ( ( ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑊 ++ 〈“ 𝑃 ”〉 ) ) ‘ 𝐾 ) = 𝐾 ) ) |