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

Theorem wlkdlem4 26817
Description: Lemma 4 for wlkd 26818. (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 3212 . . 3 (∀𝑘 ∈ (0..^(♯‘𝐹))({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) ↔ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))))
4 df-ne 2944 . . . . . 6 ((𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ¬ (𝑃𝑘) = (𝑃‘(𝑘 + 1)))
5 ifpfal 1061 . . . . . 6 (¬ (𝑃𝑘) = (𝑃‘(𝑘 + 1)) → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
64, 5sylbi 207 . . . . 5 ((𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)) → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
76biimparc 465 . . . 4 (({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
87ralimi 3101 . . 3 (∀𝑘 ∈ (0..^(♯‘𝐹))({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
93, 8sylbir 225 . 2 ((∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
101, 2, 9syl2anc 573 1 (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  if-wif 1049   = wceq 1631  wcel 2145  wne 2943  wral 3061  Vcvv 3351  wss 3723  {csn 4317  {cpr 4319  cfv 6030  (class class class)co 6796  0cc0 10142  1c1 10143   + caddc 10145  ..^cfzo 12673  chash 13321  Word cword 13487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ifp 1050  df-ne 2944  df-ral 3066
This theorem is referenced by:  wlkd  26818
  Copyright terms: Public domain W3C validator