Proof of Theorem repswsymballbi
| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . 5
⊢ (𝑊 = ∅ →
(♯‘𝑊) =
(♯‘∅)) |
| 2 | | hash0 14406 |
. . . . 5
⊢
(♯‘∅) = 0 |
| 3 | 1, 2 | eqtrdi 2793 |
. . . 4
⊢ (𝑊 = ∅ →
(♯‘𝑊) =
0) |
| 4 | | fvex 6919 |
. . . . . . . 8
⊢ (𝑊‘0) ∈
V |
| 5 | | repsw0 14815 |
. . . . . . . 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 484 |
. . . . . 6
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ 𝑊 =
∅) |
| 9 | | oveq2 7439 |
. . . . . . 7
⊢
((♯‘𝑊) =
0 → ((𝑊‘0)
repeatS (♯‘𝑊))
= ((𝑊‘0) repeatS
0)) |
| 10 | 9 | adantr 480 |
. . . . . 6
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ ((𝑊‘0) repeatS
(♯‘𝑊)) =
((𝑊‘0) repeatS
0)) |
| 11 | 7, 8, 10 | 3eqtr4a 2803 |
. . . . 5
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ 𝑊 = ((𝑊‘0) repeatS
(♯‘𝑊))) |
| 12 | | ral0 4513 |
. . . . . . 7
⊢
∀𝑖 ∈
∅ (𝑊‘𝑖) = (𝑊‘0) |
| 13 | | oveq2 7439 |
. . . . . . . . 9
⊢
((♯‘𝑊) =
0 → (0..^(♯‘𝑊)) = (0..^0)) |
| 14 | | fzo0 13723 |
. . . . . . . . 9
⊢ (0..^0) =
∅ |
| 15 | 13, 14 | eqtrdi 2793 |
. . . . . . . 8
⊢
((♯‘𝑊) =
0 → (0..^(♯‘𝑊)) = ∅) |
| 16 | 15 | raleqdv 3326 |
. . . . . . 7
⊢
((♯‘𝑊) =
0 → (∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑊‘0))) |
| 17 | 12, 16 | mpbiri 258 |
. . . . . 6
⊢
((♯‘𝑊) =
0 → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 18 | 17 | adantr 480 |
. . . . 5
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 19 | 11, 18 | 2thd 265 |
. . . 4
⊢
(((♯‘𝑊)
= 0 ∧ 𝑊 = ∅)
→ (𝑊 = ((𝑊‘0) repeatS
(♯‘𝑊)) ↔
∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 20 | 3, 19 | mpancom 688 |
. . 3
⊢ (𝑊 = ∅ → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 21 | 20 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 22 | | df-3an 1089 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 23 | 22 | a1i 11 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 24 | | fstwrdne 14593 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉) |
| 25 | 24 | ancoms 458 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘0) ∈ 𝑉) |
| 26 | | lencl 14571 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
| 27 | 26 | adantl 481 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (♯‘𝑊) ∈
ℕ0) |
| 28 | | repsdf2 14816 |
. . . . 5
⊢ (((𝑊‘0) ∈ 𝑉 ∧ (♯‘𝑊) ∈ ℕ0)
→ (𝑊 = ((𝑊‘0) repeatS
(♯‘𝑊)) ↔
(𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 29 | 25, 27, 28 | syl2anc 584 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 30 | | simpr 484 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
| 31 | | eqidd 2738 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (♯‘𝑊) = (♯‘𝑊)) |
| 32 | 30, 31 | jca 511 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊))) |
| 33 | 32 | biantrurd 532 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 34 | 23, 29, 33 | 3bitr4d 311 |
. . 3
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 35 | 34 | ex 412 |
. 2
⊢ (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 36 | 21, 35 | pm2.61ine 3025 |
1
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |