Metamath Proof Explorer

Theorem wlklnwwlkln2lem

Description: Lemma for wlklnwwlkln2 and wlklnwwlklnupgr2 . Formerly part of proof for wlklnwwlkln2 . (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Hypothesis wlklnwwlkln2lem.1 ⊢ ( 𝜑 → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
Assertion wlklnwwlkln2lem ( 𝜑 → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 wlklnwwlkln2lem.1 ⊢ ( 𝜑 → ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 wwlknbp ⊢ ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) )
4 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) )
5 4 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) )
6 lencl ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
7 6 nn0cnd ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑃 ) ∈ ℂ )
8 7 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℂ )
9 1cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → 1 ∈ ℂ )
10 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
11 10 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → 𝑁 ∈ ℂ )
12 8 9 11 subadd2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 ↔ ( 𝑁 + 1 ) = ( ♯ ‘ 𝑃 ) ) )
13 eqcom ⊢ ( ( 𝑁 + 1 ) = ( ♯ ‘ 𝑃 ) ↔ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) )
14 12 13 bitr2di ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ↔ ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 ) )
15 14 biimpcd ⊢ ( ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 ) )
16 15 adantl ⊢ ( ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 ) )
17 16 impcom ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 )
18 1 com12 ⊢ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) → ( 𝜑 → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
19 18 adantr ⊢ ( ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) → ( 𝜑 → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
20 19 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) → ( 𝜑 → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) )
21 20 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 )
22 simpr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑃 )
23 wlklenvm1 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
24 22 23 jccir ⊢ ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
25 24 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) )
26 25 eximdv ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) → ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑃 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) )
27 21 26 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
28 eqeq2 ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ↔ ( ♯ ‘ 𝑓 ) = 𝑁 ) )
29 28 anbi2d ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
30 29 exbidv ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
31 27 30 imbitrid ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 → ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ∧ 𝜑 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
32 31 expd ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑁 → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) → ( 𝜑 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) )
33 17 32 mpcom ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) → ( 𝜑 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
34 33 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) → ( 𝜑 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) )
35 5 34 sylbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝜑 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) )
36 35 3adant1 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝜑 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) )
37 3 36 mpcom ⊢ ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝜑 → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
38 37 com12 ⊢ ( 𝜑 → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )