Metamath Proof Explorer

Theorem wlkres

Description: The restriction <. H , Q >. of a walk <. F , P >. to an initial segment of the walk (of length N ) forms a walk on the subgraph S consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 5-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses wlkres.v 
|- V = ( Vtx ` G )
wlkres.i 
|- I = ( iEdg ` G )
wlkres.d 
|- ( ph -> F ( Walks ` G ) P )
wlkres.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
wlkres.s 
|- ( ph -> ( Vtx ` S ) = V )
wlkres.e 
|- ( ph -> ( iEdg ` S ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
wlkres.h 
|- H = ( F prefix N )
wlkres.q 
|- Q = ( P |` ( 0 ... N ) )
Assertion wlkres 
|- ( ph -> H ( Walks ` S ) Q )

Proof

Step Hyp Ref Expression
1 wlkres.v 
 |-  V = ( Vtx ` G )
2 wlkres.i 
 |-  I = ( iEdg ` G )
3 wlkres.d 
 |-  ( ph -> F ( Walks ` G ) P )
4 wlkres.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 wlkres.s 
 |-  ( ph -> ( Vtx ` S ) = V )
6 wlkres.e 
 |-  ( ph -> ( iEdg ` S ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
7 wlkres.h 
 |-  H = ( F prefix N )
8 wlkres.q 
 |-  Q = ( P |` ( 0 ... N ) )
9 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
10 pfxwrdsymb 
 |-  ( F e. Word dom I -> ( F prefix N ) e. Word ( F " ( 0 ..^ N ) ) )
11 3 9 10 3syl 
 |-  ( ph -> ( F prefix N ) e. Word ( F " ( 0 ..^ N ) ) )
12 7 a1i 
 |-  ( ph -> H = ( F prefix N ) )
13 6 dmeqd 
 |-  ( ph -> dom ( iEdg ` S ) = dom ( I |` ( F " ( 0 ..^ N ) ) ) )
14 3 9 syl 
 |-  ( ph -> F e. Word dom I )
15 wrdf 
 |-  ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
16 fimass 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( F " ( 0 ..^ N ) ) C_ dom I )
17 14 15 16 3syl 
 |-  ( ph -> ( F " ( 0 ..^ N ) ) C_ dom I )
18 ssdmres 
 |-  ( ( F " ( 0 ..^ N ) ) C_ dom I <-> dom ( I |` ( F " ( 0 ..^ N ) ) ) = ( F " ( 0 ..^ N ) ) )
19 17 18 sylib 
 |-  ( ph -> dom ( I |` ( F " ( 0 ..^ N ) ) ) = ( F " ( 0 ..^ N ) ) )
20 13 19 eqtrd 
 |-  ( ph -> dom ( iEdg ` S ) = ( F " ( 0 ..^ N ) ) )
21 wrdeq 
 |-  ( dom ( iEdg ` S ) = ( F " ( 0 ..^ N ) ) -> Word dom ( iEdg ` S ) = Word ( F " ( 0 ..^ N ) ) )
22 20 21 syl 
 |-  ( ph -> Word dom ( iEdg ` S ) = Word ( F " ( 0 ..^ N ) ) )
23 11 12 22 3eltr4d 
 |-  ( ph -> H e. Word dom ( iEdg ` S ) )
24 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
25 3 24 syl 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
26 5 feq3d 
 |-  ( ph -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) <-> P : ( 0 ... ( # ` F ) ) --> V ) )
27 25 26 mpbird 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) )
28 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
29 28 4 sselid 
 |-  ( ph -> N e. ( 0 ... ( # ` F ) ) )
30 elfzuz3 
 |-  ( N e. ( 0 ... ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
31 fzss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... ( # ` F ) ) )
32 29 30 31 3syl 
 |-  ( ph -> ( 0 ... N ) C_ ( 0 ... ( # ` F ) ) )
33 27 32 fssresd 
 |-  ( ph -> ( P |` ( 0 ... N ) ) : ( 0 ... N ) --> ( Vtx ` S ) )
34 7 fveq2i 
 |-  ( # ` H ) = ( # ` ( F prefix N ) )
35 pfxlen 
 |-  ( ( F e. Word dom I /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = N )
36 14 29 35 syl2anc 
 |-  ( ph -> ( # ` ( F prefix N ) ) = N )
37 34 36 syl5eq 
 |-  ( ph -> ( # ` H ) = N )
38 37 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` H ) ) = ( 0 ... N ) )
39 38 feq2d 
 |-  ( ph -> ( ( P |` ( 0 ... N ) ) : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) <-> ( P |` ( 0 ... N ) ) : ( 0 ... N ) --> ( Vtx ` S ) ) )
40 33 39 mpbird 
 |-  ( ph -> ( P |` ( 0 ... N ) ) : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) )
41 8 feq1i 
 |-  ( Q : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) <-> ( P |` ( 0 ... N ) ) : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) )
42 40 41 sylibr 
 |-  ( ph -> Q : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) )
43 1 2 wlkprop 
 |-  ( F ( Walks ` G ) P -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
44 3 43 syl 
 |-  ( ph -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
45 44 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
46 37 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ N ) )
47 46 eleq2d 
 |-  ( ph -> ( x e. ( 0 ..^ ( # ` H ) ) <-> x e. ( 0 ..^ N ) ) )
48 8 fveq1i 
 |-  ( Q ` x ) = ( ( P |` ( 0 ... N ) ) ` x )
49 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
50 49 a1i 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ... N ) )
51 50 sselda 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> x e. ( 0 ... N ) )
52 51 fvresd 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( ( P |` ( 0 ... N ) ) ` x ) = ( P ` x ) )
53 48 52 eqtr2id 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( P ` x ) = ( Q ` x ) )
54 8 fveq1i 
 |-  ( Q ` ( x + 1 ) ) = ( ( P |` ( 0 ... N ) ) ` ( x + 1 ) )
55 fzofzp1 
 |-  ( x e. ( 0 ..^ N ) -> ( x + 1 ) e. ( 0 ... N ) )
56 55 adantl 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( x + 1 ) e. ( 0 ... N ) )
57 56 fvresd 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( ( P |` ( 0 ... N ) ) ` ( x + 1 ) ) = ( P ` ( x + 1 ) ) )
58 54 57 eqtr2id 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) )
59 53 58 jca 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) )
60 59 ex 
 |-  ( ph -> ( x e. ( 0 ..^ N ) -> ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) ) )
61 47 60 sylbid 
 |-  ( ph -> ( x e. ( 0 ..^ ( # ` H ) ) -> ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) ) )
62 61 imp 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) )
63 14 ancli 
 |-  ( ph -> ( ph /\ F e. Word dom I ) )
64 15 ffund 
 |-  ( F e. Word dom I -> Fun F )
65 64 adantl 
 |-  ( ( ph /\ F e. Word dom I ) -> Fun F )
66 65 adantr 
 |-  ( ( ( ph /\ F e. Word dom I ) /\ x e. ( 0 ..^ N ) ) -> Fun F )
67 fdm 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
68 elfzouz2 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
69 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
70 4 68 69 3syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
71 sseq2 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( ( 0 ..^ N ) C_ dom F <-> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) ) )
72 70 71 syl5ibr 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( ph -> ( 0 ..^ N ) C_ dom F ) )
73 15 67 72 3syl 
 |-  ( F e. Word dom I -> ( ph -> ( 0 ..^ N ) C_ dom F ) )
74 73 impcom 
 |-  ( ( ph /\ F e. Word dom I ) -> ( 0 ..^ N ) C_ dom F )
75 74 adantr 
 |-  ( ( ( ph /\ F e. Word dom I ) /\ x e. ( 0 ..^ N ) ) -> ( 0 ..^ N ) C_ dom F )
76 simpr 
 |-  ( ( ( ph /\ F e. Word dom I ) /\ x e. ( 0 ..^ N ) ) -> x e. ( 0 ..^ N ) )
77 66 75 76 resfvresima 
 |-  ( ( ( ph /\ F e. Word dom I ) /\ x e. ( 0 ..^ N ) ) -> ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) = ( I ` ( F ` x ) ) )
78 63 77 sylan 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) = ( I ` ( F ` x ) ) )
79 78 eqcomd 
 |-  ( ( ph /\ x e. ( 0 ..^ N ) ) -> ( I ` ( F ` x ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) )
80 79 ex 
 |-  ( ph -> ( x e. ( 0 ..^ N ) -> ( I ` ( F ` x ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) ) )
81 47 80 sylbid 
 |-  ( ph -> ( x e. ( 0 ..^ ( # ` H ) ) -> ( I ` ( F ` x ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) ) )
82 81 imp 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( I ` ( F ` x ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) )
83 6 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( iEdg ` S ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
84 7 fveq1i 
 |-  ( H ` x ) = ( ( F prefix N ) ` x )
85 14 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> F e. Word dom I )
86 29 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> N e. ( 0 ... ( # ` F ) ) )
87 pfxres 
 |-  ( ( F e. Word dom I /\ N e. ( 0 ... ( # ` F ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) )
88 85 86 87 syl2anc 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) )
89 88 fveq1d 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( ( F prefix N ) ` x ) = ( ( F |` ( 0 ..^ N ) ) ` x ) )
90 84 89 syl5eq 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( H ` x ) = ( ( F |` ( 0 ..^ N ) ) ` x ) )
91 83 90 fveq12d 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( ( iEdg ` S ) ` ( H ` x ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) ` ( ( F |` ( 0 ..^ N ) ) ` x ) ) )
92 82 91 eqtr4d 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) )
93 62 92 jca 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) )
94 4 68 syl 
 |-  ( ph -> ( # ` F ) e. ( ZZ>= ` N ) )
95 37 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( # ` H ) ) = ( ZZ>= ` N ) )
96 94 95 eleqtrrd 
 |-  ( ph -> ( # ` F ) e. ( ZZ>= ` ( # ` H ) ) )
97 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( # ` H ) ) -> ( 0 ..^ ( # ` H ) ) C_ ( 0 ..^ ( # ` F ) ) )
98 96 97 syl 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) C_ ( 0 ..^ ( # ` F ) ) )
99 98 sselda 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> x e. ( 0 ..^ ( # ` F ) ) )
100 wkslem1 
 |-  ( k = x -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( I ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( I ` ( F ` x ) ) ) ) )
101 100 rspcv 
 |-  ( x e. ( 0 ..^ ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( I ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( I ` ( F ` x ) ) ) ) )
102 99 101 syl 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( I ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( I ` ( F ` x ) ) ) ) )
103 eqeq12 
 |-  ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) -> ( ( P ` x ) = ( P ` ( x + 1 ) ) <-> ( Q ` x ) = ( Q ` ( x + 1 ) ) ) )
104 103 adantr 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> ( ( P ` x ) = ( P ` ( x + 1 ) ) <-> ( Q ` x ) = ( Q ` ( x + 1 ) ) ) )
105 simpr 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) )
106 sneq 
 |-  ( ( P ` x ) = ( Q ` x ) -> { ( P ` x ) } = { ( Q ` x ) } )
107 106 adantr 
 |-  ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) -> { ( P ` x ) } = { ( Q ` x ) } )
108 107 adantr 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> { ( P ` x ) } = { ( Q ` x ) } )
109 105 108 eqeq12d 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> ( ( I ` ( F ` x ) ) = { ( P ` x ) } <-> ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } ) )
110 preq12 
 |-  ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( Q ` x ) , ( Q ` ( x + 1 ) ) } )
111 110 adantr 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( Q ` x ) , ( Q ` ( x + 1 ) ) } )
112 111 105 sseq12d 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> ( { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( I ` ( F ` x ) ) <-> { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) )
113 104 109 112 ifpbi123d 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> ( if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( I ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( I ` ( F ` x ) ) ) <-> if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) )
114 113 biimpd 
 |-  ( ( ( ( P ` x ) = ( Q ` x ) /\ ( P ` ( x + 1 ) ) = ( Q ` ( x + 1 ) ) ) /\ ( I ` ( F ` x ) ) = ( ( iEdg ` S ) ` ( H ` x ) ) ) -> ( if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( I ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( I ` ( F ` x ) ) ) -> if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) )
115 93 102 114 sylsyld 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) )
116 115 com12 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) )
117 116 3ad2ant3 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) )
118 45 117 mpcom 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` H ) ) ) -> if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) )
119 118 ralrimiva 
 |-  ( ph -> A. x e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) )
120 1 2 3 4 5 wlkreslem 
 |-  ( ph -> S e. _V )
121 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
122 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
123 121 122 iswlkg 
 |-  ( S e. _V -> ( H ( Walks ` S ) Q <-> ( H e. Word dom ( iEdg ` S ) /\ Q : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) /\ A. x e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) ) )
124 120 123 syl 
 |-  ( ph -> ( H ( Walks ` S ) Q <-> ( H e. Word dom ( iEdg ` S ) /\ Q : ( 0 ... ( # ` H ) ) --> ( Vtx ` S ) /\ A. x e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` x ) = ( Q ` ( x + 1 ) ) , ( ( iEdg ` S ) ` ( H ` x ) ) = { ( Q ` x ) } , { ( Q ` x ) , ( Q ` ( x + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` x ) ) ) ) ) )
125 23 42 119 124 mpbir3and 
 |-  ( ph -> H ( Walks ` S ) Q )