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

Theorem wlkdlem4 28580
Description: Lemma 4 for wlkd 28581. (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 3114 . . 3 (∀𝑘 ∈ (0..^(♯‘𝐹))({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) ↔ (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))))
4 df-ne 2944 . . . . . 6 ((𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ ¬ (𝑃𝑘) = (𝑃‘(𝑘 + 1)))
5 ifpfal 1075 . . . . . 6 (¬ (𝑃𝑘) = (𝑃‘(𝑘 + 1)) → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
64, 5sylbi 216 . . . . 5 ((𝑃𝑘) ≠ (𝑃‘(𝑘 + 1)) → (if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))) ↔ {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
76biimparc 480 . . . 4 (({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘)) ∧ (𝑃𝑘) ≠ (𝑃‘(𝑘 + 1))) → if-((𝑃𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹𝑘)) = {(𝑃𝑘)}, {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹𝑘))))
87ralimi 3086 . . 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 1061   = wceq 1541  wcel 2106  wne 2943  wral 3064  Vcvv 3445  wss 3910  {csn 4586  {cpr 4588  cfv 6496  (class class class)co 7356  0cc0 11050  1c1 11051   + caddc 11053  ..^cfzo 13566  chash 14229  Word cword 14401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ifp 1062  df-ne 2944  df-ral 3065
This theorem is referenced by:  wlkd  28581
  Copyright terms: Public domain W3C validator