Proof of Theorem repsdf2
Step | Hyp | Ref
| Expression |
1 | | repsconst 13370 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = ((0..^𝑁) × {𝑆})) |
2 | 1 | eqeq2d 2620 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ 𝑊 = ((0..^𝑁) × {𝑆}))) |
3 | | fconst2g 6373 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝑊:(0..^𝑁)⟶{𝑆} ↔ 𝑊 = ((0..^𝑁) × {𝑆}))) |
4 | 3 | adantr 480 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} ↔ 𝑊 = ((0..^𝑁) × {𝑆}))) |
5 | | fconstfv 6381 |
. . . . . . . . 9
⊢ (𝑊:(0..^𝑁)⟶{𝑆} ↔ (𝑊 Fn (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆)) |
6 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → 𝑊:(0..^𝑁)⟶{𝑆}) |
7 | | snssi 4280 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ 𝑉 → {𝑆} ⊆ 𝑉) |
8 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑆} ⊆ 𝑉) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → {𝑆} ⊆ 𝑉) |
10 | 6, 9 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → (𝑊:(0..^𝑁)⟶{𝑆} ∧ {𝑆} ⊆ 𝑉)) |
11 | | fss 5969 |
. . . . . . . . . . . 12
⊢ ((𝑊:(0..^𝑁)⟶{𝑆} ∧ {𝑆} ⊆ 𝑉) → 𝑊:(0..^𝑁)⟶𝑉) |
12 | | iswrdi 13164 |
. . . . . . . . . . . 12
⊢ (𝑊:(0..^𝑁)⟶𝑉 → 𝑊 ∈ Word 𝑉) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → 𝑊 ∈ Word 𝑉) |
14 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑊:(0..^𝑁)⟶{𝑆} → 𝑊 Fn (0..^𝑁)) |
15 | | ffzo0hash 13090 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 Fn (0..^𝑁)) → (#‘𝑊) = 𝑁) |
16 | 15 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 Fn (0..^𝑁) → (𝑁 ∈ ℕ0 →
(#‘𝑊) = 𝑁)) |
17 | 14, 16 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑊:(0..^𝑁)⟶{𝑆} → (𝑁 ∈ ℕ0 →
(#‘𝑊) = 𝑁)) |
18 | 17 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑊:(0..^𝑁)⟶{𝑆} → (#‘𝑊) = 𝑁)) |
19 | 18 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} → (#‘𝑊) = 𝑁)) |
20 | 19 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → (#‘𝑊) = 𝑁) |
21 | 13, 20 | jca 553 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) |
22 | 21 | ex 449 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁))) |
23 | 5, 22 | syl5bir 232 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 Fn (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁))) |
24 | 23 | expcomd 453 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^𝑁)(𝑊‘𝑖) = 𝑆 → (𝑊 Fn (0..^𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)))) |
25 | 24 | imp 444 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → (𝑊 Fn (0..^𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁))) |
26 | | wrdf 13165 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → 𝑊:(0..^(#‘𝑊))⟶𝑉) |
27 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑊:(0..^(#‘𝑊))⟶𝑉 → 𝑊 Fn (0..^(#‘𝑊))) |
28 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) = 𝑁 → (0..^(#‘𝑊)) = (0..^𝑁)) |
29 | 28 | fneq2d 5896 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) = 𝑁 → (𝑊 Fn (0..^(#‘𝑊)) ↔ 𝑊 Fn (0..^𝑁))) |
30 | 29 | biimpd 218 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) = 𝑁 → (𝑊 Fn (0..^(#‘𝑊)) → 𝑊 Fn (0..^𝑁))) |
31 | 30 | a1d 25 |
. . . . . . . . . . 11
⊢
((#‘𝑊) = 𝑁 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 Fn (0..^(#‘𝑊)) → 𝑊 Fn (0..^𝑁)))) |
32 | 31 | com13 86 |
. . . . . . . . . 10
⊢ (𝑊 Fn (0..^(#‘𝑊)) → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘𝑊) = 𝑁 → 𝑊 Fn (0..^𝑁)))) |
33 | 26, 27, 32 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘𝑊) = 𝑁 → 𝑊 Fn (0..^𝑁)))) |
34 | 33 | com12 32 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word 𝑉 → ((#‘𝑊) = 𝑁 → 𝑊 Fn (0..^𝑁)))) |
35 | 34 | impd 446 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) → 𝑊 Fn (0..^𝑁))) |
36 | 35 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) → 𝑊 Fn (0..^𝑁))) |
37 | 25, 36 | impbid 201 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → (𝑊 Fn (0..^𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁))) |
38 | 37 | ex 449 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^𝑁)(𝑊‘𝑖) = 𝑆 → (𝑊 Fn (0..^𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)))) |
39 | 38 | pm5.32rd 670 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 Fn (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) |
40 | | df-3an 1033 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆)) |
41 | 39, 5, 40 | 3bitr4g 302 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) |
42 | 2, 4, 41 | 3bitr2d 295 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) |