Metamath Proof Explorer

Theorem clwlkclwwlklem2a4

Description: Lemma 4 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Hypothesis clwlkclwwlklem2.f 
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )
Assertion clwlkclwwlklem2a4 
|- ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E -> ( E ` ( F ` I ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f 
 |-  F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )
2 fveq2 
 |-  ( I = ( ( # ` P ) - 2 ) -> ( F ` I ) = ( F ` ( ( # ` P ) - 2 ) ) )
3 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
4 1 clwlkclwwlklem2fv2 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( F ` ( ( # ` P ) - 2 ) ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
5 3 4 sylan 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( F ` ( ( # ` P ) - 2 ) ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
6 2 5 sylan9eqr 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ I = ( ( # ` P ) - 2 ) ) -> ( F ` I ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
7 6 ex 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( I = ( ( # ` P ) - 2 ) -> ( F ` I ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) ) )
8 7 3adant1 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( I = ( ( # ` P ) - 2 ) -> ( F ` I ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) ) )
9 8 ad2antrr 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> ( I = ( ( # ` P ) - 2 ) -> ( F ` I ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) ) )
10 9 impcom 
 |-  ( ( I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( F ` I ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
11 10 fveq2d 
 |-  ( ( I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( E ` ( F ` I ) ) = ( E ` ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) ) )
12 f1f1orn 
 |-  ( E : dom E -1-1-> R -> E : dom E -1-1-onto-> ran E )
13 12 3ad2ant1 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> E : dom E -1-1-onto-> ran E )
14 13 ad2antrr 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> E : dom E -1-1-onto-> ran E )
15 lsw 
 |-  ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
16 15 eqeq1d 
 |-  ( P e. Word V -> ( ( lastS ` P ) = ( P ` 0 ) <-> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) ) )
17 nn0cn 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. CC )
18 id 
 |-  ( ( # ` P ) e. CC -> ( # ` P ) e. CC )
19 2cnd 
 |-  ( ( # ` P ) e. CC -> 2 e. CC )
20 1cnd 
 |-  ( ( # ` P ) e. CC -> 1 e. CC )
21 18 19 20 subsubd 
 |-  ( ( # ` P ) e. CC -> ( ( # ` P ) - ( 2 - 1 ) ) = ( ( ( # ` P ) - 2 ) + 1 ) )
22 2m1e1 
 |-  ( 2 - 1 ) = 1
23 22 a1i 
 |-  ( ( # ` P ) e. CC -> ( 2 - 1 ) = 1 )
24 23 oveq2d 
 |-  ( ( # ` P ) e. CC -> ( ( # ` P ) - ( 2 - 1 ) ) = ( ( # ` P ) - 1 ) )
25 21 24 eqtr3d 
 |-  ( ( # ` P ) e. CC -> ( ( ( # ` P ) - 2 ) + 1 ) = ( ( # ` P ) - 1 ) )
26 3 17 25 3syl 
 |-  ( P e. Word V -> ( ( ( # ` P ) - 2 ) + 1 ) = ( ( # ` P ) - 1 ) )
27 26 adantr 
 |-  ( ( P e. Word V /\ ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) ) -> ( ( ( # ` P ) - 2 ) + 1 ) = ( ( # ` P ) - 1 ) )
28 27 fveq2d 
 |-  ( ( P e. Word V /\ ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) )
29 eqeq2 
 |-  ( ( P ` 0 ) = ( P ` ( ( # ` P ) - 1 ) ) -> ( ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) <-> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) ) )
30 29 eqcoms 
 |-  ( ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) -> ( ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) <-> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) ) )
31 30 adantl 
 |-  ( ( P e. Word V /\ ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) ) -> ( ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) <-> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) ) )
32 28 31 mpbird 
 |-  ( ( P e. Word V /\ ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) )
33 32 ex 
 |-  ( P e. Word V -> ( ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) ) )
34 16 33 sylbid 
 |-  ( P e. Word V -> ( ( lastS ` P ) = ( P ` 0 ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) ) )
35 34 3ad2ant2 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( lastS ` P ) = ( P ` 0 ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) ) )
36 35 com12 
 |-  ( ( lastS ` P ) = ( P ` 0 ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) ) )
37 36 adantr 
 |-  ( ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) ) )
38 37 impcom 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) )
39 38 adantr 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ I = ( ( # ` P ) - 2 ) ) -> ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) = ( P ` 0 ) )
40 39 preq2d 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ I = ( ( # ` P ) - 2 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } )
41 fveq2 
 |-  ( I = ( ( # ` P ) - 2 ) -> ( P ` I ) = ( P ` ( ( # ` P ) - 2 ) ) )
42 fvoveq1 
 |-  ( I = ( ( # ` P ) - 2 ) -> ( P ` ( I + 1 ) ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
43 41 42 preq12d 
 |-  ( I = ( ( # ` P ) - 2 ) -> { ( P ` I ) , ( P ` ( I + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } )
44 43 eqeq1d 
 |-  ( I = ( ( # ` P ) - 2 ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } <-> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
45 44 adantl 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ I = ( ( # ` P ) - 2 ) ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } <-> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
46 40 45 mpbird 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ I = ( ( # ` P ) - 2 ) ) -> { ( P ` I ) , ( P ` ( I + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } )
47 46 eleq1d 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ I = ( ( # ` P ) - 2 ) ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E <-> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) )
48 47 biimpd 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ I = ( ( # ` P ) - 2 ) ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) )
49 48 impancom 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) )
50 49 impcom 
 |-  ( ( I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E )
51 f1ocnvfv2 
 |-  ( ( E : dom E -1-1-onto-> ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) -> ( E ` ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) ) = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } )
52 14 50 51 syl2an2 
 |-  ( ( I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( E ` ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) ) = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } )
53 eqcom 
 |-  ( ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) <-> ( P ` 0 ) = ( P ` ( ( # ` P ) - 1 ) ) )
54 53 biimpi 
 |-  ( ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) -> ( P ` 0 ) = ( P ` ( ( # ` P ) - 1 ) ) )
55 1e2m1 
 |-  1 = ( 2 - 1 )
56 55 a1i 
 |-  ( P e. Word V -> 1 = ( 2 - 1 ) )
57 56 oveq2d 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( # ` P ) - ( 2 - 1 ) ) )
58 3 17 syl 
 |-  ( P e. Word V -> ( # ` P ) e. CC )
59 2cnd 
 |-  ( P e. Word V -> 2 e. CC )
60 1cnd 
 |-  ( P e. Word V -> 1 e. CC )
61 58 59 60 subsubd 
 |-  ( P e. Word V -> ( ( # ` P ) - ( 2 - 1 ) ) = ( ( ( # ` P ) - 2 ) + 1 ) )
62 57 61 eqtrd 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( ( # ` P ) - 2 ) + 1 ) )
63 62 fveq2d 
 |-  ( P e. Word V -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
64 54 63 sylan9eqr 
 |-  ( ( P e. Word V /\ ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) ) -> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
65 64 ex 
 |-  ( P e. Word V -> ( ( P ` ( ( # ` P ) - 1 ) ) = ( P ` 0 ) -> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) ) )
66 16 65 sylbid 
 |-  ( P e. Word V -> ( ( lastS ` P ) = ( P ` 0 ) -> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) ) )
67 66 imp 
 |-  ( ( P e. Word V /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
68 67 preq2d 
 |-  ( ( P e. Word V /\ ( lastS ` P ) = ( P ` 0 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } )
69 68 adantr 
 |-  ( ( ( P e. Word V /\ ( lastS ` P ) = ( P ` 0 ) ) /\ I = ( ( # ` P ) - 2 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } )
70 43 adantl 
 |-  ( ( ( P e. Word V /\ ( lastS ` P ) = ( P ` 0 ) ) /\ I = ( ( # ` P ) - 2 ) ) -> { ( P ` I ) , ( P ` ( I + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } )
71 69 70 eqtr4d 
 |-  ( ( ( P e. Word V /\ ( lastS ` P ) = ( P ` 0 ) ) /\ I = ( ( # ` P ) - 2 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
72 71 exp31 
 |-  ( P e. Word V -> ( ( lastS ` P ) = ( P ` 0 ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )
73 72 3ad2ant2 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( lastS ` P ) = ( P ` 0 ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )
74 73 com12 
 |-  ( ( lastS ` P ) = ( P ` 0 ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )
75 74 adantr 
 |-  ( ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )
76 75 impcom 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
77 76 adantr 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> ( I = ( ( # ` P ) - 2 ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
78 77 impcom 
 |-  ( ( I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
79 11 52 78 3eqtrd 
 |-  ( ( I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( E ` ( F ` I ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
80 simpll 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> ( # ` P ) e. NN0 )
81 oveq1 
 |-  ( ( # ` P ) = 2 -> ( ( # ` P ) - 1 ) = ( 2 - 1 ) )
82 81 22 eqtrdi 
 |-  ( ( # ` P ) = 2 -> ( ( # ` P ) - 1 ) = 1 )
83 82 oveq2d 
 |-  ( ( # ` P ) = 2 -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( 0 ..^ 1 ) )
84 83 eleq2d 
 |-  ( ( # ` P ) = 2 -> ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) <-> I e. ( 0 ..^ 1 ) ) )
85 oveq1 
 |-  ( ( # ` P ) = 2 -> ( ( # ` P ) - 2 ) = ( 2 - 2 ) )
86 2cn 
 |-  2 e. CC
87 86 subidi 
 |-  ( 2 - 2 ) = 0
88 85 87 eqtrdi 
 |-  ( ( # ` P ) = 2 -> ( ( # ` P ) - 2 ) = 0 )
89 88 eqeq2d 
 |-  ( ( # ` P ) = 2 -> ( I = ( ( # ` P ) - 2 ) <-> I = 0 ) )
90 89 notbid 
 |-  ( ( # ` P ) = 2 -> ( -. I = ( ( # ` P ) - 2 ) <-> -. I = 0 ) )
91 84 90 anbi12d 
 |-  ( ( # ` P ) = 2 -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) <-> ( I e. ( 0 ..^ 1 ) /\ -. I = 0 ) ) )
92 elsni 
 |-  ( I e. { 0 } -> I = 0 )
93 92 pm2.24d 
 |-  ( I e. { 0 } -> ( -. I = 0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
94 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
95 93 94 eleq2s 
 |-  ( I e. ( 0 ..^ 1 ) -> ( -. I = 0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
96 95 imp 
 |-  ( ( I e. ( 0 ..^ 1 ) /\ -. I = 0 ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) )
97 91 96 syl6bi 
 |-  ( ( # ` P ) = 2 -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
98 97 adantld 
 |-  ( ( # ` P ) = 2 -> ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
99 df-ne 
 |-  ( ( # ` P ) =/= 2 <-> -. ( # ` P ) = 2 )
100 2re 
 |-  2 e. RR
101 100 a1i 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 2 e. RR )
102 nn0re 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
103 102 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. RR )
104 simpr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) )
105 101 103 104 leltned 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( 2 < ( # ` P ) <-> ( # ` P ) =/= 2 ) )
106 elfzo0 
 |-  ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) <-> ( I e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ I < ( ( # ` P ) - 1 ) ) )
107 simp-4l 
 |-  ( ( ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) /\ 2 < ( # ` P ) ) /\ I < ( ( # ` P ) - 1 ) ) -> I e. NN0 )
108 nn0z 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
109 2z 
 |-  2 e. ZZ
110 109 a1i 
 |-  ( ( # ` P ) e. NN0 -> 2 e. ZZ )
111 108 110 zsubcld 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. ZZ )
112 111 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 < ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. ZZ )
113 100 a1i 
 |-  ( ( # ` P ) e. NN0 -> 2 e. RR )
114 113 102 posdifd 
 |-  ( ( # ` P ) e. NN0 -> ( 2 < ( # ` P ) <-> 0 < ( ( # ` P ) - 2 ) ) )
115 114 biimpa 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 < ( # ` P ) ) -> 0 < ( ( # ` P ) - 2 ) )
116 elnnz 
 |-  ( ( ( # ` P ) - 2 ) e. NN <-> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 < ( ( # ` P ) - 2 ) ) )
117 112 115 116 sylanbrc 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 < ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. NN )
118 117 ad5ant24 
 |-  ( ( ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) /\ 2 < ( # ` P ) ) /\ I < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) - 2 ) e. NN )
119 nn0z 
 |-  ( I e. NN0 -> I e. ZZ )
120 peano2zm 
 |-  ( ( # ` P ) e. ZZ -> ( ( # ` P ) - 1 ) e. ZZ )
121 108 120 syl 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. ZZ )
122 zltlem1 
 |-  ( ( I e. ZZ /\ ( ( # ` P ) - 1 ) e. ZZ ) -> ( I < ( ( # ` P ) - 1 ) <-> I <_ ( ( ( # ` P ) - 1 ) - 1 ) ) )
123 119 121 122 syl2an 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( I < ( ( # ` P ) - 1 ) <-> I <_ ( ( ( # ` P ) - 1 ) - 1 ) ) )
124 17 adantl 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( # ` P ) e. CC )
125 1cnd 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> 1 e. CC )
126 124 125 125 subsub4d 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - ( 1 + 1 ) ) )
127 1p1e2 
 |-  ( 1 + 1 ) = 2
128 127 a1i 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( 1 + 1 ) = 2 )
129 128 oveq2d 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - ( 1 + 1 ) ) = ( ( # ` P ) - 2 ) )
130 126 129 eqtrd 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - 2 ) )
131 130 breq2d 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( I <_ ( ( ( # ` P ) - 1 ) - 1 ) <-> I <_ ( ( # ` P ) - 2 ) ) )
132 123 131 bitrd 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( I < ( ( # ` P ) - 1 ) <-> I <_ ( ( # ` P ) - 2 ) ) )
133 necom 
 |-  ( ( ( # ` P ) - 2 ) =/= I <-> I =/= ( ( # ` P ) - 2 ) )
134 df-ne 
 |-  ( I =/= ( ( # ` P ) - 2 ) <-> -. I = ( ( # ` P ) - 2 ) )
135 133 134 bitr2i 
 |-  ( -. I = ( ( # ` P ) - 2 ) <-> ( ( # ` P ) - 2 ) =/= I )
136 nn0re 
 |-  ( I e. NN0 -> I e. RR )
137 136 ad2antrr 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ I <_ ( ( # ` P ) - 2 ) ) -> I e. RR )
138 102 113 resubcld 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. RR )
139 138 ad2antlr 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ I <_ ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) - 2 ) e. RR )
140 simpr 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ I <_ ( ( # ` P ) - 2 ) ) -> I <_ ( ( # ` P ) - 2 ) )
141 leltne 
 |-  ( ( I e. RR /\ ( ( # ` P ) - 2 ) e. RR /\ I <_ ( ( # ` P ) - 2 ) ) -> ( I < ( ( # ` P ) - 2 ) <-> ( ( # ` P ) - 2 ) =/= I ) )
142 141 bicomd 
 |-  ( ( I e. RR /\ ( ( # ` P ) - 2 ) e. RR /\ I <_ ( ( # ` P ) - 2 ) ) -> ( ( ( # ` P ) - 2 ) =/= I <-> I < ( ( # ` P ) - 2 ) ) )
143 137 139 140 142 syl3anc 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ I <_ ( ( # ` P ) - 2 ) ) -> ( ( ( # ` P ) - 2 ) =/= I <-> I < ( ( # ` P ) - 2 ) ) )
144 143 biimpd 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ I <_ ( ( # ` P ) - 2 ) ) -> ( ( ( # ` P ) - 2 ) =/= I -> I < ( ( # ` P ) - 2 ) ) )
145 135 144 syl5bi 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ I <_ ( ( # ` P ) - 2 ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> I < ( ( # ` P ) - 2 ) ) )
146 145 ex 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( I <_ ( ( # ` P ) - 2 ) -> ( -. I = ( ( # ` P ) - 2 ) -> I < ( ( # ` P ) - 2 ) ) ) )
147 132 146 sylbid 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( I < ( ( # ` P ) - 1 ) -> ( -. I = ( ( # ` P ) - 2 ) -> I < ( ( # ` P ) - 2 ) ) ) )
148 147 com23 
 |-  ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( I < ( ( # ` P ) - 1 ) -> I < ( ( # ` P ) - 2 ) ) ) )
149 148 imp 
 |-  ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( I < ( ( # ` P ) - 1 ) -> I < ( ( # ` P ) - 2 ) ) )
150 149 adantr 
 |-  ( ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) /\ 2 < ( # ` P ) ) -> ( I < ( ( # ` P ) - 1 ) -> I < ( ( # ` P ) - 2 ) ) )
151 150 imp 
 |-  ( ( ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) /\ 2 < ( # ` P ) ) /\ I < ( ( # ` P ) - 1 ) ) -> I < ( ( # ` P ) - 2 ) )
152 107 118 151 3jca 
 |-  ( ( ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) /\ 2 < ( # ` P ) ) /\ I < ( ( # ` P ) - 1 ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) )
153 152 ex 
 |-  ( ( ( ( I e. NN0 /\ ( # ` P ) e. NN0 ) /\ -. I = ( ( # ` P ) - 2 ) ) /\ 2 < ( # ` P ) ) -> ( I < ( ( # ` P ) - 1 ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
154 153 exp41 
 |-  ( I e. NN0 -> ( ( # ` P ) e. NN0 -> ( -. I = ( ( # ` P ) - 2 ) -> ( 2 < ( # ` P ) -> ( I < ( ( # ` P ) - 1 ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) ) ) )
155 154 com25 
 |-  ( I e. NN0 -> ( I < ( ( # ` P ) - 1 ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( 2 < ( # ` P ) -> ( ( # ` P ) e. NN0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) ) ) )
156 155 imp 
 |-  ( ( I e. NN0 /\ I < ( ( # ` P ) - 1 ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( 2 < ( # ` P ) -> ( ( # ` P ) e. NN0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) ) )
157 156 3adant2 
 |-  ( ( I e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ I < ( ( # ` P ) - 1 ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( 2 < ( # ` P ) -> ( ( # ` P ) e. NN0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) ) )
158 106 157 sylbi 
 |-  ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( 2 < ( # ` P ) -> ( ( # ` P ) e. NN0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) ) )
159 158 imp 
 |-  ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( 2 < ( # ` P ) -> ( ( # ` P ) e. NN0 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) )
160 159 com13 
 |-  ( ( # ` P ) e. NN0 -> ( 2 < ( # ` P ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) )
161 160 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( 2 < ( # ` P ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) )
162 105 161 sylbird 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) =/= 2 -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) )
163 99 162 syl5bir 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( -. ( # ` P ) = 2 -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) )
164 163 com23 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( -. ( # ` P ) = 2 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) ) )
165 164 imp 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> ( -. ( # ` P ) = 2 -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
166 165 com12 
 |-  ( -. ( # ` P ) = 2 -> ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) ) )
167 98 166 pm2.61i 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) )
168 elfzo0 
 |-  ( I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) <-> ( I e. NN0 /\ ( ( # ` P ) - 2 ) e. NN /\ I < ( ( # ` P ) - 2 ) ) )
169 167 168 sylibr 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) )
170 80 169 jca 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) )
171 170 exp31 
 |-  ( ( # ` P ) e. NN0 -> ( 2 <_ ( # ` P ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) ) )
172 3 171 syl 
 |-  ( P e. Word V -> ( 2 <_ ( # ` P ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) ) )
173 172 imp 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) )
174 173 3adant1 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ -. I = ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) )
175 174 expd 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) ) )
176 175 com12 
 |-  ( I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) ) )
177 176 adantl 
 |-  ( ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) ) )
178 177 impcom 
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) )
179 178 adantr 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> ( -. I = ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) ) )
180 179 impcom 
 |-  ( ( -. I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) )
181 1 clwlkclwwlklem2fv1 
 |-  ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
182 180 181 syl 
 |-  ( ( -. I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
183 182 fveq2d 
 |-  ( ( -. I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( E ` ( F ` I ) ) = ( E ` ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )
184 simprr 
 |-  ( ( -. I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E )
185 f1ocnvfv2 
 |-  ( ( E : dom E -1-1-onto-> ran E /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> ( E ` ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
186 14 184 185 syl2an2 
 |-  ( ( -. I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( E ` ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
187 183 186 eqtrd 
 |-  ( ( -. I = ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) ) -> ( E ` ( F ` I ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
188 79 187 pm2.61ian 
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) /\ { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E ) -> ( E ` ( F ` I ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } )
189 188 exp31 
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E -> ( E ` ( F ` I ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )