Metamath Proof Explorer

Theorem upgrimwlklem5

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

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimwlk.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
Assertion upgrimwlklem5 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3 upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
4 upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
5 upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
6 upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
7 upgrimwlk.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
8 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
9 7 8 syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
10 1 2 3 4 5 6 9 upgrimwlklem1 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
11 10 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
13 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
14 3 13 syl ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
15 1 upgrwlkedg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
16 14 7 15 syl2anc ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
17 2fveq3 ⊢ ( 𝑥 = 𝑖 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) )
18 fveq2 ⊢ ( 𝑥 = 𝑖 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑖 ) )
19 fvoveq1 ⊢ ( 𝑥 = 𝑖 → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
20 18 19 preq12d ⊢ ( 𝑥 = 𝑖 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } )
21 17 20 eqeq12d ⊢ ( 𝑥 = 𝑖 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
22 21 rspcv ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } → ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } → ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
24 imaeq2 ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝑁 “ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) )
25 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
26 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
27 25 26 grimf1o ⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
28 f1ofn ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑁 Fn ( Vtx ‘ 𝐺 ) )
29 5 27 28 3syl ⊢ ( 𝜑 → 𝑁 Fn ( Vtx ‘ 𝐺 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑁 Fn ( Vtx ‘ 𝐺 ) )
31 25 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
32 7 31 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
34 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
36 33 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
37 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
39 33 38 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ( Vtx ‘ 𝐺 ) )
40 fnimapr ⊢ ( ( 𝑁 Fn ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 𝑖 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑁 “ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) = { ( 𝑁 ‘ ( 𝑃 ‘ 𝑖 ) ) , ( 𝑁 ‘ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) } )
41 30 36 39 40 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 “ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) = { ( 𝑁 ‘ ( 𝑃 ‘ 𝑖 ) ) , ( 𝑁 ‘ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) } )
42 7 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
43 42 31 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
44 43 35 fvco3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) = ( 𝑁 ‘ ( 𝑃 ‘ 𝑖 ) ) )
45 33 38 fvco3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑁 ‘ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
46 44 45 preq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } = { ( 𝑁 ‘ ( 𝑃 ‘ 𝑖 ) ) , ( 𝑁 ‘ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) } )
47 41 46 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 “ { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )
48 24 47 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )
49 48 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) )
50 23 49 syld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) )
51 50 ex ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) ) )
52 16 51 mpid ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) )
53 12 52 sylbid ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) )
54 53 imp ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )