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

Metamath Proof Explorer

Theorem upgrimwlklem3

Description: Lemma 3 for upgrimwlk . (Contributed by AV, 25-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimwlk.f ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
Assertion upgrimwlklem3 ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )

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.f ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
8 6 a1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
9 2fveq3 ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) )
10 9 imaeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
11 10 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
12 11 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ 𝑥 = 𝑋 ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
13 1 2 3 4 5 6 7 upgrimwlklem1 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
14 13 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
15 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
16 fdm ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17 16 eqcomd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
18 15 17 syl ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
19 7 18 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
20 14 19 eqtrd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = dom 𝐹 )
21 20 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ↔ 𝑋 ∈ dom 𝐹 ) )
22 21 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝑋 ∈ dom 𝐹 )
23 fvexd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ∈ V )
24 8 12 22 23 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐸 ‘ 𝑋 ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
25 24 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
26 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝐻 ∈ USPGraph )
27 2 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
29 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
30 3 29 syl ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
31 uspgruhgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
32 4 31 syl ⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
33 30 32 jca ⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
35 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
36 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
37 30 36 syl ⊢ ( 𝜑 → Fun 𝐼 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → Fun 𝐼 )
39 13 7 wrdfd ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐼 )
40 39 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 )
41 1 iedgedg ⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) )
42 38 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) )
43 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
44 eqid ⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
45 43 44 uhgrimedgi ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
46 34 35 42 45 syl12anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
47 f1ocnvfv2 ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
48 28 46 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
49 25 48 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )