Metamath Proof Explorer

Theorem upgrimwlklem2

Description: Lemma 2 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 upgrimwlklem2 ⊢ φ → E ∈ Word dom ⁡ J

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 4 adantr ⊢ φ ∧ x ∈ dom ⁡ F → H ∈ USHGraph
9 2 uspgrf1oedg ⊢ H ∈ USHGraph → J : dom ⁡ J ⟶ 1-1 onto Edg ⁡ H
10 8 9 syl ⊢ φ ∧ x ∈ dom ⁡ F → J : dom ⁡ J ⟶ 1-1 onto Edg ⁡ H
11 uspgruhgr ⊢ G ∈ USHGraph → G ∈ UHGraph
12 3 11 syl ⊢ φ → G ∈ UHGraph
13 uspgruhgr ⊢ H ∈ USHGraph → H ∈ UHGraph
14 4 13 syl ⊢ φ → H ∈ UHGraph
15 12 14 jca ⊢ φ → G ∈ UHGraph ∧ H ∈ UHGraph
16 15 adantr ⊢ φ ∧ x ∈ dom ⁡ F → G ∈ UHGraph ∧ H ∈ UHGraph
17 5 adantr ⊢ φ ∧ x ∈ dom ⁡ F → N ∈ G GraphIso H
18 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
19 12 18 syl ⊢ φ → Fun ⁡ I
20 19 adantr ⊢ φ ∧ x ∈ dom ⁡ F → Fun ⁡ I
21 wrdf ⊢ F ∈ Word dom ⁡ I → F : 0 ..^ F ⟶ dom ⁡ I
22 21 ffdmd ⊢ F ∈ Word dom ⁡ I → F : dom ⁡ F ⟶ dom ⁡ I
23 7 22 syl ⊢ φ → F : dom ⁡ F ⟶ dom ⁡ I
24 23 ffvelcdmda ⊢ φ ∧ x ∈ dom ⁡ F → F ⁡ x ∈ dom ⁡ I
25 1 iedgedg ⊢ Fun ⁡ I ∧ F ⁡ x ∈ dom ⁡ I → I ⁡ F ⁡ x ∈ Edg ⁡ G
26 20 24 25 syl2anc ⊢ φ ∧ x ∈ dom ⁡ F → I ⁡ F ⁡ x ∈ Edg ⁡ G
27 eqid ⊢ Edg ⁡ G = Edg ⁡ G
28 eqid ⊢ Edg ⁡ H = Edg ⁡ H
29 27 28 uhgrimedgi ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ N ∈ G GraphIso H ∧ I ⁡ F ⁡ x ∈ Edg ⁡ G → N I ⁡ F ⁡ x ∈ Edg ⁡ H
30 16 17 26 29 syl12anc ⊢ φ ∧ x ∈ dom ⁡ F → N I ⁡ F ⁡ x ∈ Edg ⁡ H
31 f1ocnvdm ⊢ J : dom ⁡ J ⟶ 1-1 onto Edg ⁡ H ∧ N I ⁡ F ⁡ x ∈ Edg ⁡ H → J -1 ⁡ N I ⁡ F ⁡ x ∈ dom ⁡ J
32 10 30 31 syl2anc ⊢ φ ∧ x ∈ dom ⁡ F → J -1 ⁡ N I ⁡ F ⁡ x ∈ dom ⁡ J
33 32 6 fmptd ⊢ φ → E : dom ⁡ F ⟶ dom ⁡ J
34 1 2 3 4 5 6 7 upgrimwlklem1 ⊢ φ → E = F
35 34 oveq2d ⊢ φ → 0 ..^ E = 0 ..^ F
36 iswrdb ⊢ F ∈ Word dom ⁡ I ↔ F : 0 ..^ F ⟶ dom ⁡ I
37 fdm ⊢ F : 0 ..^ F ⟶ dom ⁡ I → dom ⁡ F = 0 ..^ F
38 37 eqcomd ⊢ F : 0 ..^ F ⟶ dom ⁡ I → 0 ..^ F = dom ⁡ F
39 36 38 sylbi ⊢ F ∈ Word dom ⁡ I → 0 ..^ F = dom ⁡ F
40 7 39 syl ⊢ φ → 0 ..^ F = dom ⁡ F
41 35 40 eqtrd ⊢ φ → 0 ..^ E = dom ⁡ F
42 41 feq2d ⊢ φ → E : 0 ..^ E ⟶ dom ⁡ J ↔ E : dom ⁡ F ⟶ dom ⁡ J
43 33 42 mpbird ⊢ φ → E : 0 ..^ E ⟶ dom ⁡ J
44 iswrdb ⊢ E ∈ Word dom ⁡ J ↔ E : 0 ..^ E ⟶ dom ⁡ J
45 43 44 sylibr ⊢ φ → E ∈ Word dom ⁡ J