Proof of Theorem repswsymballbi
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
⊢ (𝑊 = ∅ → (#‘𝑊) =
(#‘∅)) |
2 | | hash0 13158 |
. . . . 5
⊢
(#‘∅) = 0 |
3 | 1, 2 | syl6eq 2672 |
. . . 4
⊢ (𝑊 = ∅ → (#‘𝑊) = 0) |
4 | | fvex 6201 |
. . . . . . . 8
⊢ (𝑊‘0) ∈
V |
5 | | repsw0 13524 |
. . . . . . . 8
⊢ ((𝑊‘0) ∈ V →
((𝑊‘0) repeatS 0) =
∅) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑊‘0) repeatS 0) =
∅ |
7 | 6 | eqcomi 2631 |
. . . . . 6
⊢ ∅ =
((𝑊‘0) repeatS
0) |
8 | | simpr 477 |
. . . . . 6
⊢
(((#‘𝑊) = 0
∧ 𝑊 = ∅) →
𝑊 =
∅) |
9 | | oveq2 6658 |
. . . . . . 7
⊢
((#‘𝑊) = 0
→ ((𝑊‘0) repeatS
(#‘𝑊)) = ((𝑊‘0) repeatS
0)) |
10 | 9 | adantr 481 |
. . . . . 6
⊢
(((#‘𝑊) = 0
∧ 𝑊 = ∅) →
((𝑊‘0) repeatS
(#‘𝑊)) = ((𝑊‘0) repeatS
0)) |
11 | 7, 8, 10 | 3eqtr4a 2682 |
. . . . 5
⊢
(((#‘𝑊) = 0
∧ 𝑊 = ∅) →
𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) |
12 | | ral0 4076 |
. . . . . . 7
⊢
∀𝑖 ∈
∅ (𝑊‘𝑖) = (𝑊‘0) |
13 | | oveq2 6658 |
. . . . . . . . 9
⊢
((#‘𝑊) = 0
→ (0..^(#‘𝑊)) =
(0..^0)) |
14 | | fzo0 12492 |
. . . . . . . . 9
⊢ (0..^0) =
∅ |
15 | 13, 14 | syl6eq 2672 |
. . . . . . . 8
⊢
((#‘𝑊) = 0
→ (0..^(#‘𝑊)) =
∅) |
16 | 15 | raleqdv 3144 |
. . . . . . 7
⊢
((#‘𝑊) = 0
→ (∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑊‘0))) |
17 | 12, 16 | mpbiri 248 |
. . . . . 6
⊢
((#‘𝑊) = 0
→ ∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
18 | 17 | adantr 481 |
. . . . 5
⊢
(((#‘𝑊) = 0
∧ 𝑊 = ∅) →
∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
19 | 11, 18 | 2thd 255 |
. . . 4
⊢
(((#‘𝑊) = 0
∧ 𝑊 = ∅) →
(𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
20 | 3, 19 | mpancom 703 |
. . 3
⊢ (𝑊 = ∅ → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
21 | 20 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
22 | | df-3an 1039 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
23 | 22 | a1i 11 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
24 | | fstwrdne 13344 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉) |
25 | 24 | ancoms 469 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊‘0) ∈ 𝑉) |
26 | | lencl 13324 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
27 | 26 | adantl 482 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (#‘𝑊) ∈
ℕ0) |
28 | | repsdf2 13525 |
. . . . 5
⊢ (((𝑊‘0) ∈ 𝑉 ∧ (#‘𝑊) ∈ ℕ0)
→ (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
29 | 25, 27, 28 | syl2anc 693 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
30 | | simpr 477 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
31 | | eqidd 2623 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (#‘𝑊) = (#‘𝑊)) |
32 | 30, 31 | jca 554 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊))) |
33 | 32 | biantrurd 529 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (#‘𝑊)) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
34 | 23, 29, 33 | 3bitr4d 300 |
. . 3
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉) → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
35 | 34 | ex 450 |
. 2
⊢ (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
36 | 21, 35 | pm2.61ine 2877 |
1
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |