Metamath Proof Explorer

Theorem wlkp1lem6

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v 
|- V = ( Vtx ` G )
wlkp1.i 
|- I = ( iEdg ` G )
wlkp1.f 
|- ( ph -> Fun I )
wlkp1.a 
|- ( ph -> I e. Fin )
wlkp1.b 
|- ( ph -> B e. W )
wlkp1.c 
|- ( ph -> C e. V )
wlkp1.d 
|- ( ph -> -. B e. dom I )
wlkp1.w 
|- ( ph -> F ( Walks ` G ) P )
wlkp1.n 
|- N = ( # ` F )
wlkp1.e 
|- ( ph -> E e. ( Edg ` G ) )
wlkp1.x 
|- ( ph -> { ( P ` N ) , C } C_ E )
wlkp1.u 
|- ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
wlkp1.h 
|- H = ( F u. { <. N , B >. } )
wlkp1.q 
|- Q = ( P u. { <. ( N + 1 ) , C >. } )
wlkp1.s 
|- ( ph -> ( Vtx ` S ) = V )
Assertion wlkp1lem6 
|- ( ph -> A. k e. ( 0 ..^ N ) ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v 
 |-  V = ( Vtx ` G )
2 wlkp1.i 
 |-  I = ( iEdg ` G )
3 wlkp1.f 
 |-  ( ph -> Fun I )
4 wlkp1.a 
 |-  ( ph -> I e. Fin )
5 wlkp1.b 
 |-  ( ph -> B e. W )
6 wlkp1.c 
 |-  ( ph -> C e. V )
7 wlkp1.d 
 |-  ( ph -> -. B e. dom I )
8 wlkp1.w 
 |-  ( ph -> F ( Walks ` G ) P )
9 wlkp1.n 
 |-  N = ( # ` F )
10 wlkp1.e 
 |-  ( ph -> E e. ( Edg ` G ) )
11 wlkp1.x 
 |-  ( ph -> { ( P ` N ) , C } C_ E )
12 wlkp1.u 
 |-  ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
13 wlkp1.h 
 |-  H = ( F u. { <. N , B >. } )
14 wlkp1.q 
 |-  Q = ( P u. { <. ( N + 1 ) , C >. } )
15 wlkp1.s 
 |-  ( ph -> ( Vtx ` S ) = V )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 
 |-  ( ph -> A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) )
17 elfzofz 
 |-  ( k e. ( 0 ..^ N ) -> k e. ( 0 ... N ) )
18 17 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ... N ) )
19 fveq2 
 |-  ( x = k -> ( Q ` x ) = ( Q ` k ) )
20 fveq2 
 |-  ( x = k -> ( P ` x ) = ( P ` k ) )
21 19 20 eqeq12d 
 |-  ( x = k -> ( ( Q ` x ) = ( P ` x ) <-> ( Q ` k ) = ( P ` k ) ) )
22 21 rspcv 
 |-  ( k e. ( 0 ... N ) -> ( A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) -> ( Q ` k ) = ( P ` k ) ) )
23 18 22 syl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) -> ( Q ` k ) = ( P ` k ) ) )
24 23 imp 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) ) -> ( Q ` k ) = ( P ` k ) )
25 fzofzp1 
 |-  ( k e. ( 0 ..^ N ) -> ( k + 1 ) e. ( 0 ... N ) )
26 25 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 0 ... N ) )
27 fveq2 
 |-  ( x = ( k + 1 ) -> ( Q ` x ) = ( Q ` ( k + 1 ) ) )
28 fveq2 
 |-  ( x = ( k + 1 ) -> ( P ` x ) = ( P ` ( k + 1 ) ) )
29 27 28 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( ( Q ` x ) = ( P ` x ) <-> ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) ) )
30 29 rspcv 
 |-  ( ( k + 1 ) e. ( 0 ... N ) -> ( A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) -> ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) ) )
31 26 30 syl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) -> ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) ) )
32 31 imp 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) ) -> ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) )
33 12 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
34 13 fveq1i 
 |-  ( H ` k ) = ( ( F u. { <. N , B >. } ) ` k )
35 fzonel 
 |-  -. N e. ( 0 ..^ N )
36 eleq1 
 |-  ( N = k -> ( N e. ( 0 ..^ N ) <-> k e. ( 0 ..^ N ) ) )
37 35 36 mtbii 
 |-  ( N = k -> -. k e. ( 0 ..^ N ) )
38 37 a1i 
 |-  ( ph -> ( N = k -> -. k e. ( 0 ..^ N ) ) )
39 38 con2d 
 |-  ( ph -> ( k e. ( 0 ..^ N ) -> -. N = k ) )
40 39 imp 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> -. N = k )
41 40 neqned 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> N =/= k )
42 fvunsn 
 |-  ( N =/= k -> ( ( F u. { <. N , B >. } ) ` k ) = ( F ` k ) )
43 41 42 syl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( F u. { <. N , B >. } ) ` k ) = ( F ` k ) )
44 34 43 syl5eq 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( H ` k ) = ( F ` k ) )
45 33 44 fveq12d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( iEdg ` S ) ` ( H ` k ) ) = ( ( I u. { <. B , E >. } ) ` ( F ` k ) ) )
46 9 oveq2i 
 |-  ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) )
47 46 eleq2i 
 |-  ( k e. ( 0 ..^ N ) <-> k e. ( 0 ..^ ( # ` F ) ) )
48 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
49 8 48 syl 
 |-  ( ph -> F e. Word dom I )
50 wrdsymbcl 
 |-  ( ( F e. Word dom I /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` k ) e. dom I )
51 50 ex 
 |-  ( F e. Word dom I -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( F ` k ) e. dom I ) )
52 49 51 syl 
 |-  ( ph -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( F ` k ) e. dom I ) )
53 47 52 syl5bi 
 |-  ( ph -> ( k e. ( 0 ..^ N ) -> ( F ` k ) e. dom I ) )
54 53 imp 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( F ` k ) e. dom I )
55 eleq1 
 |-  ( B = ( F ` k ) -> ( B e. dom I <-> ( F ` k ) e. dom I ) )
56 54 55 syl5ibrcom 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( B = ( F ` k ) -> B e. dom I ) )
57 56 con3d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( -. B e. dom I -> -. B = ( F ` k ) ) )
58 57 ex 
 |-  ( ph -> ( k e. ( 0 ..^ N ) -> ( -. B e. dom I -> -. B = ( F ` k ) ) ) )
59 7 58 mpid 
 |-  ( ph -> ( k e. ( 0 ..^ N ) -> -. B = ( F ` k ) ) )
60 59 imp 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> -. B = ( F ` k ) )
61 60 neqned 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> B =/= ( F ` k ) )
62 fvunsn 
 |-  ( B =/= ( F ` k ) -> ( ( I u. { <. B , E >. } ) ` ( F ` k ) ) = ( I ` ( F ` k ) ) )
63 61 62 syl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( I u. { <. B , E >. } ) ` ( F ` k ) ) = ( I ` ( F ` k ) ) )
64 45 63 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) )
65 64 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) ) -> ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) )
66 24 32 65 3jca 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) ) -> ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) )
67 16 66 mpidan 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) )
68 67 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ..^ N ) ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) )