Proof of Theorem erclwwlkneqlen
Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . 3
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) |
2 | | erclwwlkn.r |
. . 3
⊢ ∼ =
{〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} |
3 | 1, 2 | erclwwlkneq 26351 |
. 2
⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 ↔ (𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛)))) |
4 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑇 = (𝑈 cyclShift 𝑛) → (#‘𝑇) = (#‘(𝑈 cyclShift 𝑛))) |
5 | | clwwlknprop 26300 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁))) |
6 | 5, 1 | eleq2s 2706 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ 𝑊 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁))) |
7 | | simpl2 1058 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁)) ∧ 𝑛 ∈ (0...𝑁)) → 𝑈 ∈ Word 𝑉) |
8 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = (#‘𝑈) → (0...𝑁) = (0...(#‘𝑈))) |
9 | 8 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑈) → (𝑛 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...(#‘𝑈)))) |
10 | 9 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑈) = 𝑁 → (𝑛 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...(#‘𝑈)))) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑈) = 𝑁) → (𝑛 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...(#‘𝑈)))) |
12 | 11 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁)) → (𝑛 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...(#‘𝑈)))) |
13 | 12 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁)) ∧ 𝑛 ∈ (0...𝑁)) → 𝑛 ∈ (0...(#‘𝑈))) |
14 | 7, 13 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁)) ∧ 𝑛 ∈ (0...𝑁)) → (𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...(#‘𝑈)))) |
15 | 14 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑈 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑈) = 𝑁)) → (𝑛 ∈ (0...𝑁) → (𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...(#‘𝑈))))) |
16 | 6, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑊 → (𝑛 ∈ (0...𝑁) → (𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...(#‘𝑈))))) |
17 | 16 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) ∧ (𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌)) → (𝑛 ∈ (0...𝑁) → (𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...(#‘𝑈))))) |
18 | 17 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) ∧ (𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌)) ∧ 𝑛 ∈ (0...𝑁)) → (𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...(#‘𝑈)))) |
19 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (0...(#‘𝑈)) → 𝑛 ∈ ℤ) |
20 | | cshwlen 13396 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ ℤ) → (#‘(𝑈 cyclShift 𝑛)) = (#‘𝑈)) |
21 | 19, 20 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...(#‘𝑈))) → (#‘(𝑈 cyclShift 𝑛)) = (#‘𝑈)) |
22 | 18, 21 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) ∧ (𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌)) ∧ 𝑛 ∈ (0...𝑁)) → (#‘(𝑈 cyclShift 𝑛)) = (#‘𝑈)) |
23 | 4, 22 | sylan9eqr 2666 |
. . . . . . . 8
⊢
(((((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) ∧ (𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌)) ∧ 𝑛 ∈ (0...𝑁)) ∧ 𝑇 = (𝑈 cyclShift 𝑛)) → (#‘𝑇) = (#‘𝑈)) |
24 | 23 | ex 449 |
. . . . . . 7
⊢ ((((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) ∧ (𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌)) ∧ 𝑛 ∈ (0...𝑁)) → (𝑇 = (𝑈 cyclShift 𝑛) → (#‘𝑇) = (#‘𝑈))) |
25 | 24 | rexlimdva 3013 |
. . . . . 6
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) ∧ (𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌)) → (∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛) → (#‘𝑇) = (#‘𝑈))) |
26 | 25 | ex 449 |
. . . . 5
⊢ ((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) → ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛) → (#‘𝑇) = (#‘𝑈)))) |
27 | 26 | com23 84 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊) → (∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛) → ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (#‘𝑇) = (#‘𝑈)))) |
28 | 27 | 3impia 1253 |
. . 3
⊢ ((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛)) → ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (#‘𝑇) = (#‘𝑈))) |
29 | 28 | com12 32 |
. 2
⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → ((𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛)) → (#‘𝑇) = (#‘𝑈))) |
30 | 3, 29 | sylbid 229 |
1
⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 → (#‘𝑇) = (#‘𝑈))) |