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

Metamath Proof Explorer

Theorem wlkiswwlks2lem6

Description: Lemma 6 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Hypotheses wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
wlkiswwlks2lem.e ⊢ E = iEdg ⁡ G
Assertion wlkiswwlks2lem6 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
2 wlkiswwlks2lem.e ⊢ E = iEdg ⁡ G
3 1 2 wlkiswwlks2lem5 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E
4 3 imp ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E
5 1 wlkiswwlks2lem3 ⊢ P ∈ Word V ∧ 1 ≤ P → P : 0 … F ⟶ V
6 5 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → P : 0 … F ⟶ V
7 6 adantr ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → P : 0 … F ⟶ V
8 1 2 wlkiswwlks2lem4 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
9 8 imp ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
10 4 7 9 3jca ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
11 10 ex ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E ∧ P : 0 … F ⟶ V ∧ ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1