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

Theorem wlkdlem4 28341
Description: Lemma 4 for wlkd 28342. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.)
Hypotheses
Ref Expression
wlkd.p (𝜑𝑃 ∈ Word V)
wlkd.f (𝜑𝐹 ∈ Word V)
wlkd.l (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))
wlkd.e (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))
wlkd.n (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)))
Assertion
Ref Expression
wlkdlem4 (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
Distinct variable groups:   𝑘,𝐹   𝑃,𝑘   𝑘,𝐼   𝜑,𝑘

Proof of Theorem wlkdlem4
StepHypRef Expression
1 wlkd.e . 2 (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)))
2 wlkd.n . 2 (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)))
3 r19.26 3110 . . 3 (∀𝑘 ∈ (0..^(♯‘𝐹))({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) ↔ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))))
4 df-ne 2941 . . . . . 6 ((𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ¬ (𝑃𝑘) = (𝑃‘(𝑘 + 1)))
5 ifpfal 1074 . . . . . 6 (¬ (𝑃𝑘) = (𝑃‘(𝑘 + 1)) → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
64, 5sylbi 216 . . . . 5 ((𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)) → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
76biimparc 480 . . . 4 (({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
87ralimi 3082 . . 3 (∀𝑘 ∈ (0..^(♯‘𝐹))({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
93, 8sylbir 234 . 2 ((∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
101, 2, 9syl2anc 584 1 (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  if-wif 1060   = wceq 1540  wcel 2105  wne 2940  wral 3061  Vcvv 3441  wss 3898  {csn 4573  {cpr 4575  cfv 6479  (class class class)co 7337  0cc0 10972  1c1 10973   + caddc 10975  ..^cfzo 13483  chash 14145  Word cword 14317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ifp 1061  df-ne 2941  df-ral 3062
This theorem is referenced by:  wlkd  28342
  Copyright terms: Public domain W3C validator