Step | Hyp | Ref
| Expression |
1 | | elrabi 3328 |
. . . . 5
⊢ (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → 𝑄 ∈ 𝑃) |
2 | | eqid 2610 |
. . . . . 6
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
3 | | psgnfix.p |
. . . . . 6
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
4 | 2, 3 | symgbasf 17627 |
. . . . 5
⊢ (𝑄 ∈ 𝑃 → 𝑄:𝑁⟶𝑁) |
5 | | ffn 5958 |
. . . . 5
⊢ (𝑄:𝑁⟶𝑁 → 𝑄 Fn 𝑁) |
6 | 1, 4, 5 | 3syl 18 |
. . . 4
⊢ (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → 𝑄 Fn 𝑁) |
7 | 6 | ad3antlr 763 |
. . 3
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝑄 Fn 𝑁) |
8 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → 𝑁 ∈ Fin) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → 𝑁 ∈ Fin) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) → 𝑁 ∈ Fin) |
11 | | simp1 1054 |
. . . . . 6
⊢ ((𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑈 ∈ Word 𝑅) |
12 | 10, 11 | anim12i 588 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑁 ∈ Fin ∧ 𝑈 ∈ Word 𝑅)) |
13 | | psgnfix.z |
. . . . . 6
⊢ 𝑍 = (SymGrp‘𝑁) |
14 | 13 | eqcomi 2619 |
. . . . . . . 8
⊢
(SymGrp‘𝑁) =
𝑍 |
15 | 14 | fveq2i 6106 |
. . . . . . 7
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘𝑍) |
16 | 3, 15 | eqtri 2632 |
. . . . . 6
⊢ 𝑃 = (Base‘𝑍) |
17 | | psgnfix.r |
. . . . . 6
⊢ 𝑅 = ran (pmTrsp‘𝑁) |
18 | 13, 16, 17 | gsmtrcl 17759 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑈 ∈ Word 𝑅) → (𝑍 Σg 𝑈) ∈ 𝑃) |
19 | 12, 18 | syl 17 |
. . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑍 Σg 𝑈) ∈ 𝑃) |
20 | 2, 3 | symgbasf 17627 |
. . . 4
⊢ ((𝑍 Σg
𝑈) ∈ 𝑃 → (𝑍 Σg 𝑈):𝑁⟶𝑁) |
21 | | ffn 5958 |
. . . 4
⊢ ((𝑍 Σg
𝑈):𝑁⟶𝑁 → (𝑍 Σg 𝑈) Fn 𝑁) |
22 | 19, 20, 21 | 3syl 18 |
. . 3
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑍 Σg 𝑈) Fn 𝑁) |
23 | 8 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝑁 ∈ Fin) |
24 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → 𝐾 ∈ 𝑁) |
25 | 24 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝐾 ∈ 𝑁) |
26 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑍) =
(Base‘𝑍) |
27 | 17, 13, 26 | symgtrf 17712 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 ⊆ (Base‘𝑍) |
28 | | sswrd 13168 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ⊆ (Base‘𝑍) → Word 𝑅 ⊆ Word (Base‘𝑍)) |
29 | 28 | sseld 3567 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ⊆ (Base‘𝑍) → (𝑈 ∈ Word 𝑅 → 𝑈 ∈ Word (Base‘𝑍))) |
30 | 27, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ Word 𝑅 → 𝑈 ∈ Word (Base‘𝑍)) |
31 | 30 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑈 ∈ Word (Base‘𝑍)) |
32 | 31 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝑈 ∈ Word (Base‘𝑍)) |
33 | 23, 25, 32 | 3jca 1235 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑈 ∈ Word (Base‘𝑍))) |
34 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) → ((𝑈‘𝑖)‘𝐾) = 𝐾) |
35 | 34 | ralimi 2936 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) → ∀𝑖 ∈ (0..^(#‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾) |
36 | 35 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → ∀𝑖 ∈ (0..^(#‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾) |
37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → ∀𝑖 ∈ (0..^(#‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾) |
38 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑈) =
(#‘𝑊) →
(0..^(#‘𝑈)) =
(0..^(#‘𝑊))) |
39 | 38 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) =
(#‘𝑈) →
(0..^(#‘𝑈)) =
(0..^(#‘𝑊))) |
40 | 39 | raleqdv 3121 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) =
(#‘𝑈) →
(∀𝑖 ∈
(0..^(#‘𝑈))((𝑈‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)) |
41 | 40 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → (∀𝑖 ∈ (0..^(#‘𝑈))((𝑈‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (∀𝑖 ∈ (0..^(#‘𝑈))((𝑈‘𝑖)‘𝐾) = 𝐾 ↔ ∀𝑖 ∈ (0..^(#‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)) |
43 | 37, 42 | mpbird 246 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → ∀𝑖 ∈ (0..^(#‘𝑈))((𝑈‘𝑖)‘𝐾) = 𝐾) |
44 | 13, 26 | gsmsymgrfix 17671 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑈 ∈ Word (Base‘𝑍)) → (∀𝑖 ∈ (0..^(#‘𝑈))((𝑈‘𝑖)‘𝐾) = 𝐾 → ((𝑍 Σg 𝑈)‘𝐾) = 𝐾)) |
45 | 33, 43, 44 | sylc 63 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → ((𝑍 Σg 𝑈)‘𝐾) = 𝐾) |
46 | 45 | eqcomd 2616 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝐾 = ((𝑍 Σg 𝑈)‘𝐾)) |
47 | 46 | adantr 480 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 = 𝐾) → 𝐾 = ((𝑍 Σg 𝑈)‘𝐾)) |
48 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑄‘𝑘) = (𝑄‘𝐾)) |
49 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑄 → (𝑞‘𝐾) = (𝑄‘𝐾)) |
50 | 49 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑄 → ((𝑞‘𝐾) = 𝐾 ↔ (𝑄‘𝐾) = 𝐾)) |
51 | 50 | elrab 3331 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↔ (𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐾)) |
52 | 51 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → (𝑄‘𝐾) = 𝐾) |
53 | 52 | ad3antlr 763 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑄‘𝐾) = 𝐾) |
54 | 48, 53 | sylan9eqr 2666 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 = 𝐾) → (𝑄‘𝑘) = 𝐾) |
55 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((𝑍 Σg 𝑈)‘𝑘) = ((𝑍 Σg 𝑈)‘𝐾)) |
56 | 55 | adantl 481 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 = 𝐾) → ((𝑍 Σg 𝑈)‘𝑘) = ((𝑍 Σg 𝑈)‘𝐾)) |
57 | 54, 56 | eqeq12d 2625 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 = 𝐾) → ((𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘) ↔ 𝐾 = ((𝑍 Σg 𝑈)‘𝐾))) |
58 | 47, 57 | mpbird 246 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 = 𝐾) → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘)) |
59 | 58 | ex 449 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑘 = 𝐾 → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘))) |
60 | 59 | adantr 480 |
. . . . 5
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → (𝑘 = 𝐾 → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘))) |
61 | 60 | com12 32 |
. . . 4
⊢ (𝑘 = 𝐾 → ((((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘))) |
62 | | fveq1 6102 |
. . . . . . . . 9
⊢ ((𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = ((𝑆 Σg 𝑊)‘𝑘)) |
63 | 62 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = ((𝑆 Σg 𝑊)‘𝑘)) |
64 | 63 | ad3antlr 763 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = ((𝑆 Σg 𝑊)‘𝑘)) |
65 | 64 | adantl 481 |
. . . . . 6
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = ((𝑆 Σg 𝑊)‘𝑘)) |
66 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
67 | | df-ne 2782 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ≠ 𝐾 ↔ ¬ 𝑘 = 𝐾) |
68 | 67 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ (¬
𝑘 = 𝐾 → 𝑘 ≠ 𝐾) |
69 | 66, 68 | anim12i 588 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ ¬ 𝑘 = 𝐾) → (𝑘 ∈ 𝑁 ∧ 𝑘 ≠ 𝐾)) |
70 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑁 ∖ {𝐾}) ↔ (𝑘 ∈ 𝑁 ∧ 𝑘 ≠ 𝐾)) |
71 | 69, 70 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑁 ∖ {𝐾})) |
72 | | fvres 6117 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑁 ∖ {𝐾}) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = (𝑄‘𝑘)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑘 ∈ 𝑁) ∧ ¬ 𝑘 = 𝐾) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = (𝑄‘𝑘)) |
74 | 73 | exp31 628 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑘 ∈ 𝑁 → (¬ 𝑘 = 𝐾 → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = (𝑄‘𝑘)))) |
75 | 74 | ad3antrrr 762 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑘 ∈ 𝑁 → (¬ 𝑘 = 𝐾 → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = (𝑄‘𝑘)))) |
76 | 75 | imp 444 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → (¬ 𝑘 = 𝐾 → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = (𝑄‘𝑘))) |
77 | 76 | impcom 445 |
. . . . . 6
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → ((𝑄 ↾ (𝑁 ∖ {𝐾}))‘𝑘) = (𝑄‘𝑘)) |
78 | 68 | anim2i 591 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ 𝑁 ∧ ¬ 𝑘 = 𝐾) → (𝑘 ∈ 𝑁 ∧ 𝑘 ≠ 𝐾)) |
79 | 78, 70 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑁 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑁 ∖ {𝐾})) |
80 | 79 | ex 449 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑁 → (¬ 𝑘 = 𝐾 → 𝑘 ∈ (𝑁 ∖ {𝐾}))) |
81 | 80 | adantl 481 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → (¬ 𝑘 = 𝐾 → 𝑘 ∈ (𝑁 ∖ {𝐾}))) |
82 | 81 | impcom 445 |
. . . . . . 7
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → 𝑘 ∈ (𝑁 ∖ {𝐾})) |
83 | | diffi 8077 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝐾}) ∈ Fin) |
84 | 83 | ancri 573 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ Fin → ((𝑁 ∖ {𝐾}) ∈ Fin ∧ 𝑁 ∈ Fin)) |
85 | 84 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → ((𝑁 ∖ {𝐾}) ∈ Fin ∧ 𝑁 ∈ Fin)) |
86 | 85 | ad3antrrr 762 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → ((𝑁 ∖ {𝐾}) ∈ Fin ∧ 𝑁 ∈ Fin)) |
87 | | psgnfix.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) |
88 | | psgnfix.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) |
89 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑆) =
(Base‘𝑆) |
90 | 87, 88, 89 | symgtrf 17712 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ⊆ (Base‘𝑆) |
91 | | sswrd 13168 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ⊆ (Base‘𝑆) → Word 𝑇 ⊆ Word (Base‘𝑆)) |
92 | 91 | sseld 3567 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ⊆ (Base‘𝑆) → (𝑊 ∈ Word 𝑇 → 𝑊 ∈ Word (Base‘𝑆))) |
93 | 90, 92 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑇 → 𝑊 ∈ Word (Base‘𝑆)) |
94 | 93 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) → 𝑊 ∈ Word (Base‘𝑆)) |
95 | 94 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝑊 ∈ Word (Base‘𝑆)) |
96 | | simpr2 1061 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (#‘𝑊) = (#‘𝑈)) |
97 | 95, 32, 96 | 3jca 1235 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (𝑊 ∈ Word (Base‘𝑆) ∧ 𝑈 ∈ Word (Base‘𝑍) ∧ (#‘𝑊) = (#‘𝑈))) |
98 | 86, 97 | jca 553 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → (((𝑁 ∖ {𝐾}) ∈ Fin ∧ 𝑁 ∈ Fin) ∧ (𝑊 ∈ Word (Base‘𝑆) ∧ 𝑈 ∈ Word (Base‘𝑍) ∧ (#‘𝑊) = (#‘𝑈)))) |
99 | 98 | ad2antrl 760 |
. . . . . . . 8
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → (((𝑁 ∖ {𝐾}) ∈ Fin ∧ 𝑁 ∈ Fin) ∧ (𝑊 ∈ Word (Base‘𝑆) ∧ 𝑈 ∈ Word (Base‘𝑍) ∧ (#‘𝑊) = (#‘𝑈)))) |
100 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) → ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) |
101 | 100 | ralimi 2936 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
(0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) → ∀𝑖 ∈ (0..^(#‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) |
102 | 101 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → ∀𝑖 ∈ (0..^(#‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) |
103 | 102 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → ∀𝑖 ∈ (0..^(#‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) |
104 | 103 | ad2antrl 760 |
. . . . . . . 8
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → ∀𝑖 ∈ (0..^(#‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) |
105 | | incom 3767 |
. . . . . . . . . . 11
⊢ ((𝑁 ∖ {𝐾}) ∩ 𝑁) = (𝑁 ∩ (𝑁 ∖ {𝐾})) |
106 | | indif 3828 |
. . . . . . . . . . 11
⊢ (𝑁 ∩ (𝑁 ∖ {𝐾})) = (𝑁 ∖ {𝐾}) |
107 | 105, 106 | eqtri 2632 |
. . . . . . . . . 10
⊢ ((𝑁 ∖ {𝐾}) ∩ 𝑁) = (𝑁 ∖ {𝐾}) |
108 | 107 | eqcomi 2619 |
. . . . . . . . 9
⊢ (𝑁 ∖ {𝐾}) = ((𝑁 ∖ {𝐾}) ∩ 𝑁) |
109 | 88, 89, 13, 26, 108 | gsmsymgreq 17675 |
. . . . . . . 8
⊢ ((((𝑁 ∖ {𝐾}) ∈ Fin ∧ 𝑁 ∈ Fin) ∧ (𝑊 ∈ Word (Base‘𝑆) ∧ 𝑈 ∈ Word (Base‘𝑍) ∧ (#‘𝑊) = (#‘𝑈))) → (∀𝑖 ∈ (0..^(#‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛) → ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑆 Σg 𝑊)‘𝑛) = ((𝑍 Σg 𝑈)‘𝑛))) |
110 | 99, 104, 109 | sylc 63 |
. . . . . . 7
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑆 Σg 𝑊)‘𝑛) = ((𝑍 Σg 𝑈)‘𝑛)) |
111 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝑆 Σg 𝑊)‘𝑛) = ((𝑆 Σg 𝑊)‘𝑘)) |
112 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝑍 Σg 𝑈)‘𝑛) = ((𝑍 Σg 𝑈)‘𝑘)) |
113 | 111, 112 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (((𝑆 Σg 𝑊)‘𝑛) = ((𝑍 Σg 𝑈)‘𝑛) ↔ ((𝑆 Σg 𝑊)‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘))) |
114 | 113 | rspcva 3280 |
. . . . . . 7
⊢ ((𝑘 ∈ (𝑁 ∖ {𝐾}) ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑆 Σg 𝑊)‘𝑛) = ((𝑍 Σg 𝑈)‘𝑛)) → ((𝑆 Σg 𝑊)‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘)) |
115 | 82, 110, 114 | syl2anc 691 |
. . . . . 6
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → ((𝑆 Σg 𝑊)‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘)) |
116 | 65, 77, 115 | 3eqtr3d 2652 |
. . . . 5
⊢ ((¬
𝑘 = 𝐾 ∧ (((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁)) → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘)) |
117 | 116 | ex 449 |
. . . 4
⊢ (¬
𝑘 = 𝐾 → ((((((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘))) |
118 | 61, 117 | pm2.61i 175 |
. . 3
⊢
((((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) ∧ 𝑘 ∈ 𝑁) → (𝑄‘𝑘) = ((𝑍 Σg 𝑈)‘𝑘)) |
119 | 7, 22, 118 | eqfnfvd 6222 |
. 2
⊢
(((((𝑁 ∈ Fin
∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ∧ (𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊))) ∧ (𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)))) → 𝑄 = (𝑍 Σg 𝑈)) |
120 | 119 | exp31 628 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (#‘𝑊) = (#‘𝑈) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈)))) |