Metamath Proof Explorer

Theorem wwlksnextbi

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 16-Apr-2021) (Proof shortened by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnext.v 
|- V = ( Vtx ` G )
wwlksnext.e 
|- E = ( Edg ` G )
Assertion wwlksnextbi 
|- ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( W e. ( ( N + 1 ) WWalksN G ) <-> T e. ( N WWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 wwlksnext.v 
 |-  V = ( Vtx ` G )
2 wwlksnext.e 
 |-  E = ( Edg ` G )
3 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 ) )
4 wwlksnred 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )
5 4 ad2antrr 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )
6 fveqeq2 
 |-  ( W = ( T ++ <" S "> ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) <-> ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) )
7 6 3ad2ant2 
 |-  ( ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) <-> ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) )
8 7 adantl 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) <-> ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) )
9 s1cl 
 |-  ( S e. V -> <" S "> e. Word V )
10 9 adantl 
 |-  ( ( N e. NN0 /\ S e. V ) -> <" S "> e. Word V )
11 10 anim1ci 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( T e. Word V /\ <" S "> e. Word V ) )
12 ccatlen 
 |-  ( ( T e. Word V /\ <" S "> e. Word V ) -> ( # ` ( T ++ <" S "> ) ) = ( ( # ` T ) + ( # ` <" S "> ) ) )
13 11 12 syl 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( # ` ( T ++ <" S "> ) ) = ( ( # ` T ) + ( # ` <" S "> ) ) )
14 13 eqeq1d 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) <-> ( ( # ` T ) + ( # ` <" S "> ) ) = ( ( N + 1 ) + 1 ) ) )
15 s1len 
 |-  ( # ` <" S "> ) = 1
16 15 a1i 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( # ` <" S "> ) = 1 )
17 16 oveq2d 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( # ` T ) + ( # ` <" S "> ) ) = ( ( # ` T ) + 1 ) )
18 17 eqeq1d 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( ( # ` T ) + ( # ` <" S "> ) ) = ( ( N + 1 ) + 1 ) <-> ( ( # ` T ) + 1 ) = ( ( N + 1 ) + 1 ) ) )
19 lencl 
 |-  ( T e. Word V -> ( # ` T ) e. NN0 )
20 19 nn0cnd 
 |-  ( T e. Word V -> ( # ` T ) e. CC )
21 20 adantl 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( # ` T ) e. CC )
22 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
23 22 nn0cnd 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
24 23 ad2antrr 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( N + 1 ) e. CC )
25 1cnd 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> 1 e. CC )
26 21 24 25 addcan2d 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( ( # ` T ) + 1 ) = ( ( N + 1 ) + 1 ) <-> ( # ` T ) = ( N + 1 ) ) )
27 14 18 26 3bitrd 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) <-> ( # ` T ) = ( N + 1 ) ) )
28 oveq2 
 |-  ( ( N + 1 ) = ( # ` T ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = ( ( T ++ <" S "> ) prefix ( # ` T ) ) )
29 28 eqcoms 
 |-  ( ( # ` T ) = ( N + 1 ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = ( ( T ++ <" S "> ) prefix ( # ` T ) ) )
30 pfxccat1 
 |-  ( ( T e. Word V /\ <" S "> e. Word V ) -> ( ( T ++ <" S "> ) prefix ( # ` T ) ) = T )
31 11 30 syl 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( T ++ <" S "> ) prefix ( # ` T ) ) = T )
32 29 31 sylan9eqr 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) /\ ( # ` T ) = ( N + 1 ) ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T )
33 32 ex 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( # ` T ) = ( N + 1 ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
34 27 33 sylbid 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ T e. Word V ) -> ( ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
35 34 3ad2antr1 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
36 8 35 sylbid 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
37 36 imp 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T )
38 oveq1 
 |-  ( W = ( T ++ <" S "> ) -> ( W prefix ( N + 1 ) ) = ( ( T ++ <" S "> ) prefix ( N + 1 ) ) )
39 38 eqeq1d 
 |-  ( W = ( T ++ <" S "> ) -> ( ( W prefix ( N + 1 ) ) = T <-> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
40 39 3ad2ant2 
 |-  ( ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) -> ( ( W prefix ( N + 1 ) ) = T <-> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
41 40 ad2antlr 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( W prefix ( N + 1 ) ) = T <-> ( ( T ++ <" S "> ) prefix ( N + 1 ) ) = T ) )
42 37 41 mpbird 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( W prefix ( N + 1 ) ) = T )
43 42 eleq1d 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> T e. ( N WWalksN G ) ) )
44 43 biimpd 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) -> T e. ( N WWalksN G ) ) )
45 44 ex 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) -> T e. ( N WWalksN G ) ) ) )
46 45 com23 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> T e. ( N WWalksN G ) ) ) )
47 5 46 syld 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> T e. ( N WWalksN G ) ) ) )
48 47 com13 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> T e. ( N WWalksN G ) ) ) )
49 48 3ad2ant2 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> T e. ( N WWalksN G ) ) ) )
50 3 49 mpcom 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> T e. ( N WWalksN G ) ) )
51 50 com12 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( W e. ( ( N + 1 ) WWalksN G ) -> T e. ( N WWalksN G ) ) )
52 1 2 wwlksnext 
 |-  ( ( T e. ( N WWalksN G ) /\ S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) )
53 eleq1 
 |-  ( W = ( T ++ <" S "> ) -> ( W e. ( ( N + 1 ) WWalksN G ) <-> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) ) )
54 52 53 syl5ibrcom 
 |-  ( ( T e. ( N WWalksN G ) /\ S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( W = ( T ++ <" S "> ) -> W e. ( ( N + 1 ) WWalksN G ) ) )
55 54 3exp 
 |-  ( T e. ( N WWalksN G ) -> ( S e. V -> ( { ( lastS ` T ) , S } e. E -> ( W = ( T ++ <" S "> ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) ) )
56 55 com23 
 |-  ( T e. ( N WWalksN G ) -> ( { ( lastS ` T ) , S } e. E -> ( S e. V -> ( W = ( T ++ <" S "> ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) ) )
57 56 com14 
 |-  ( W = ( T ++ <" S "> ) -> ( { ( lastS ` T ) , S } e. E -> ( S e. V -> ( T e. ( N WWalksN G ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) ) )
58 57 imp 
 |-  ( ( W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) -> ( S e. V -> ( T e. ( N WWalksN G ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) )
59 58 3adant1 
 |-  ( ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) -> ( S e. V -> ( T e. ( N WWalksN G ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) )
60 59 com12 
 |-  ( S e. V -> ( ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) -> ( T e. ( N WWalksN G ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) )
61 60 adantl 
 |-  ( ( N e. NN0 /\ S e. V ) -> ( ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) -> ( T e. ( N WWalksN G ) -> W e. ( ( N + 1 ) WWalksN G ) ) ) )
62 61 imp 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( T e. ( N WWalksN G ) -> W e. ( ( N + 1 ) WWalksN G ) ) )
63 51 62 impbid 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( W e. ( ( N + 1 ) WWalksN G ) <-> T e. ( N WWalksN G ) ) )