Step | Hyp | Ref
| Expression |
1 | | pmtrdifel.t |
. . . . 5
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) |
2 | | pmtrdifel.r |
. . . . 5
⊢ 𝑅 = ran (pmTrsp‘𝑁) |
3 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → (𝑤‘𝑗) = (𝑤‘𝑛)) |
4 | 3 | difeq1d 3689 |
. . . . . . . 8
⊢ (𝑗 = 𝑛 → ((𝑤‘𝑗) ∖ I ) = ((𝑤‘𝑛) ∖ I )) |
5 | 4 | dmeqd 5248 |
. . . . . . 7
⊢ (𝑗 = 𝑛 → dom ((𝑤‘𝑗) ∖ I ) = dom ((𝑤‘𝑛) ∖ I )) |
6 | 5 | fveq2d 6107 |
. . . . . 6
⊢ (𝑗 = 𝑛 → ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )) = ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑛) ∖ I ))) |
7 | 6 | cbvmptv 4678 |
. . . . 5
⊢ (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) = (𝑛 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑛) ∖ I ))) |
8 | 1, 2, 7 | pmtrdifwrdellem1 17724 |
. . . 4
⊢ (𝑤 ∈ Word 𝑇 → (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅) |
9 | 8 | adantl 481 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅) |
10 | 1, 2, 7 | pmtrdifwrdellem2 17725 |
. . . 4
⊢ (𝑤 ∈ Word 𝑇 → (#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
11 | 10 | adantl 481 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → (#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
12 | 1, 2, 7 | pmtrdifwrdel2lem1 17727 |
. . . . 5
⊢ ((𝑤 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(#‘𝑤))(((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾) |
13 | 12 | ancoms 468 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∀𝑖 ∈ (0..^(#‘𝑤))(((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾) |
14 | 1, 2, 7 | pmtrdifwrdellem3 17726 |
. . . . 5
⊢ (𝑤 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
15 | 14 | adantl 481 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
16 | | r19.26 3046 |
. . . 4
⊢
(∀𝑖 ∈
(0..^(#‘𝑤))((((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) ↔ (∀𝑖 ∈ (0..^(#‘𝑤))(((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
17 | 13, 15, 16 | sylanbrc 695 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∀𝑖 ∈ (0..^(#‘𝑤))((((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
18 | | fveq2 6103 |
. . . . . 6
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (#‘𝑢) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
19 | 18 | eqeq2d 2620 |
. . . . 5
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((#‘𝑤) = (#‘𝑢) ↔ (#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))))) |
20 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (𝑢‘𝑖) = ((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)) |
21 | 20 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((𝑢‘𝑖)‘𝐾) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾)) |
22 | 21 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((𝑢‘𝑖)‘𝐾) = 𝐾 ↔ (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾)) |
23 | 20 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((𝑢‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
24 | 23 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥) ↔ ((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
25 | 24 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥) ↔ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
26 | 22, 25 | anbi12d 743 |
. . . . . 6
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)) ↔ ((((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)))) |
27 | 26 | ralbidv 2969 |
. . . . 5
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (∀𝑖 ∈ (0..^(#‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)) ↔ ∀𝑖 ∈ (0..^(#‘𝑤))((((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)))) |
28 | 19, 27 | anbi12d 743 |
. . . 4
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥))) ↔ ((#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))((((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))))) |
29 | 28 | rspcev 3282 |
. . 3
⊢ (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅 ∧ ((#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))((((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)))) → ∃𝑢 ∈ Word 𝑅((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)))) |
30 | 9, 11, 17, 29 | syl12anc 1316 |
. 2
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∃𝑢 ∈ Word 𝑅((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)))) |
31 | 30 | ralrimiva 2949 |
1
⊢ (𝐾 ∈ 𝑁 → ∀𝑤 ∈ Word 𝑇∃𝑢 ∈ Word 𝑅((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)))) |