| Step | Hyp | Ref
| Expression |
|---|
| 1 | | pmtrdifel.t |
. . . . 5
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) |
| 2 | | pmtrdifel.r |
. . . . 5
⊢ 𝑅 = ran (pmTrsp‘𝑁) |
| 3 | | fveq2 6834 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → (𝑤‘𝑗) = (𝑤‘𝑛)) |
| 4 | 3 | difeq1d 4077 |
. . . . . . . 8
⊢ (𝑗 = 𝑛 → ((𝑤‘𝑗) ∖ I ) = ((𝑤‘𝑛) ∖ I )) |
| 5 | 4 | dmeqd 5854 |
. . . . . . 7
⊢ (𝑗 = 𝑛 → dom ((𝑤‘𝑗) ∖ I ) = dom ((𝑤‘𝑛) ∖ I )) |
| 6 | 5 | fveq2d 6838 |
. . . . . 6
⊢ (𝑗 = 𝑛 → ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )) = ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑛) ∖ I ))) |
| 7 | 6 | cbvmptv 5202 |
. . . . 5
⊢ (𝑗 ∈
(0..^(♯‘𝑤))
↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) = (𝑛 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑛) ∖ I ))) |
| 8 | 1, 2, 7 | pmtrdifwrdellem1 19410 |
. . . 4
⊢ (𝑤 ∈ Word 𝑇 → (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅) |
| 9 | 8 | adantl 481 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) ∈ Word 𝑅) |
| 10 | 1, 2, 7 | pmtrdifwrdellem2 19411 |
. . . 4
⊢ (𝑤 ∈ Word 𝑇 → (♯‘𝑤) = (♯‘(𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
| 11 | 10 | adantl 481 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → (♯‘𝑤) = (♯‘(𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
| 12 | 1, 2, 7 | pmtrdifwrdel2lem1 19413 |
. . . . 5
⊢ ((𝑤 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑤))(((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾) |
| 13 | 12 | ancoms 458 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∀𝑖 ∈ (0..^(♯‘𝑤))(((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾) |
| 14 | 1, 2, 7 | pmtrdifwrdellem3 19412 |
. . . . 5
⊢ (𝑤 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
| 15 | 14 | adantl 481 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∀𝑖 ∈ (0..^(♯‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
| 16 | | r19.26 3096 |
. . . 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 583 |
. . 3
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∀𝑖 ∈ (0..^(♯‘𝑤))((((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
| 18 | | fveq2 6834 |
. . . . . 6
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (♯‘𝑢) = (♯‘(𝑗 ∈
(0..^(♯‘𝑤))
↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))))) |
| 19 | 18 | eqeq2d 2747 |
. . . . 5
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((♯‘𝑤) = (♯‘𝑢) ↔ (♯‘𝑤) = (♯‘(𝑗 ∈
(0..^(♯‘𝑤))
↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))))) |
| 20 | | fveq1 6833 |
. . . . . . . . 9
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (𝑢‘𝑖) = ((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)) |
| 21 | 20 | fveq1d 6836 |
. . . . . . . 8
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((𝑢‘𝑖)‘𝐾) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾)) |
| 22 | 21 | eqeq1d 2738 |
. . . . . . 7
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((𝑢‘𝑖)‘𝐾) = 𝐾 ↔ (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾)) |
| 23 | 20 | fveq1d 6836 |
. . . . . . . . 9
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((𝑢‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)) |
| 24 | 23 | eqeq2d 2747 |
. . . . . . . 8
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥) ↔ ((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
| 25 | 24 | ralbidv 3159 |
. . . . . . 7
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥) ↔ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))) |
| 26 | 22, 25 | anbi12d 632 |
. . . . . 6
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → ((((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)) ↔ ((((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)))) |
| 27 | 26 | ralbidv 3159 |
. . . . 5
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (∀𝑖 ∈
(0..^(♯‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑤))((((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥)))) |
| 28 | 19, 27 | anbi12d 632 |
. . . 4
⊢ (𝑢 = (𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I ))) → (((♯‘𝑤) = (♯‘𝑢) ∧ ∀𝑖 ∈
(0..^(♯‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥))) ↔ ((♯‘𝑤) = (♯‘(𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))) ∧ ∀𝑖 ∈
(0..^(♯‘𝑤))((((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = (((𝑗 ∈ (0..^(♯‘𝑤)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑤‘𝑗) ∖ I )))‘𝑖)‘𝑥))))) |
| 29 | 28 | rspcev 3576 |
. . 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 836 |
. 2
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇) → ∃𝑢 ∈ Word 𝑅((♯‘𝑤) = (♯‘𝑢) ∧ ∀𝑖 ∈ (0..^(♯‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)))) |
| 31 | 30 | ralrimiva 3128 |
1
⊢ (𝐾 ∈ 𝑁 → ∀𝑤 ∈ Word 𝑇∃𝑢 ∈ Word 𝑅((♯‘𝑤) = (♯‘𝑢) ∧ ∀𝑖 ∈ (0..^(♯‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥)))) |
