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	⊢ 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 }
	wlknwwlksnbij.w	⊢ 𝑊 = ( 𝑁 WWalksN 𝐺 )
	wlknwwlksnbij.f	⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 2^nd ‘ 𝑡 ) )
Assertion	wlknwwlksnbij	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → 𝐹 : 𝑇 –1-1-onto→ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		wlknwwlksnbij.t	⊢ 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 }
2		wlknwwlksnbij.w	⊢ 𝑊 = ( 𝑁 WWalksN 𝐺 )
3		wlknwwlksnbij.f	⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 2^nd ‘ 𝑡 ) )
4		eqid	⊢ ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) = ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) )
5	4	wlkswwlksf1o	⊢ ( 𝐺 ∈ USPGraph → ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )
6	5	adantr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )
7		fveqeq2	⊢ ( 𝑞 = ( 2^nd ‘ 𝑝 ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ) )
8	7	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2^nd ‘ 𝑝 ) ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ) )
9		wlkcpr	⊢ ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) )
10		wlklenvp1	⊢ ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) → ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) + 1 ) )
11		eqeq1	⊢ ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) + 1 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) + 1 ) = ( 𝑁 + 1 ) ) )
12		wlkcl	⊢ ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) → ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) ∈ ℕ₀ )
13	12	nn0cnd	⊢ ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) → ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) ∈ ℂ )
14	13	adantr	⊢ ( ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ) → ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) ∈ ℂ )
15		nn0cn	⊢ ( 𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ )
16	15	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → 𝑁 ∈ ℂ )
17	16	adantl	⊢ ( ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ) → 𝑁 ∈ ℂ )
18		1cnd	⊢ ( ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ) → 1 ∈ ℂ )
19	14 17 18	addcan2d	⊢ ( ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) + 1 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) )
20	11 19	sylan9bbr	⊢ ( ( ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ) ∧ ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) + 1 ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) )
21	20	exp31	⊢ ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) + 1 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) ) ) )
22	10 21	mpid	⊢ ( ( 1^st ‘ 𝑝 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑝 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) ) )
23	9 22	sylbi	⊢ ( 𝑝 ∈ ( Walks ‘ 𝐺 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) ) )
24	23	impcom	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) )
25	24	3adant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2^nd ‘ 𝑝 ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) )
26	8 25	bitrd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2^nd ‘ 𝑝 ) ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 ) )
27	4 6 26	f1oresrab	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } –1-1-onto→ { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
28	1	mpteq1i	⊢ ( 𝑡 ∈ 𝑇 ↦ ( 2^nd ‘ 𝑡 ) ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑡 ) )
29		ssrab2	⊢ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ⊆ ( Walks ‘ 𝐺 )
30		resmpt	⊢ ( { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ⊆ ( Walks ‘ 𝐺 ) → ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑡 ) ) )
31	29 30	ax-mp	⊢ ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ↦ ( 2^nd ‘ 𝑡 ) )
32		fveq2	⊢ ( 𝑡 = 𝑝 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑝 ) )
33	32	cbvmptv	⊢ ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑡 ) ) = ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) )
34	33	reseq1i	⊢ ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } )
35	28 31 34	3eqtr2i	⊢ ( 𝑡 ∈ 𝑇 ↦ ( 2^nd ‘ 𝑡 ) ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } )
36	35	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑡 ∈ 𝑇 ↦ ( 2^nd ‘ 𝑡 ) ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) )
37	3 36	syl5eq	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → 𝐹 = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) )
38	1	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } )
39		wwlksn	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑁 WWalksN 𝐺 ) = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
40	39	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑁 WWalksN 𝐺 ) = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
41	2 40	syl5eq	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → 𝑊 = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
42	37 38 41	f1oeq123d	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → ( 𝐹 : 𝑇 –1-1-onto→ 𝑊 ↔ ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2^nd ‘ 𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1^st ‘ 𝑝 ) ) = 𝑁 } –1-1-onto→ { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) )
43	27 42	mpbird	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) → 𝐹 : 𝑇 –1-1-onto→ 𝑊 )

Metamath Proof Explorer

Theorem wlknwwlksnbij

Proof