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

Metamath Proof Explorer

Theorem 2wlklem

Description: Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018)

Ref Expression
Assertion 2wlklem ⊢ ∀ k ∈ 0 1 E ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ↔ E ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 1 ∧ E ⁡ F ⁡ 1 = P ⁡ 1 P ⁡ 2

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1ex ⊢ 1 ∈ V
3 2fveq3 ⊢ k = 0 → E ⁡ F ⁡ k = E ⁡ F ⁡ 0
4 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
5 fv0p1e1 ⊢ k = 0 → P ⁡ k + 1 = P ⁡ 1
6 4 5 preq12d ⊢ k = 0 → P ⁡ k P ⁡ k + 1 = P ⁡ 0 P ⁡ 1
7 3 6 eqeq12d ⊢ k = 0 → E ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ↔ E ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 1
8 2fveq3 ⊢ k = 1 → E ⁡ F ⁡ k = E ⁡ F ⁡ 1
9 fveq2 ⊢ k = 1 → P ⁡ k = P ⁡ 1
10 oveq1 ⊢ k = 1 → k + 1 = 1 + 1
11 1p1e2 ⊢ 1 + 1 = 2
12 10 11 eqtrdi ⊢ k = 1 → k + 1 = 2
13 12 fveq2d ⊢ k = 1 → P ⁡ k + 1 = P ⁡ 2
14 9 13 preq12d ⊢ k = 1 → P ⁡ k P ⁡ k + 1 = P ⁡ 1 P ⁡ 2
15 8 14 eqeq12d ⊢ k = 1 → E ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ↔ E ⁡ F ⁡ 1 = P ⁡ 1 P ⁡ 2
16 1 2 7 15 ralpr ⊢ ∀ k ∈ 0 1 E ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ↔ E ⁡ F ⁡ 0 = P ⁡ 0 P ⁡ 1 ∧ E ⁡ F ⁡ 1 = P ⁡ 1 P ⁡ 2