Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
2 | | hasheq0 13154 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ V → ((#‘𝑤) = 0 ↔ 𝑤 = ∅)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢
((#‘𝑤) = 0
↔ 𝑤 =
∅) |
4 | 3 | biimpri 218 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (#‘𝑤) = 0) |
5 | 4 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑤 = ∅ →
(0..^(#‘𝑤)) =
(0..^0)) |
6 | | fzo0 12492 |
. . . . . . . 8
⊢ (0..^0) =
∅ |
7 | 5, 6 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑤 = ∅ →
(0..^(#‘𝑤)) =
∅) |
8 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤‘𝑖) = (∅‘𝑖)) |
9 | 8 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑤 = ∅ → ((𝑤‘𝑖)‘𝐾) = ((∅‘𝑖)‘𝐾)) |
10 | 9 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑤 = ∅ → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ((∅‘𝑖)‘𝐾) = 𝐾)) |
11 | 7, 10 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑤 = ∅ → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾)) |
12 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑆 Σg
𝑤) = (𝑆 Σg
∅)) |
13 | 12 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑤 = ∅ → ((𝑆 Σg
𝑤)‘𝐾) = ((𝑆 Σg
∅)‘𝐾)) |
14 | 13 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = ∅ → (((𝑆 Σg
𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg
∅)‘𝐾) = 𝐾)) |
15 | 11, 14 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = ∅ →
((∀𝑖 ∈
(0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg
∅)‘𝐾) = 𝐾))) |
16 | 15 | imbi2d 330 |
. . . 4
⊢ (𝑤 = ∅ → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg
∅)‘𝐾) = 𝐾)))) |
17 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (#‘𝑤) = (#‘𝑦)) |
18 | 17 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (0..^(#‘𝑤)) = (0..^(#‘𝑦))) |
19 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤‘𝑖) = (𝑦‘𝑖)) |
20 | 19 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤‘𝑖)‘𝐾) = ((𝑦‘𝑖)‘𝐾)) |
21 | 20 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ((𝑦‘𝑖)‘𝐾) = 𝐾)) |
22 | 18, 21 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾)) |
23 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝑆 Σg 𝑤) = (𝑆 Σg 𝑦)) |
24 | 23 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((𝑆 Σg 𝑤)‘𝐾) = ((𝑆 Σg 𝑦)‘𝐾)) |
25 | 24 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (((𝑆 Σg 𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)) |
26 | 22, 25 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) |
27 | 26 | imbi2d 330 |
. . . 4
⊢ (𝑤 = 𝑦 → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)))) |
28 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (#‘𝑤) = (#‘(𝑦 ++ 〈“𝑧”〉))) |
29 | 28 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (0..^(#‘𝑤)) = (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))) |
30 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (𝑤‘𝑖) = ((𝑦 ++ 〈“𝑧”〉)‘𝑖)) |
31 | 30 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → ((𝑤‘𝑖)‘𝐾) = (((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾)) |
32 | 31 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ (((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) |
33 | 29, 32 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) |
34 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (𝑆 Σg 𝑤) = (𝑆 Σg (𝑦 ++ 〈“𝑧”〉))) |
35 | 34 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → ((𝑆 Σg 𝑤)‘𝐾) = ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾)) |
36 | 35 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (((𝑆 Σg 𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) |
37 | 33, 36 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → ((∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾))) |
38 | 37 | imbi2d 330 |
. . . 4
⊢ (𝑤 = (𝑦 ++ 〈“𝑧”〉) → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)))) |
39 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (#‘𝑤) = (#‘𝑊)) |
40 | 39 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (0..^(#‘𝑤)) = (0..^(#‘𝑊))) |
41 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑤‘𝑖) = (𝑊‘𝑖)) |
42 | 41 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑤‘𝑖)‘𝐾) = ((𝑊‘𝑖)‘𝐾)) |
43 | 42 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ((𝑊‘𝑖)‘𝐾) = 𝐾)) |
44 | 40, 43 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾)) |
45 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑆 Σg 𝑤) = (𝑆 Σg 𝑊)) |
46 | 45 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((𝑆 Σg 𝑤)‘𝐾) = ((𝑆 Σg 𝑊)‘𝐾)) |
47 | 46 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((𝑆 Σg 𝑤)‘𝐾) = 𝐾 ↔ ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) |
48 | 44, 47 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾) ↔ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾))) |
49 | 48 | imbi2d 330 |
. . . 4
⊢ (𝑤 = 𝑊 → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑤))((𝑤‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑤)‘𝐾) = 𝐾)) ↔ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)))) |
50 | | gsmsymgrfix.s |
. . . . . . . . . 10
⊢ 𝑆 = (SymGrp‘𝑁) |
51 | 50 | symgid 17821 |
. . . . . . . . 9
⊢ (𝑁 ∈ Fin → ( I ↾
𝑁) =
(0g‘𝑆)) |
52 | 51 | adantr 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ( I ↾ 𝑁) = (0g‘𝑆)) |
53 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝑆) = (0g‘𝑆) |
54 | 53 | gsum0 17278 |
. . . . . . . 8
⊢ (𝑆 Σg
∅) = (0g‘𝑆) |
55 | 52, 54 | syl6reqr 2675 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑆 Σg ∅) = ( I
↾ 𝑁)) |
56 | 55 | fveq1d 6193 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((𝑆 Σg
∅)‘𝐾) = (( I
↾ 𝑁)‘𝐾)) |
57 | | fvresi 6439 |
. . . . . . 7
⊢ (𝐾 ∈ 𝑁 → (( I ↾ 𝑁)‘𝐾) = 𝐾) |
58 | 57 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (( I ↾ 𝑁)‘𝐾) = 𝐾) |
59 | 56, 58 | eqtrd 2656 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((𝑆 Σg
∅)‘𝐾) = 𝐾) |
60 | 59 | a1d 25 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ ∅ ((∅‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg
∅)‘𝐾) = 𝐾)) |
61 | | ccatws1len 13398 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (#‘(𝑦 ++ 〈“𝑧”〉)) = ((#‘𝑦) + 1)) |
62 | 61 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (0..^(#‘(𝑦 ++ 〈“𝑧”〉))) = (0..^((#‘𝑦) + 1))) |
63 | 62 | raleqdv 3144 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^((#‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) |
64 | 63 | adantr 481 |
. . . . . . 7
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) → (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^((#‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾)) |
65 | | gsmsymgrfix.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
66 | 50, 65 | gsmsymgrfixlem1 17847 |
. . . . . . . 8
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((#‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) |
67 | 66 | 3expb 1266 |
. . . . . . 7
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) → (∀𝑖 ∈ (0..^((#‘𝑦) + 1))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) |
68 | 64, 67 | sylbid 230 |
. . . . . 6
⊢ (((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾))) → (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)) |
69 | 68 | exp32 631 |
. . . . 5
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾) → (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)))) |
70 | 69 | a2d 29 |
. . . 4
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑦))((𝑦‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑦)‘𝐾) = 𝐾)) → ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘(𝑦 ++ 〈“𝑧”〉)))(((𝑦 ++ 〈“𝑧”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑦 ++ 〈“𝑧”〉))‘𝐾) = 𝐾)))) |
71 | 16, 27, 38, 49, 60, 70 | wrdind 13476 |
. . 3
⊢ (𝑊 ∈ Word 𝐵 → ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾))) |
72 | 71 | com12 32 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑊 ∈ Word 𝐵 → (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾))) |
73 | 72 | 3impia 1261 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑊 ∈ Word 𝐵) → (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) |