Metamath Proof Explorer

Theorem wlknwwlksnbij

Description: The mapping ( t e. T |-> ( 2ndt ) ) is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Hypotheses wlknwwlksnbij.t ⊢ T = p ∈ Walks ⁡ G | 1 st ⁡ p = N
wlknwwlksnbij.w ⊢ W = N WWalksN G
wlknwwlksnbij.f ⊢ F = t ∈ T ⟼ 2 nd ⁡ t
Assertion wlknwwlksnbij ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → F : T ⟶ 1-1 onto W

Proof

Step Hyp Ref Expression
1 wlknwwlksnbij.t ⊢ T = p ∈ Walks ⁡ G | 1 st ⁡ p = N
2 wlknwwlksnbij.w ⊢ W = N WWalksN G
3 wlknwwlksnbij.f ⊢ F = t ∈ T ⟼ 2 nd ⁡ t
4 eqid ⊢ p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p = p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p
5 4 wlkswwlksf1o ⊢ G ∈ USHGraph → p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p : Walks ⁡ G ⟶ 1-1 onto WWalks ⁡ G
6 5 adantr ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p : Walks ⁡ G ⟶ 1-1 onto WWalks ⁡ G
7 fveqeq2 ⊢ q = 2 nd ⁡ p → q = N + 1 ↔ 2 nd ⁡ p = N + 1
8 7 3ad2ant3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ p ∈ Walks ⁡ G ∧ q = 2 nd ⁡ p → q = N + 1 ↔ 2 nd ⁡ p = N + 1
9 wlkcpr ⊢ p ∈ Walks ⁡ G ↔ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p
10 wlklenvp1 ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p → 2 nd ⁡ p = 1 st ⁡ p + 1
11 eqeq1 ⊢ 2 nd ⁡ p = 1 st ⁡ p + 1 → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p + 1 = N + 1
12 wlkcl ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p → 1 st ⁡ p ∈ ℕ 0
13 12 nn0cnd ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p → 1 st ⁡ p ∈ ℂ
14 13 adantr ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p ∧ G ∈ USHGraph ∧ N ∈ ℕ 0 → 1 st ⁡ p ∈ ℂ
15 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
16 15 adantl ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → N ∈ ℂ
17 16 adantl ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p ∧ G ∈ USHGraph ∧ N ∈ ℕ 0 → N ∈ ℂ
18 1cnd ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p ∧ G ∈ USHGraph ∧ N ∈ ℕ 0 → 1 ∈ ℂ
19 14 17 18 addcan2d ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p ∧ G ∈ USHGraph ∧ N ∈ ℕ 0 → 1 st ⁡ p + 1 = N + 1 ↔ 1 st ⁡ p = N
20 11 19 sylan9bbr ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p ∧ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ 2 nd ⁡ p = 1 st ⁡ p + 1 → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p = N
21 20 exp31 ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p → G ∈ USHGraph ∧ N ∈ ℕ 0 → 2 nd ⁡ p = 1 st ⁡ p + 1 → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p = N
22 10 21 mpid ⊢ 1 st ⁡ p Walks ⁡ G 2 nd ⁡ p → G ∈ USHGraph ∧ N ∈ ℕ 0 → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p = N
23 9 22 sylbi ⊢ p ∈ Walks ⁡ G → G ∈ USHGraph ∧ N ∈ ℕ 0 → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p = N
24 23 impcom ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ p ∈ Walks ⁡ G → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p = N
25 24 3adant3 ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ p ∈ Walks ⁡ G ∧ q = 2 nd ⁡ p → 2 nd ⁡ p = N + 1 ↔ 1 st ⁡ p = N
26 8 25 bitrd ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 ∧ p ∈ Walks ⁡ G ∧ q = 2 nd ⁡ p → q = N + 1 ↔ 1 st ⁡ p = N
27 4 6 26 f1oresrab ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N : p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟶ 1-1 onto q ∈ WWalks ⁡ G | q = N + 1
28 1 mpteq1i ⊢ t ∈ T ⟼ 2 nd ⁡ t = t ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ t
29 ssrab2 ⊢ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⊆ Walks ⁡ G
30 resmpt ⊢ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⊆ Walks ⁡ G → t ∈ Walks ⁡ G ⟼ 2 nd ⁡ t ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N = t ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ t
31 29 30 ax-mp ⊢ t ∈ Walks ⁡ G ⟼ 2 nd ⁡ t ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N = t ∈ p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟼ 2 nd ⁡ t
32 fveq2 ⊢ t = p → 2 nd ⁡ t = 2 nd ⁡ p
33 32 cbvmptv ⊢ t ∈ Walks ⁡ G ⟼ 2 nd ⁡ t = p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p
34 33 reseq1i ⊢ t ∈ Walks ⁡ G ⟼ 2 nd ⁡ t ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N = p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N
35 28 31 34 3eqtr2i ⊢ t ∈ T ⟼ 2 nd ⁡ t = p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N
36 35 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → t ∈ T ⟼ 2 nd ⁡ t = p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N
37 3 36 syl5eq ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → F = p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N
38 1 a1i ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → T = p ∈ Walks ⁡ G | 1 st ⁡ p = N
39 wwlksn ⊢ N ∈ ℕ 0 → N WWalksN G = q ∈ WWalks ⁡ G | q = N + 1
40 39 adantl ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → N WWalksN G = q ∈ WWalks ⁡ G | q = N + 1
41 2 40 syl5eq ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → W = q ∈ WWalks ⁡ G | q = N + 1
42 37 38 41 f1oeq123d ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → F : T ⟶ 1-1 onto W ↔ p ∈ Walks ⁡ G ⟼ 2 nd ⁡ p ↾ p ∈ Walks ⁡ G | 1 st ⁡ p = N : p ∈ Walks ⁡ G | 1 st ⁡ p = N ⟶ 1-1 onto q ∈ WWalks ⁡ G | q = N + 1
43 27 42 mpbird ⊢ G ∈ USHGraph ∧ N ∈ ℕ 0 → F : T ⟶ 1-1 onto W