Metamath Proof Explorer

Theorem wlkiswwlks2lem5

Description: Lemma 5 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 wlkiswwlks2lem5 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E

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 2 uspgrf1oedg ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
4 2 rneqi ⊢ ran ⁡ E = ran ⁡ iEdg ⁡ G
5 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
6 4 5 eqtr4i ⊢ ran ⁡ E = Edg ⁡ G
7 6 a1i ⊢ G ∈ USHGraph → ran ⁡ E = Edg ⁡ G
8 7 f1oeq3d ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ↔ E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
9 3 8 mpbird ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
10 9 3ad2ant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
11 10 ad2antrr ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ x ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
12 simpr ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ x ∈ 0 ..^ P − 1 → x ∈ 0 ..^ P − 1
13 fveq2 ⊢ i = x → P ⁡ i = P ⁡ x
14 fvoveq1 ⊢ i = x → P ⁡ i + 1 = P ⁡ x + 1
15 13 14 preq12d ⊢ i = x → P ⁡ i P ⁡ i + 1 = P ⁡ x P ⁡ x + 1
16 15 eleq1d ⊢ i = x → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
17 16 adantl ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ x ∈ 0 ..^ P − 1 ∧ i = x → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ↔ P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
18 12 17 rspcdv ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ x ∈ 0 ..^ P − 1 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
19 18 impancom ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → x ∈ 0 ..^ P − 1 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
20 19 imp ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ x ∈ 0 ..^ P − 1 → P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E
21 f1ocnvdm ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ∧ P ⁡ x P ⁡ x + 1 ∈ ran ⁡ E → E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E
22 11 20 21 syl2anc ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E ∧ x ∈ 0 ..^ P − 1 → E -1 ⁡ P ⁡ x P ⁡ x + 1 ∈ dom ⁡ E
23 22 1 fmptd ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F : 0 ..^ P − 1 ⟶ dom ⁡ E
24 iswrdi ⊢ F : 0 ..^ P − 1 ⟶ dom ⁡ E → F ∈ Word dom ⁡ E
25 23 24 syl ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E
26 25 ex ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ∈ Word dom ⁡ E