Metamath Proof Explorer


Theorem clwlkclwwlklem3

Description: Lemma 3 for clwlkclwwlk . (Contributed by Alexander van der Vekens, 22-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem3
|- ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> E : dom E -1-1-> R )
2 simp1
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> f e. Word dom E )
3 2 adantr
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> f e. Word dom E )
4 1 3 anim12i
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( E : dom E -1-1-> R /\ f e. Word dom E ) )
5 simp3
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) )
6 simpl2
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> P : ( 0 ... ( # ` f ) ) --> V )
7 5 6 anim12ci
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( P : ( 0 ... ( # ` f ) ) --> V /\ 2 <_ ( # ` P ) ) )
8 simp3
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
9 8 anim1i
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) )
10 9 adantl
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) )
11 clwlkclwwlklem2
 |-  ( ( ( E : dom E -1-1-> R /\ f e. Word dom E ) /\ ( P : ( 0 ... ( # ` f ) ) --> V /\ 2 <_ ( # ` P ) ) /\ ( A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )
12 4 7 10 11 syl3anc
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )
13 lencl
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
14 lencl
 |-  ( f e. Word dom E -> ( # ` f ) e. NN0 )
15 ffz0hash
 |-  ( ( ( # ` f ) e. NN0 /\ P : ( 0 ... ( # ` f ) ) --> V ) -> ( # ` P ) = ( ( # ` f ) + 1 ) )
16 oveq1
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( # ` P ) - 1 ) = ( ( ( # ` f ) + 1 ) - 1 ) )
17 16 oveq1d
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( ( # ` P ) - 1 ) - 0 ) = ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) )
18 nn0cn
 |-  ( ( # ` f ) e. NN0 -> ( # ` f ) e. CC )
19 peano2cn
 |-  ( ( # ` f ) e. CC -> ( ( # ` f ) + 1 ) e. CC )
20 peano2cnm
 |-  ( ( ( # ` f ) + 1 ) e. CC -> ( ( ( # ` f ) + 1 ) - 1 ) e. CC )
21 18 19 20 3syl
 |-  ( ( # ` f ) e. NN0 -> ( ( ( # ` f ) + 1 ) - 1 ) e. CC )
22 21 subid1d
 |-  ( ( # ` f ) e. NN0 -> ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) = ( ( ( # ` f ) + 1 ) - 1 ) )
23 1cnd
 |-  ( ( # ` f ) e. NN0 -> 1 e. CC )
24 18 23 pncand
 |-  ( ( # ` f ) e. NN0 -> ( ( ( # ` f ) + 1 ) - 1 ) = ( # ` f ) )
25 22 24 eqtrd
 |-  ( ( # ` f ) e. NN0 -> ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) = ( # ` f ) )
26 25 adantr
 |-  ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( ( # ` f ) + 1 ) - 1 ) - 0 ) = ( # ` f ) )
27 17 26 sylan9eqr
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( # ` P ) - 1 ) - 0 ) = ( # ` f ) )
28 27 oveq1d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( # ` f ) - 1 ) )
29 28 oveq2d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) = ( 0 ..^ ( ( # ` f ) - 1 ) ) )
30 29 raleqdv
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
31 oveq1
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( # ` P ) - 2 ) = ( ( ( # ` f ) + 1 ) - 2 ) )
32 2cnd
 |-  ( ( # ` f ) e. NN0 -> 2 e. CC )
33 18 32 23 subsub3d
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) - ( 2 - 1 ) ) = ( ( ( # ` f ) + 1 ) - 2 ) )
34 2m1e1
 |-  ( 2 - 1 ) = 1
35 34 a1i
 |-  ( ( # ` f ) e. NN0 -> ( 2 - 1 ) = 1 )
36 35 oveq2d
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) - ( 2 - 1 ) ) = ( ( # ` f ) - 1 ) )
37 33 36 eqtr3d
 |-  ( ( # ` f ) e. NN0 -> ( ( ( # ` f ) + 1 ) - 2 ) = ( ( # ` f ) - 1 ) )
38 37 adantr
 |-  ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( # ` f ) + 1 ) - 2 ) = ( ( # ` f ) - 1 ) )
39 31 38 sylan9eqr
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( # ` P ) - 2 ) = ( ( # ` f ) - 1 ) )
40 39 fveq2d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( P ` ( ( # ` P ) - 2 ) ) = ( P ` ( ( # ` f ) - 1 ) ) )
41 40 preq1d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } )
42 41 eleq1d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )
43 30 42 anbi12d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) <-> ( A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) )
44 43 anbi2d
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
45 3anass
 |-  ( ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) )
46 44 45 bitr4di
 |-  ( ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( # ` P ) = ( ( # ` f ) + 1 ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) )
47 46 expcom
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( ( # ` f ) e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
48 47 expd
 |-  ( ( # ` P ) = ( ( # ` f ) + 1 ) -> ( ( # ` f ) e. NN0 -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) )
49 15 48 syl
 |-  ( ( ( # ` f ) e. NN0 /\ P : ( 0 ... ( # ` f ) ) --> V ) -> ( ( # ` f ) e. NN0 -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) )
50 49 ex
 |-  ( ( # ` f ) e. NN0 -> ( P : ( 0 ... ( # ` f ) ) --> V -> ( ( # ` f ) e. NN0 -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) )
51 50 com23
 |-  ( ( # ` f ) e. NN0 -> ( ( # ` f ) e. NN0 -> ( P : ( 0 ... ( # ` f ) ) --> V -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) ) )
52 14 14 51 sylc
 |-  ( f e. Word dom E -> ( P : ( 0 ... ( # ` f ) ) --> V -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) ) )
53 52 imp
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V ) -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
54 53 3adant3
 |-  ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
55 54 adantr
 |-  ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( ( # ` P ) e. NN0 -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
56 13 55 syl5com
 |-  ( P e. Word V -> ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
57 56 3ad2ant2
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
58 57 imp
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0 ..^ ( ( # ` f ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` f ) - 1 ) ) , ( P ` 0 ) } e. ran E ) ) )
59 12 58 mpbird
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) )
60 59 ex
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
61 60 exlimdv
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
62 clwlkclwwlklem1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) )
63 61 62 impbid
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0 ..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )