Metamath Proof Explorer

Theorem upgrimwlklem3

Description: Lemma 3 for upgrimwlk . (Contributed by AV, 25-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.f ⊢ φ → F ∈ Word dom ⁡ I
Assertion upgrimwlklem3 ⊢ φ ∧ X ∈ 0 ..^ E → J ⁡ E ⁡ X = N I ⁡ F ⁡ X

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.f ⊢ φ → F ∈ Word dom ⁡ I
8 6 a1i ⊢ φ ∧ X ∈ 0 ..^ E → E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
9 2fveq3 ⊢ x = X → I ⁡ F ⁡ x = I ⁡ F ⁡ X
10 9 imaeq2d ⊢ x = X → N I ⁡ F ⁡ x = N I ⁡ F ⁡ X
11 10 fveq2d ⊢ x = X → J -1 ⁡ N I ⁡ F ⁡ x = J -1 ⁡ N I ⁡ F ⁡ X
12 11 adantl ⊢ φ ∧ X ∈ 0 ..^ E ∧ x = X → J -1 ⁡ N I ⁡ F ⁡ x = J -1 ⁡ N I ⁡ F ⁡ X
13 1 2 3 4 5 6 7 upgrimwlklem1 ⊢ φ → E = F
14 13 oveq2d ⊢ φ → 0 ..^ E = 0 ..^ F
15 wrdf ⊢ F ∈ Word dom ⁡ I → F : 0 ..^ F ⟶ dom ⁡ I
16 fdm ⊢ F : 0 ..^ F ⟶ dom ⁡ I → dom ⁡ F = 0 ..^ F
17 16 eqcomd ⊢ F : 0 ..^ F ⟶ dom ⁡ I → 0 ..^ F = dom ⁡ F
18 15 17 syl ⊢ F ∈ Word dom ⁡ I → 0 ..^ F = dom ⁡ F
19 7 18 syl ⊢ φ → 0 ..^ F = dom ⁡ F
20 14 19 eqtrd ⊢ φ → 0 ..^ E = dom ⁡ F
21 20 eleq2d ⊢ φ → X ∈ 0 ..^ E ↔ X ∈ dom ⁡ F
22 21 biimpa ⊢ φ ∧ X ∈ 0 ..^ E → X ∈ dom ⁡ F
23 fvexd ⊢ φ ∧ X ∈ 0 ..^ E → J -1 ⁡ N I ⁡ F ⁡ X ∈ V
24 8 12 22 23 fvmptd ⊢ φ ∧ X ∈ 0 ..^ E → E ⁡ X = J -1 ⁡ N I ⁡ F ⁡ X
25 24 fveq2d ⊢ φ ∧ X ∈ 0 ..^ E → J ⁡ E ⁡ X = J ⁡ J -1 ⁡ N I ⁡ F ⁡ X
26 4 adantr ⊢ φ ∧ X ∈ 0 ..^ E → H ∈ USHGraph
27 2 uspgrf1oedg ⊢ H ∈ USHGraph → J : dom ⁡ J ⟶ 1-1 onto Edg ⁡ H
28 26 27 syl ⊢ φ ∧ X ∈ 0 ..^ E → J : dom ⁡ J ⟶ 1-1 onto Edg ⁡ H
29 uspgruhgr ⊢ G ∈ USHGraph → G ∈ UHGraph
30 3 29 syl ⊢ φ → G ∈ UHGraph
31 uspgruhgr ⊢ H ∈ USHGraph → H ∈ UHGraph
32 4 31 syl ⊢ φ → H ∈ UHGraph
33 30 32 jca ⊢ φ → G ∈ UHGraph ∧ H ∈ UHGraph
34 33 adantr ⊢ φ ∧ X ∈ 0 ..^ E → G ∈ UHGraph ∧ H ∈ UHGraph
35 5 adantr ⊢ φ ∧ X ∈ 0 ..^ E → N ∈ G GraphIso H
36 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
37 30 36 syl ⊢ φ → Fun ⁡ I
38 37 adantr ⊢ φ ∧ X ∈ 0 ..^ E → Fun ⁡ I
39 13 7 wrdfd ⊢ φ → F : 0 ..^ E ⟶ dom ⁡ I
40 39 ffvelcdmda ⊢ φ ∧ X ∈ 0 ..^ E → F ⁡ X ∈ dom ⁡ I
41 1 iedgedg ⊢ Fun ⁡ I ∧ F ⁡ X ∈ dom ⁡ I → I ⁡ F ⁡ X ∈ Edg ⁡ G
42 38 40 41 syl2anc ⊢ φ ∧ X ∈ 0 ..^ E → I ⁡ F ⁡ X ∈ Edg ⁡ G
43 eqid ⊢ Edg ⁡ G = Edg ⁡ G
44 eqid ⊢ Edg ⁡ H = Edg ⁡ H
45 43 44 uhgrimedgi ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ N ∈ G GraphIso H ∧ I ⁡ F ⁡ X ∈ Edg ⁡ G → N I ⁡ F ⁡ X ∈ Edg ⁡ H
46 34 35 42 45 syl12anc ⊢ φ ∧ X ∈ 0 ..^ E → N I ⁡ F ⁡ X ∈ Edg ⁡ H
47 f1ocnvfv2 ⊢ J : dom ⁡ J ⟶ 1-1 onto Edg ⁡ H ∧ N I ⁡ F ⁡ X ∈ Edg ⁡ H → J ⁡ J -1 ⁡ N I ⁡ F ⁡ X = N I ⁡ F ⁡ X
48 28 46 47 syl2anc ⊢ φ ∧ X ∈ 0 ..^ E → J ⁡ J -1 ⁡ N I ⁡ F ⁡ X = N I ⁡ F ⁡ X
49 25 48 eqtrd ⊢ φ ∧ X ∈ 0 ..^ E → J ⁡ E ⁡ X = N I ⁡ F ⁡ X