Metamath Proof Explorer

Theorem dlwwlknondlwlknonf1o

Description: F is a bijection between the two representations of double loops of a fixed positive length on a fixed vertex. (Contributed by AV, 30-May-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses dlwwlknondlwlknonbij.v ⊢ V = Vtx ⁡ G
dlwwlknondlwlknonbij.w ⊢ W = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
dlwwlknondlwlknonbij.d ⊢ D = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
dlwwlknondlwlknonf1o.f ⊢ F = c ∈ W ⟼ 2 nd ⁡ c prefix 1 st ⁡ c
Assertion dlwwlknondlwlknonf1o ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → F : W ⟶ 1-1 onto D

Proof

Step Hyp Ref Expression
1 dlwwlknondlwlknonbij.v ⊢ V = Vtx ⁡ G
2 dlwwlknondlwlknonbij.w ⊢ W = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
3 dlwwlknondlwlknonbij.d ⊢ D = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
4 dlwwlknondlwlknonf1o.f ⊢ F = c ∈ W ⟼ 2 nd ⁡ c prefix 1 st ⁡ c
5 df-3an ⊢ 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X ↔ 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
6 5 rabbii ⊢ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
7 2 6 eqtri ⊢ W = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
8 eqid ⊢ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X
9 eqid ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ⟼ 2 nd ⁡ c prefix 1 st ⁡ c = c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ⟼ 2 nd ⁡ c prefix 1 st ⁡ c
10 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
11 1 8 9 clwwlknonclwlknonf1o ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℕ → c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ⟼ 2 nd ⁡ c prefix 1 st ⁡ c : w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ⟶ 1-1 onto X ClWWalksNOn ⁡ G N
12 10 11 syl3an3 ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ⟼ 2 nd ⁡ c prefix 1 st ⁡ c : w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ⟶ 1-1 onto X ClWWalksNOn ⁡ G N
13 fveq1 ⊢ y = 2 nd ⁡ c prefix 1 st ⁡ c → y ⁡ N − 2 = 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2
14 13 3ad2ant3 ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ y = 2 nd ⁡ c prefix 1 st ⁡ c → y ⁡ N − 2 = 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2
15 2fveq3 ⊢ w = c → 1 st ⁡ w = 1 st ⁡ c
16 15 eqeq1d ⊢ w = c → 1 st ⁡ w = N ↔ 1 st ⁡ c = N
17 fveq2 ⊢ w = c → 2 nd ⁡ w = 2 nd ⁡ c
18 17 fveq1d ⊢ w = c → 2 nd ⁡ w ⁡ 0 = 2 nd ⁡ c ⁡ 0
19 18 eqeq1d ⊢ w = c → 2 nd ⁡ w ⁡ 0 = X ↔ 2 nd ⁡ c ⁡ 0 = X
20 16 19 anbi12d ⊢ w = c → 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ↔ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X
21 20 elrab ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ↔ c ∈ ClWalks ⁡ G ∧ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X
22 simplrl ⊢ c ∈ ClWalks ⁡ G ∧ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X ∧ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c = N
23 simpll ⊢ c ∈ ClWalks ⁡ G ∧ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X ∧ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → c ∈ ClWalks ⁡ G
24 simpr3 ⊢ c ∈ ClWalks ⁡ G ∧ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X ∧ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → N ∈ ℤ ≥ 2
25 22 23 24 3jca ⊢ c ∈ ClWalks ⁡ G ∧ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X ∧ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2
26 25 ex ⊢ c ∈ ClWalks ⁡ G ∧ 1 st ⁡ c = N ∧ 2 nd ⁡ c ⁡ 0 = X → G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2
27 21 26 sylbi ⊢ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X → G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2
28 27 impcom ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X → 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2
29 dlwwlknondlwlknonf1olem1 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2
30 28 29 syl ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X → 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2
31 30 3adant3 ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ y = 2 nd ⁡ c prefix 1 st ⁡ c → 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2
32 14 31 eqtrd ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ y = 2 nd ⁡ c prefix 1 st ⁡ c → y ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2
33 32 eqeq1d ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ y = 2 nd ⁡ c prefix 1 st ⁡ c → y ⁡ N − 2 = X ↔ 2 nd ⁡ c ⁡ N − 2 = X
34 nfv ⊢ Ⅎ w 2 nd ⁡ c ⁡ N − 2 = X
35 17 fveq1d ⊢ w = c → 2 nd ⁡ w ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2
36 35 eqeq1d ⊢ w = c → 2 nd ⁡ w ⁡ N − 2 = X ↔ 2 nd ⁡ c ⁡ N − 2 = X
37 34 36 sbiev ⊢ c w 2 nd ⁡ w ⁡ N − 2 = X ↔ 2 nd ⁡ c ⁡ N − 2 = X
38 33 37 bitr4di ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 ∧ c ∈ w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ y = 2 nd ⁡ c prefix 1 st ⁡ c → y ⁡ N − 2 = X ↔ c w 2 nd ⁡ w ⁡ N − 2 = X
39 7 8 4 9 12 38 f1ossf1o ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → F : W ⟶ 1-1 onto y ∈ X ClWWalksNOn ⁡ G N | y ⁡ N − 2 = X
40 fveq1 ⊢ w = y → w ⁡ N − 2 = y ⁡ N − 2
41 40 eqeq1d ⊢ w = y → w ⁡ N − 2 = X ↔ y ⁡ N − 2 = X
42 41 cbvrabv ⊢ w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X = y ∈ X ClWWalksNOn ⁡ G N | y ⁡ N − 2 = X
43 3 42 eqtri ⊢ D = y ∈ X ClWWalksNOn ⁡ G N | y ⁡ N − 2 = X
44 f1oeq3 ⊢ D = y ∈ X ClWWalksNOn ⁡ G N | y ⁡ N − 2 = X → F : W ⟶ 1-1 onto D ↔ F : W ⟶ 1-1 onto y ∈ X ClWWalksNOn ⁡ G N | y ⁡ N − 2 = X
45 43 44 ax-mp ⊢ F : W ⟶ 1-1 onto D ↔ F : W ⟶ 1-1 onto y ∈ X ClWWalksNOn ⁡ G N | y ⁡ N − 2 = X
46 39 45 sylibr ⊢ G ∈ USHGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → F : W ⟶ 1-1 onto D