Step | Hyp | Ref
| Expression |
1 | | pmtrdifel.t |
. . . 4
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) |
2 | | pmtrdifel.r |
. . . 4
⊢ 𝑅 = ran (pmTrsp‘𝑁) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑗 = 𝑛 → (𝑤‘𝑗) = (𝑤‘𝑛)) |
4 | 3 | difeq1d 3689 |
. . . . . . 7
⊢ (𝑗 = 𝑛 → ((𝑤‘𝑗) ∖ I ) = ((𝑤‘𝑛) ∖ I )) |
5 | 4 | dmeqd 5248 |
. . . . . 6
⊢ (𝑗 = 𝑛 → dom ((𝑤‘𝑗) ∖ I ) = dom ((𝑤‘𝑛) ∖ I )) |
6 | 5 | fveq2d 6107 |
. . . . 5
⊢ (𝑗 = 𝑛 → ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )) = ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑛) ∖ I ))) |
7 | 6 | cbvmptv 4678 |
. . . 4
⊢ (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) = (𝑛 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑛) ∖ I ))) |
8 | 1, 2, 7 | pmtrdifwrdellem1 17724 |
. . 3
⊢ (𝑤 ∈ Word 𝑇 → (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅) |
9 | 1, 2, 7 | pmtrdifwrdellem2 17725 |
. . 3
⊢ (𝑤 ∈ Word 𝑇 → (#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
10 | 1, 2, 7 | pmtrdifwrdellem3 17726 |
. . 3
⊢ (𝑤 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
11 | | fveq2 6103 |
. . . . . 6
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (#‘𝑢) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
12 | 11 | eqeq2d 2620 |
. . . . 5
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((#‘𝑤) = (#‘𝑢) ↔ (#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))))) |
13 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (𝑢‘𝑖) = ((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)) |
14 | 13 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((𝑢‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
15 | 14 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥) ↔ ((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
16 | 15 | 2ralbidv 2972 |
. . . . 5
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥) ↔ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
17 | 12, 16 | anbi12d 743 |
. . . 4
⊢ (𝑢 = (𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)) ↔ ((#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)))) |
18 | 17 | rspcev 3282 |
. . 3
⊢ (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅 ∧ ((#‘𝑤) = (#‘(𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(#‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) → ∃𝑢 ∈ Word 𝑅((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥))) |
19 | 8, 9, 10, 18 | syl12anc 1316 |
. 2
⊢ (𝑤 ∈ Word 𝑇 → ∃𝑢 ∈ Word 𝑅((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥))) |
20 | 19 | rgen 2906 |
1
⊢
∀𝑤 ∈
Word 𝑇∃𝑢 ∈ Word 𝑅((#‘𝑤) = (#‘𝑢) ∧ ∀𝑖 ∈ (0..^(#‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)) |