Metamath Proof Explorer

Theorem upgrimwlklem5

Description: Lemma 5 for upgrimwlk . (Contributed by AV, 28-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ I = iEdg ⁡ G
upgrimwlk.j ⊢ J = iEdg ⁡ H
upgrimwlk.g ⊢ φ → G ∈ USHGraph
upgrimwlk.h ⊢ φ → H ∈ USHGraph
upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
upgrimwlk.w ⊢ φ → F Walks ⁡ G P
Assertion upgrimwlklem5 ⊢ φ ∧ i ∈ 0 ..^ E → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ I = iEdg ⁡ G
2 upgrimwlk.j ⊢ J = iEdg ⁡ H
3 upgrimwlk.g ⊢ φ → G ∈ USHGraph
4 upgrimwlk.h ⊢ φ → H ∈ USHGraph
5 upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
6 upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
7 upgrimwlk.w ⊢ φ → F Walks ⁡ G P
8 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
9 7 8 syl ⊢ φ → F ∈ Word dom ⁡ I
10 1 2 3 4 5 6 9 upgrimwlklem1 ⊢ φ → E = F
11 10 oveq2d ⊢ φ → 0 ..^ E = 0 ..^ F
12 11 eleq2d ⊢ φ → i ∈ 0 ..^ E ↔ i ∈ 0 ..^ F
13 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
14 3 13 syl ⊢ φ → G ∈ UPGraph
15 1 upgrwlkedg ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ x ∈ 0 ..^ F I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1
16 14 7 15 syl2anc ⊢ φ → ∀ x ∈ 0 ..^ F I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1
17 2fveq3 ⊢ x = i → I ⁡ F ⁡ x = I ⁡ F ⁡ i
18 fveq2 ⊢ x = i → P ⁡ x = P ⁡ i
19 fvoveq1 ⊢ x = i → P ⁡ x + 1 = P ⁡ i + 1
20 18 19 preq12d ⊢ x = i → P ⁡ x P ⁡ x + 1 = P ⁡ i P ⁡ i + 1
21 17 20 eqeq12d ⊢ x = i → I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1 ↔ I ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
22 21 rspcv ⊢ i ∈ 0 ..^ F → ∀ x ∈ 0 ..^ F I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1 → I ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
23 22 adantl ⊢ φ ∧ i ∈ 0 ..^ F → ∀ x ∈ 0 ..^ F I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1 → I ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1
24 imaeq2 ⊢ I ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 → N I ⁡ F ⁡ i = N P ⁡ i P ⁡ i + 1
25 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
26 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
27 25 26 grimf1o ⊢ N ∈ G GraphIso H → N : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
28 f1ofn ⊢ N : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → N Fn Vtx ⁡ G
29 5 27 28 3syl ⊢ φ → N Fn Vtx ⁡ G
30 29 adantr ⊢ φ ∧ i ∈ 0 ..^ F → N Fn Vtx ⁡ G
31 25 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ Vtx ⁡ G
32 7 31 syl ⊢ φ → P : 0 … F ⟶ Vtx ⁡ G
33 32 adantr ⊢ φ ∧ i ∈ 0 ..^ F → P : 0 … F ⟶ Vtx ⁡ G
34 elfzofz ⊢ i ∈ 0 ..^ F → i ∈ 0 … F
35 34 adantl ⊢ φ ∧ i ∈ 0 ..^ F → i ∈ 0 … F
36 33 35 ffvelcdmd ⊢ φ ∧ i ∈ 0 ..^ F → P ⁡ i ∈ Vtx ⁡ G
37 fzofzp1 ⊢ i ∈ 0 ..^ F → i + 1 ∈ 0 … F
38 37 adantl ⊢ φ ∧ i ∈ 0 ..^ F → i + 1 ∈ 0 … F
39 33 38 ffvelcdmd ⊢ φ ∧ i ∈ 0 ..^ F → P ⁡ i + 1 ∈ Vtx ⁡ G
40 fnimapr ⊢ N Fn Vtx ⁡ G ∧ P ⁡ i ∈ Vtx ⁡ G ∧ P ⁡ i + 1 ∈ Vtx ⁡ G → N P ⁡ i P ⁡ i + 1 = N ⁡ P ⁡ i N ⁡ P ⁡ i + 1
41 30 36 39 40 syl3anc ⊢ φ ∧ i ∈ 0 ..^ F → N P ⁡ i P ⁡ i + 1 = N ⁡ P ⁡ i N ⁡ P ⁡ i + 1
42 7 adantr ⊢ φ ∧ i ∈ 0 ..^ F → F Walks ⁡ G P
43 42 31 syl ⊢ φ ∧ i ∈ 0 ..^ F → P : 0 … F ⟶ Vtx ⁡ G
44 43 35 fvco3d ⊢ φ ∧ i ∈ 0 ..^ F → N ∘ P ⁡ i = N ⁡ P ⁡ i
45 33 38 fvco3d ⊢ φ ∧ i ∈ 0 ..^ F → N ∘ P ⁡ i + 1 = N ⁡ P ⁡ i + 1
46 44 45 preq12d ⊢ φ ∧ i ∈ 0 ..^ F → N ∘ P ⁡ i N ∘ P ⁡ i + 1 = N ⁡ P ⁡ i N ⁡ P ⁡ i + 1
47 41 46 eqtr4d ⊢ φ ∧ i ∈ 0 ..^ F → N P ⁡ i P ⁡ i + 1 = N ∘ P ⁡ i N ∘ P ⁡ i + 1
48 24 47 sylan9eqr ⊢ φ ∧ i ∈ 0 ..^ F ∧ I ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
49 48 ex ⊢ φ ∧ i ∈ 0 ..^ F → I ⁡ F ⁡ i = P ⁡ i P ⁡ i + 1 → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
50 23 49 syld ⊢ φ ∧ i ∈ 0 ..^ F → ∀ x ∈ 0 ..^ F I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1 → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
51 50 ex ⊢ φ → i ∈ 0 ..^ F → ∀ x ∈ 0 ..^ F I ⁡ F ⁡ x = P ⁡ x P ⁡ x + 1 → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
52 16 51 mpid ⊢ φ → i ∈ 0 ..^ F → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
53 12 52 sylbid ⊢ φ → i ∈ 0 ..^ E → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
54 53 imp ⊢ φ ∧ i ∈ 0 ..^ E → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1