Proof of Theorem pfxeq
| Step | Hyp | Ref
| Expression |
| 1 | | pfxcl 14715 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝑀) ∈ Word 𝑉) |
| 2 | | pfxcl 14715 |
. . . . 5
⊢ (𝑈 ∈ Word 𝑉 → (𝑈 prefix 𝑁) ∈ Word 𝑉) |
| 3 | | eqwrd 14595 |
. . . . 5
⊢ (((𝑊 prefix 𝑀) ∈ Word 𝑉 ∧ (𝑈 prefix 𝑁) ∈ Word 𝑉) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ ((♯‘(𝑊 prefix 𝑀)) = (♯‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
| 4 | 1, 2, 3 | syl2an 596 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ ((♯‘(𝑊 prefix 𝑀)) = (♯‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
| 5 | 4 | 3ad2ant2 1135 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ ((♯‘(𝑊 prefix 𝑀)) = (♯‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
| 6 | | simp2l 1200 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑊 ∈ Word 𝑉) |
| 7 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈
ℕ0) |
| 8 | | lencl 14571 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈
ℕ0) |
| 10 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)) → 𝑀 ≤ (♯‘𝑊)) |
| 11 | 7, 9, 10 | 3anim123i 1152 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0 ∧ 𝑀
≤ (♯‘𝑊))) |
| 12 | | elfz2nn0 13658 |
. . . . . . 7
⊢ (𝑀 ∈
(0...(♯‘𝑊))
↔ (𝑀 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ0 ∧ 𝑀 ≤ (♯‘𝑊))) |
| 13 | 11, 12 | sylibr 234 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ (0...(♯‘𝑊))) |
| 14 | | pfxlen 14721 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝑀)) = 𝑀) |
| 15 | 6, 13, 14 | syl2anc 584 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 prefix 𝑀)) = 𝑀) |
| 16 | | simp2r 1201 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑈 ∈ Word 𝑉) |
| 17 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
| 18 | | lencl 14571 |
. . . . . . . . 9
⊢ (𝑈 ∈ Word 𝑉 → (♯‘𝑈) ∈
ℕ0) |
| 19 | 18 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑈) ∈
ℕ0) |
| 20 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)) → 𝑁 ≤ (♯‘𝑈)) |
| 21 | 17, 19, 20 | 3anim123i 1152 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑁 ∈ ℕ0 ∧
(♯‘𝑈) ∈
ℕ0 ∧ 𝑁
≤ (♯‘𝑈))) |
| 22 | | elfz2nn0 13658 |
. . . . . . 7
⊢ (𝑁 ∈
(0...(♯‘𝑈))
↔ (𝑁 ∈
ℕ0 ∧ (♯‘𝑈) ∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝑈))) |
| 23 | 21, 22 | sylibr 234 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈ (0...(♯‘𝑈))) |
| 24 | | pfxlen 14721 |
. . . . . 6
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑈))) → (♯‘(𝑈 prefix 𝑁)) = 𝑁) |
| 25 | 16, 23, 24 | syl2anc 584 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑈 prefix 𝑁)) = 𝑁) |
| 26 | 15, 25 | eqeq12d 2753 |
. . . 4
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((♯‘(𝑊 prefix 𝑀)) = (♯‘(𝑈 prefix 𝑁)) ↔ 𝑀 = 𝑁)) |
| 27 | 26 | anbi1d 631 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (((♯‘(𝑊 prefix 𝑀)) = (♯‘(𝑈 prefix 𝑁)) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)))) |
| 28 | 15 | adantr 480 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (♯‘(𝑊 prefix 𝑀)) = 𝑀) |
| 29 | 28 | oveq2d 7447 |
. . . . . 6
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (0..^(♯‘(𝑊 prefix 𝑀))) = (0..^𝑀)) |
| 30 | 29 | raleqdv 3326 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖))) |
| 31 | 6 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ Word 𝑉) |
| 32 | 13 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ (0...(♯‘𝑊))) |
| 33 | | simpr 484 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀)) |
| 34 | | pfxfv 14720 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 prefix 𝑀)‘𝑖) = (𝑊‘𝑖)) |
| 35 | 31, 32, 33, 34 | syl3anc 1373 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑊 prefix 𝑀)‘𝑖) = (𝑊‘𝑖)) |
| 36 | 16 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑈 ∈ Word 𝑉) |
| 37 | 23 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑁 ∈ (0...(♯‘𝑈))) |
| 38 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁)) |
| 39 | 38 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑀 = 𝑁 → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
| 40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (𝑖 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑁))) |
| 41 | 40 | biimpa 476 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑁)) |
| 42 | | pfxfv 14720 |
. . . . . . . 8
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑈)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑈 prefix 𝑁)‘𝑖) = (𝑈‘𝑖)) |
| 43 | 36, 37, 41, 42 | syl3anc 1373 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑈 prefix 𝑁)‘𝑖) = (𝑈‘𝑖)) |
| 44 | 35, 43 | eqeq12d 2753 |
. . . . . 6
⊢
(((((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ (𝑊‘𝑖) = (𝑈‘𝑖))) |
| 45 | 44 | ralbidva 3176 |
. . . . 5
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^𝑀)((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
| 46 | 30, 45 | bitrd 279 |
. . . 4
⊢ ((((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 = 𝑁) → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖))) |
| 47 | 46 | pm5.32da 579 |
. . 3
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 𝑀)))((𝑊 prefix 𝑀)‘𝑖) = ((𝑈 prefix 𝑁)‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
| 48 | 5, 27, 47 | 3bitrd 305 |
. 2
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |
| 49 | 48 | 3com12 1124 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝑀 ≤
(♯‘𝑊) ∧
𝑁 ≤ (♯‘𝑈))) → ((𝑊 prefix 𝑀) = (𝑈 prefix 𝑁) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) |