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 
|- ( ph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )
Assertion wlklnwwlkln2lem 
|- ( ph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )

Proof

Step Hyp Ref Expression
1 wlklnwwlkln2lem.1 
 |-  ( ph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 wwlknbp 
 |-  ( P e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ P e. Word ( Vtx ` G ) ) )
4 iswwlksn 
 |-  ( N e. NN0 -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) )
5 4 adantr 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( P e. ( N WWalksN G ) <-> ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) )
6 lencl 
 |-  ( P e. Word ( Vtx ` G ) -> ( # ` P ) e. NN0 )
7 6 nn0cnd 
 |-  ( P e. Word ( Vtx ` G ) -> ( # ` P ) e. CC )
8 7 adantl 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( # ` P ) e. CC )
9 1cnd 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> 1 e. CC )
10 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
11 10 adantr 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> N e. CC )
12 8 9 11 subadd2d 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( ( ( # ` P ) - 1 ) = N <-> ( N + 1 ) = ( # ` P ) ) )
13 eqcom 
 |-  ( ( N + 1 ) = ( # ` P ) <-> ( # ` P ) = ( N + 1 ) )
14 12 13 bitr2di 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( ( # ` P ) = ( N + 1 ) <-> ( ( # ` P ) - 1 ) = N ) )
15 14 biimpcd 
 |-  ( ( # ` P ) = ( N + 1 ) -> ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( ( # ` P ) - 1 ) = N ) )
16 15 adantl 
 |-  ( ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) -> ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( ( # ` P ) - 1 ) = N ) )
17 16 impcom 
 |-  ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) -> ( ( # ` P ) - 1 ) = N )
18 1 com12 
 |-  ( P e. ( WWalks ` G ) -> ( ph -> E. f f ( Walks ` G ) P ) )
19 18 adantr 
 |-  ( ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) -> ( ph -> E. f f ( Walks ` G ) P ) )
20 19 adantl 
 |-  ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) -> ( ph -> E. f f ( Walks ` G ) P ) )
21 20 imp 
 |-  ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) -> E. f f ( Walks ` G ) P )
22 simpr 
 |-  ( ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) /\ f ( Walks ` G ) P ) -> f ( Walks ` G ) P )
23 wlklenvm1 
 |-  ( f ( Walks ` G ) P -> ( # ` f ) = ( ( # ` P ) - 1 ) )
24 22 23 jccir 
 |-  ( ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) /\ f ( Walks ` G ) P ) -> ( f ( Walks ` G ) P /\ ( # ` f ) = ( ( # ` P ) - 1 ) ) )
25 24 ex 
 |-  ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) -> ( f ( Walks ` G ) P -> ( f ( Walks ` G ) P /\ ( # ` f ) = ( ( # ` P ) - 1 ) ) ) )
26 25 eximdv 
 |-  ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) -> ( E. f f ( Walks ` G ) P -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = ( ( # ` P ) - 1 ) ) ) )
27 21 26 mpd 
 |-  ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = ( ( # ` P ) - 1 ) ) )
28 eqeq2 
 |-  ( ( ( # ` P ) - 1 ) = N -> ( ( # ` f ) = ( ( # ` P ) - 1 ) <-> ( # ` f ) = N ) )
29 28 anbi2d 
 |-  ( ( ( # ` P ) - 1 ) = N -> ( ( f ( Walks ` G ) P /\ ( # ` f ) = ( ( # ` P ) - 1 ) ) <-> ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )
30 29 exbidv 
 |-  ( ( ( # ` P ) - 1 ) = N -> ( E. f ( f ( Walks ` G ) P /\ ( # ` f ) = ( ( # ` P ) - 1 ) ) <-> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )
31 27 30 imbitrid 
 |-  ( ( ( # ` P ) - 1 ) = N -> ( ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) /\ ph ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )
32 31 expd 
 |-  ( ( ( # ` P ) - 1 ) = N -> ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) -> ( ph -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) )
33 17 32 mpcom 
 |-  ( ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) /\ ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) ) -> ( ph -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )
34 33 ex 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( ( P e. ( WWalks ` G ) /\ ( # ` P ) = ( N + 1 ) ) -> ( ph -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) )
35 5 34 sylbid 
 |-  ( ( N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( P e. ( N WWalksN G ) -> ( ph -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) )
36 35 3adant1 
 |-  ( ( G e. _V /\ N e. NN0 /\ P e. Word ( Vtx ` G ) ) -> ( P e. ( N WWalksN G ) -> ( ph -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) )
37 3 36 mpcom 
 |-  ( P e. ( N WWalksN G ) -> ( ph -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )
38 37 com12 
 |-  ( ph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) )