Metamath Proof Explorer

Theorem wlkiswwlks2lem4

Description: Lemma 4 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-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 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

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 wlkiswwlks2lem1 ⊢ P ∈ Word V ∧ 1 ≤ P → F = P − 1
4 3 3adant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → F = P − 1
5 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
6 5 3ad2ant2 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → P ∈ ℕ 0
7 1 wlkiswwlks2lem2 ⊢ P ∈ ℕ 0 ∧ i ∈ 0 ..^ P − 1 → F ⁡ i = E -1 ⁡ P ⁡ i P ⁡ i + 1
8 6 7 sylan ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 → F ⁡ i = E -1 ⁡ P ⁡ i P ⁡ i + 1
9 8 adantr ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 ∧ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → F ⁡ i = E -1 ⁡ P ⁡ i P ⁡ i + 1
10 9 fveq2d ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 ∧ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ F ⁡ i = E ⁡ E -1 ⁡ P ⁡ i P ⁡ i + 1
11 2 uspgrf1oedg ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
12 2 rneqi ⊢ ran ⁡ E = ran ⁡ iEdg ⁡ G
13 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
14 12 13 eqtr4i ⊢ ran ⁡ E = Edg ⁡ G
15 f1oeq3 ⊢ ran ⁡ E = Edg ⁡ G → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ↔ E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
16 14 15 ax-mp ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ↔ E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
17 11 16 sylibr ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
18 17 3ad2ant1 ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
19 18 adantr ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
20 f1ocnvfv2 ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ∧ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ E -1 ⁡ P ⁡ i P ⁡ i + 1 = P ⁡ i P ⁡ i + 1
21 19 20 sylan ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 ∧ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ E -1 ⁡ P ⁡ i P ⁡ i + 1 = P ⁡ i P ⁡ i + 1
22 10 21 eqtrd ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 ∧ P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
23 22 ex ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P ∧ i ∈ 0 ..^ P − 1 → P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
24 23 ralimdva ⊢ G ∈ USHGraph ∧ P ∈ Word V ∧ 1 ≤ P → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
25 oveq2 ⊢ F = P − 1 → 0 ..^ F = 0 ..^ P − 1
26 25 raleqdv ⊢ F = P − 1 → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ↔ ∀ i ∈ 0 ..^ P − 1 E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
27 26 imbi2d ⊢ F = P − 1 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ F E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 ↔ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ ran ⁡ E → ∀ i ∈ 0 ..^ P − 1 E ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
28 24 27 imbitrrid ⊢ F = P − 1 → 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
29 4 28 mpcom ⊢ 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