Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . 5
⊢ (𝑊 = ∅ →
(♯‘𝑊) =
(♯‘∅)) |
2 | | hash0 14274 |
. . . . 5
⊢
(♯‘∅) = 0 |
3 | 1, 2 | eqtrdi 2793 |
. . . 4
⊢ (𝑊 = ∅ →
(♯‘𝑊) =
0) |
4 | | fvex 6860 |
. . . . . . . 8
⊢ (𝑊‘0) ∈
V |
5 | | repsw0 14672 |
. . . . . . . 8
⊢ ((𝑊‘0) ∈ V →
((𝑊‘0) repeatS 0) =
∅) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑊‘0) repeatS 0) =
∅ |
7 | 6 | eqcomi 2746 |
. . . . . 6
⊢ ∅ =
((𝑊‘0) repeatS
0) |
8 | | simpr 486 |
. . . . . 6
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ 𝑊 =
∅) |
9 | | oveq2 7370 |
. . . . . . 7
⊢
((♯‘𝑊) =
0 → ((𝑊‘0)
repeatS (♯‘𝑊))
= ((𝑊‘0) repeatS
0)) |
10 | 9 | adantr 482 |
. . . . . 6
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ ((𝑊‘0) repeatS
(♯‘𝑊)) =
((𝑊‘0) repeatS
0)) |
11 | 7, 8, 10 | 3eqtr4a 2803 |
. . . . 5
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ 𝑊 = ((𝑊‘0) repeatS
(♯‘𝑊))) |
12 | | ral0 4475 |
. . . . . . 7
⊢
∀𝑖 ∈
∅ (𝑊‘𝑖) = (𝑊‘0) |
13 | | oveq2 7370 |
. . . . . . . . 9
⊢
((♯‘𝑊) =
0 → (0..^(♯‘𝑊)) = (0..^0)) |
14 | | fzo0 13603 |
. . . . . . . . 9
⊢ (0..^0) =
∅ |
15 | 13, 14 | eqtrdi 2793 |
. . . . . . . 8
⊢
((♯‘𝑊) =
0 → (0..^(♯‘𝑊)) = ∅) |
16 | 15 | raleqdv 3316 |
. . . . . . 7
⊢
((♯‘𝑊) =
0 → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑊‘0))) |
17 | 12, 16 | mpbiri 258 |
. . . . . 6
⊢
((♯‘𝑊) =
0 → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
18 | 17 | adantr 482 |
. . . . 5
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
19 | 11, 18 | 2thd 265 |
. . . 4
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ (𝑊 = ((𝑊‘0) repeatS
(♯‘𝑊)) ↔
∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
20 | 3, 19 | mpancom 687 |
. . 3
⊢ (𝑊 = ∅ → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
21 | 20 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
22 | | df-3an 1090 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
23 | 22 | a1i 11 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
24 | | fstwrdne 14450 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉) |
25 | 24 | ancoms 460 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘0) ∈ 𝑉) |
26 | | lencl 14428 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
27 | 26 | adantl 483 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (♯‘𝑊) ∈
ℕ0) |
28 | | repsdf2 14673 |
. . . . 5
⊢ (((𝑊‘0) ∈ 𝑉 ∧ (♯‘𝑊) ∈ ℕ0)
→ (𝑊 = ((𝑊‘0) repeatS
(♯‘𝑊)) ↔
(𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
29 | 25, 27, 28 | syl2anc 585 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
30 | | simpr 486 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
31 | | eqidd 2738 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (♯‘𝑊) = (♯‘𝑊)) |
32 | 30, 31 | jca 513 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊))) |
33 | 32 | biantrurd 534 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
34 | 23, 29, 33 | 3bitr4d 311 |
. . 3
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
35 | 34 | ex 414 |
. 2
⊢ (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
36 | 21, 35 | pm2.61ine 3029 |
1
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |