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	eqtrid	|- ( ( 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	biimtrid	|- ( 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 ) ) ) )