Metamath Proof Explorer

Theorem wwlksnextwrd

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij0.v 
|- V = ( Vtx ` G )
wwlksnextbij0.e 
|- E = ( Edg ` G )
wwlksnextbij0.d 
|- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
Assertion wwlksnextwrd 
|- ( W e. ( N WWalksN G ) -> D = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v 
 |-  V = ( Vtx ` G )
2 wwlksnextbij0.e 
 |-  E = ( Edg ` G )
3 wwlksnextbij0.d 
 |-  D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
4 3anass 
 |-  ( ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) <-> ( ( # ` w ) = ( N + 2 ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) )
5 4 bianass 
 |-  ( ( w e. Word V /\ ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) <-> ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) )
6 1 wwlknbp 
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
7 simpl 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> N e. NN0 )
8 simpl 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) -> w e. Word V )
9 nn0re 
 |-  ( N e. NN0 -> N e. RR )
10 2re 
 |-  2 e. RR
11 10 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
12 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
13 2pos 
 |-  0 < 2
14 13 a1i 
 |-  ( N e. NN0 -> 0 < 2 )
15 9 11 12 14 addgegt0d 
 |-  ( N e. NN0 -> 0 < ( N + 2 ) )
16 15 adantr 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> 0 < ( N + 2 ) )
17 breq2 
 |-  ( ( # ` w ) = ( N + 2 ) -> ( 0 < ( # ` w ) <-> 0 < ( N + 2 ) ) )
18 17 ad2antll 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( 0 < ( # ` w ) <-> 0 < ( N + 2 ) ) )
19 16 18 mpbird 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> 0 < ( # ` w ) )
20 hashgt0n0 
 |-  ( ( w e. Word V /\ 0 < ( # ` w ) ) -> w =/= (/) )
21 8 19 20 syl2an2 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> w =/= (/) )
22 lswcl 
 |-  ( ( w e. Word V /\ w =/= (/) ) -> ( lastS ` w ) e. V )
23 8 21 22 syl2an2 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( lastS ` w ) e. V )
24 23 adantrr 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> ( lastS ` w ) e. V )
25 pfxcl 
 |-  ( w e. Word V -> ( w prefix ( N + 1 ) ) e. Word V )
26 eleq1 
 |-  ( W = ( w prefix ( N + 1 ) ) -> ( W e. Word V <-> ( w prefix ( N + 1 ) ) e. Word V ) )
27 25 26 imbitrrid 
 |-  ( W = ( w prefix ( N + 1 ) ) -> ( w e. Word V -> W e. Word V ) )
28 27 eqcoms 
 |-  ( ( w prefix ( N + 1 ) ) = W -> ( w e. Word V -> W e. Word V ) )
29 28 adantr 
 |-  ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) -> ( w e. Word V -> W e. Word V ) )
30 29 com12 
 |-  ( w e. Word V -> ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) -> W e. Word V ) )
31 30 adantr 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) -> ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) -> W e. Word V ) )
32 31 imp 
 |-  ( ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> W e. Word V )
33 32 adantl 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> W e. Word V )
34 oveq1 
 |-  ( W = ( w prefix ( N + 1 ) ) -> ( W ++ <" ( lastS ` w ) "> ) = ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) )
35 34 eqcoms 
 |-  ( ( w prefix ( N + 1 ) ) = W -> ( W ++ <" ( lastS ` w ) "> ) = ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) )
36 35 adantr 
 |-  ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) -> ( W ++ <" ( lastS ` w ) "> ) = ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) )
37 36 ad2antll 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> ( W ++ <" ( lastS ` w ) "> ) = ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) )
38 oveq1 
 |-  ( ( # ` w ) = ( N + 2 ) -> ( ( # ` w ) - 1 ) = ( ( N + 2 ) - 1 ) )
39 38 adantl 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) -> ( ( # ` w ) - 1 ) = ( ( N + 2 ) - 1 ) )
40 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
41 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
42 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
43 40 41 42 addsubassd 
 |-  ( N e. NN0 -> ( ( N + 2 ) - 1 ) = ( N + ( 2 - 1 ) ) )
44 2m1e1 
 |-  ( 2 - 1 ) = 1
45 44 a1i 
 |-  ( N e. NN0 -> ( 2 - 1 ) = 1 )
46 45 oveq2d 
 |-  ( N e. NN0 -> ( N + ( 2 - 1 ) ) = ( N + 1 ) )
47 43 46 eqtrd 
 |-  ( N e. NN0 -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
48 39 47 sylan9eqr 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( ( # ` w ) - 1 ) = ( N + 1 ) )
49 48 oveq2d 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( w prefix ( ( # ` w ) - 1 ) ) = ( w prefix ( N + 1 ) ) )
50 49 oveq1d 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) = ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) )
51 pfxlswccat 
 |-  ( ( w e. Word V /\ w =/= (/) ) -> ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) = w )
52 8 21 51 syl2an2 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) = w )
53 50 52 eqtr3d 
 |-  ( ( N e. NN0 /\ ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) -> ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) = w )
54 53 adantrr 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> ( ( w prefix ( N + 1 ) ) ++ <" ( lastS ` w ) "> ) = w )
55 37 54 eqtr2d 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> w = ( W ++ <" ( lastS ` w ) "> ) )
56 simprrr 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> { ( lastS ` W ) , ( lastS ` w ) } e. E )
57 1 2 wwlksnextbi 
 |-  ( ( ( N e. NN0 /\ ( lastS ` w ) e. V ) /\ ( W e. Word V /\ w = ( W ++ <" ( lastS ` w ) "> ) /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> ( w e. ( ( N + 1 ) WWalksN G ) <-> W e. ( N WWalksN G ) ) )
58 7 24 33 55 56 57 syl23anc 
 |-  ( ( N e. NN0 /\ ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) -> ( w e. ( ( N + 1 ) WWalksN G ) <-> W e. ( N WWalksN G ) ) )
59 58 exbiri 
 |-  ( N e. NN0 -> ( ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> ( W e. ( N WWalksN G ) -> w e. ( ( N + 1 ) WWalksN G ) ) ) )
60 59 com23 
 |-  ( N e. NN0 -> ( W e. ( N WWalksN G ) -> ( ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> w e. ( ( N + 1 ) WWalksN G ) ) ) )
61 60 3ad2ant2 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) -> ( W e. ( N WWalksN G ) -> ( ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> w e. ( ( N + 1 ) WWalksN G ) ) ) )
62 6 61 mpcom 
 |-  ( W e. ( N WWalksN G ) -> ( ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> w e. ( ( N + 1 ) WWalksN G ) ) )
63 62 expcomd 
 |-  ( W e. ( N WWalksN G ) -> ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) -> ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) -> w e. ( ( N + 1 ) WWalksN G ) ) ) )
64 63 imp 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) -> w e. ( ( N + 1 ) WWalksN G ) ) )
65 1 2 wwlknp 
 |-  ( w e. ( ( N + 1 ) WWalksN G ) -> ( w e. Word V /\ ( # ` w ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
66 40 42 42 addassd 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
67 1p1e2 
 |-  ( 1 + 1 ) = 2
68 67 a1i 
 |-  ( N e. NN0 -> ( 1 + 1 ) = 2 )
69 68 oveq2d 
 |-  ( N e. NN0 -> ( N + ( 1 + 1 ) ) = ( N + 2 ) )
70 66 69 eqtrd 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
71 70 eqeq2d 
 |-  ( N e. NN0 -> ( ( # ` w ) = ( ( N + 1 ) + 1 ) <-> ( # ` w ) = ( N + 2 ) ) )
72 71 biimpd 
 |-  ( N e. NN0 -> ( ( # ` w ) = ( ( N + 1 ) + 1 ) -> ( # ` w ) = ( N + 2 ) ) )
73 72 adantr 
 |-  ( ( N e. NN0 /\ W e. Word V ) -> ( ( # ` w ) = ( ( N + 1 ) + 1 ) -> ( # ` w ) = ( N + 2 ) ) )
74 73 com12 
 |-  ( ( # ` w ) = ( ( N + 1 ) + 1 ) -> ( ( N e. NN0 /\ W e. Word V ) -> ( # ` w ) = ( N + 2 ) ) )
75 74 adantl 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( ( N + 1 ) + 1 ) ) -> ( ( N e. NN0 /\ W e. Word V ) -> ( # ` w ) = ( N + 2 ) ) )
76 simpl 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( ( N + 1 ) + 1 ) ) -> w e. Word V )
77 75 76 jctild 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( ( N + 1 ) + 1 ) ) -> ( ( N e. NN0 /\ W e. Word V ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
78 77 3adant3 
 |-  ( ( w e. Word V /\ ( # ` w ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) -> ( ( N e. NN0 /\ W e. Word V ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
79 65 78 syl 
 |-  ( w e. ( ( N + 1 ) WWalksN G ) -> ( ( N e. NN0 /\ W e. Word V ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
80 79 com12 
 |-  ( ( N e. NN0 /\ W e. Word V ) -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
81 80 3adant1 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
82 6 81 syl 
 |-  ( W e. ( N WWalksN G ) -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
83 82 adantr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> ( w e. ( ( N + 1 ) WWalksN G ) -> ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) ) )
84 64 83 impbid 
 |-  ( ( W e. ( N WWalksN G ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) -> ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) <-> w e. ( ( N + 1 ) WWalksN G ) ) )
85 84 ex 
 |-  ( W e. ( N WWalksN G ) -> ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) -> ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) <-> w e. ( ( N + 1 ) WWalksN G ) ) ) )
86 85 pm5.32rd 
 |-  ( W e. ( N WWalksN G ) -> ( ( ( w e. Word V /\ ( # ` w ) = ( N + 2 ) ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) <-> ( w e. ( ( N + 1 ) WWalksN G ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) )
87 5 86 bitrid 
 |-  ( W e. ( N WWalksN G ) -> ( ( w e. Word V /\ ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) <-> ( w e. ( ( N + 1 ) WWalksN G ) /\ ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) ) ) )
88 87 rabbidva2 
 |-  ( W e. ( N WWalksN G ) -> { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )
89 3 88 eqtrid 
 |-  ( W e. ( N WWalksN G ) -> D = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )