MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  erclwwlkntr Structured version   Visualization version   GIF version

Theorem erclwwlkntr 26121
Description: is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
Hypotheses
Ref Expression
erclwwlkn.w 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁)
erclwwlkn.r = {⟨𝑡, 𝑢⟩ ∣ (𝑡𝑊𝑢𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}
Assertion
Ref Expression
erclwwlkntr ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧)
Distinct variable groups:   𝑡,𝐸,𝑢   𝑡,𝑁,𝑢   𝑛,𝑉,𝑡,𝑢   𝑡,𝑊,𝑢   𝑥,𝑛,𝑡,𝑢   𝑛,𝑁   𝑦,𝑛,𝑡,𝑢,𝑥   𝑛,𝑊   𝑧,𝑛,𝑡,𝑢,𝑦,𝑥
Allowed substitution hints:   (𝑥,𝑦,𝑧,𝑢,𝑡,𝑛)   𝐸(𝑥,𝑦,𝑧,𝑛)   𝑁(𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem erclwwlkntr
Dummy variables 𝑚 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3175 . 2 𝑥 ∈ V
2 vex 3175 . 2 𝑦 ∈ V
3 vex 3175 . 2 𝑧 ∈ V
4 erclwwlkn.w . . . . . 6 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁)
5 erclwwlkn.r . . . . . 6 = {⟨𝑡, 𝑢⟩ ∣ (𝑡𝑊𝑢𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}
64, 5erclwwlkneqlen 26118 . . . . 5 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 𝑦 → (#‘𝑥) = (#‘𝑦)))
763adant3 1073 . . . 4 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑦 → (#‘𝑥) = (#‘𝑦)))
84, 5erclwwlkneqlen 26118 . . . . . . 7 ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 𝑧 → (#‘𝑦) = (#‘𝑧)))
983adant1 1071 . . . . . 6 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 𝑧 → (#‘𝑦) = (#‘𝑧)))
104, 5erclwwlkneq 26117 . . . . . . . 8 ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 𝑧 ↔ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))))
11103adant1 1071 . . . . . . 7 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 𝑧 ↔ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))))
124, 5erclwwlkneq 26117 . . . . . . . . . 10 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 𝑦 ↔ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))))
13123adant3 1073 . . . . . . . . 9 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑦 ↔ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))))
14 simpr1 1059 . . . . . . . . . . . . . . 15 (((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → 𝑥𝑊)
15 simplr2 1096 . . . . . . . . . . . . . . 15 (((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → 𝑧𝑊)
16 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑦 cyclShift 𝑛) = (𝑦 cyclShift 𝑚))
1716eqeq2d 2619 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → (𝑥 = (𝑦 cyclShift 𝑛) ↔ 𝑥 = (𝑦 cyclShift 𝑚)))
1817cbvrexv 3147 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑚))
19 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑘 → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift 𝑘))
2019eqeq2d 2619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑘 → (𝑦 = (𝑧 cyclShift 𝑛) ↔ 𝑦 = (𝑧 cyclShift 𝑘)))
2120cbvrexv 3147 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) ↔ ∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘))
22 clwwlknprop 26066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑧 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑧 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑧) = 𝑁)))
23 eqcom 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((#‘𝑧) = 𝑁𝑁 = (#‘𝑧))
2423biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((#‘𝑧) = 𝑁𝑁 = (#‘𝑧))
2524adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑁 ∈ ℕ0 ∧ (#‘𝑧) = 𝑁) → 𝑁 = (#‘𝑧))
26253ad2ant3 1076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑧 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑧) = 𝑁)) → 𝑁 = (#‘𝑧))
2722, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑧 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → 𝑁 = (#‘𝑧))
2827, 4eleq2s 2705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑧𝑊𝑁 = (#‘𝑧))
2928adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) → 𝑁 = (#‘𝑧))
3029adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → 𝑁 = (#‘𝑧))
3122simp2d 1066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → 𝑧 ∈ Word 𝑉)
3231, 4eleq2s 2705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑧𝑊𝑧 ∈ Word 𝑉)
3332adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) → 𝑧 ∈ Word 𝑉)
3433adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → 𝑧 ∈ Word 𝑉)
3534adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → 𝑧 ∈ Word 𝑉)
36 simprr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))
3735, 36cshwcsh2id 13371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
38 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑁 = (#‘𝑧) → (0...𝑁) = (0...(#‘𝑧)))
39 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((#‘𝑧) = (#‘𝑦) → (0...(#‘𝑧)) = (0...(#‘𝑦)))
4039eqcoms 2617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((#‘𝑦) = (#‘𝑧) → (0...(#‘𝑧)) = (0...(#‘𝑦)))
4140adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (0...(#‘𝑧)) = (0...(#‘𝑦)))
4241adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (0...(#‘𝑧)) = (0...(#‘𝑦)))
4338, 42sylan9eq 2663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (0...𝑁) = (0...(#‘𝑦)))
4443eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (𝑚 ∈ (0...𝑁) ↔ 𝑚 ∈ (0...(#‘𝑦))))
4544anbi1d 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → ((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ↔ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚))))
4638eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑁 = (#‘𝑧) → (𝑘 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...(#‘𝑧))))
4746anbi1d 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑁 = (#‘𝑧) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) ↔ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))))
4847adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) ↔ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))))
4945, 48anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) ↔ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)))))
5038rexeqdv 3121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑁 = (#‘𝑧) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
5150adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
5237, 49, 513imtr4d 281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑁 = (#‘𝑧) ∧ (((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)))) → (((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))
5330, 52mpancom 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))
5453expdcom 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ (0...𝑁) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
5554ancoms 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑘 ∈ (0...𝑁) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
5655expdcom 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))
5756com4t 90 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 = (𝑦 cyclShift 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))
5857ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑦 cyclShift 𝑚) → (𝑚 ∈ (0...𝑁) → ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))))
5958com13 85 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (𝑚 ∈ (0...𝑁) → (𝑥 = (𝑦 cyclShift 𝑚) → (𝑘 ∈ (0...𝑁) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))))
6059imp41 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))
6160rexlimdva 3012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))
6261ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
6362rexlimdva 3012 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
6421, 63syl7bi 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑚 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
6518, 64syl5bi 230 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑥𝑊𝑦𝑊) ∧ 𝑧𝑊) ∧ ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
6665exp31 627 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑊𝑦𝑊) → (𝑧𝑊 → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))))
6766com15 98 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛) → (𝑧𝑊 → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥𝑊𝑦𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))))
6867impcom 444 . . . . . . . . . . . . . . . . . . . 20 ((𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥𝑊𝑦𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))
69683adant1 1071 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥𝑊𝑦𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))))
7069impcom 444 . . . . . . . . . . . . . . . . . 18 ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥𝑊𝑦𝑊) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
7170com13 85 . . . . . . . . . . . . . . . . 17 ((𝑥𝑊𝑦𝑊) → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
72713impia 1252 . . . . . . . . . . . . . . . 16 ((𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))
7372impcom 444 . . . . . . . . . . . . . . 15 (((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))
7414, 15, 733jca 1234 . . . . . . . . . . . . . 14 (((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → (𝑥𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛)))
754, 5erclwwlkneq 26117 . . . . . . . . . . . . . . 15 ((𝑥 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑧 ↔ (𝑥𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
76753adant2 1072 . . . . . . . . . . . . . 14 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑧 ↔ (𝑥𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑧 cyclShift 𝑛))))
7774, 76syl5ibrcom 235 . . . . . . . . . . . . 13 (((((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) ∧ (𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛))) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 𝑧))
7877exp31 627 . . . . . . . . . . . 12 (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → ((𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 𝑧))))
7978com24 92 . . . . . . . . . . 11 (((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 𝑧))))
8079ex 448 . . . . . . . . . 10 ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 𝑧)))))
8180com4t 90 . . . . . . . . 9 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥𝑊𝑦𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑦 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 𝑧)))))
8213, 81sylbid 228 . . . . . . . 8 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑦 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 𝑧)))))
8382com25 96 . . . . . . 7 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑦𝑊𝑧𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑧 cyclShift 𝑛)) → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 𝑦𝑥 𝑧)))))
8411, 83sylbid 228 . . . . . 6 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 𝑧 → ((#‘𝑦) = (#‘𝑧) → ((#‘𝑥) = (#‘𝑦) → (𝑥 𝑦𝑥 𝑧)))))
859, 84mpdd 41 . . . . 5 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 𝑧 → ((#‘𝑥) = (#‘𝑦) → (𝑥 𝑦𝑥 𝑧))))
8685com24 92 . . . 4 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑦 → ((#‘𝑥) = (#‘𝑦) → (𝑦 𝑧𝑥 𝑧))))
877, 86mpdd 41 . . 3 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 𝑦 → (𝑦 𝑧𝑥 𝑧)))
8887impd 445 . 2 ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧))
891, 2, 3, 88mp3an 1415 1 ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wrex 2896  Vcvv 3172   class class class wbr 4577  {copab 4636  cfv 5790  (class class class)co 6527  0cc0 9792  0cn0 11139  ...cfz 12152  #chash 12934  Word cword 13092   cyclShift ccsh 13331   ClWWalksN cclwwlkn 26043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-hash 12935  df-word 13100  df-concat 13102  df-substr 13104  df-csh 13332  df-clwwlk 26045  df-clwwlkn 26046
This theorem is referenced by:  erclwwlkn  26122
  Copyright terms: Public domain W3C validator