This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkdlem4

Description: Lemma 4 for wlkd . (Contributed by Alexander van der Vekens, 1-Feb-2018) (Revised by AV, 23-Jan-2021)

Ref Expression
Hypotheses wlkd.p ⊢ φ → P ∈ Word V
wlkd.f ⊢ φ → F ∈ Word V
wlkd.l ⊢ φ → P = F + 1
wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
wlkd.n ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
Assertion wlkdlem4 ⊢ φ → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 wlkd.p ⊢ φ → P ∈ Word V
2 wlkd.f ⊢ φ → F ∈ Word V
3 wlkd.l ⊢ φ → P = F + 1
4 wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
5 wlkd.n ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
6 r19.26 ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ P ⁡ k ≠ P ⁡ k + 1 ↔ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
7 df-ne ⊢ P ⁡ k ≠ P ⁡ k + 1 ↔ ¬ P ⁡ k = P ⁡ k + 1
8 ifpfal ⊢ ¬ P ⁡ k = P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
9 7 8 sylbi ⊢ P ⁡ k ≠ P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
10 9 biimparc ⊢ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ P ⁡ k ≠ P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
11 10 ralimi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ P ⁡ k ≠ P ⁡ k + 1 → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
12 6 11 sylbir ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
13 4 5 12 syl2anc ⊢ φ → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k