Theorem wlkp1lem5

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

	Ref	Expression
Hypotheses	wlkp1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	wlkp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	wlkp1.f	$$⊢\phi \to \mathrm{Fun}I$$
	wlkp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
	wlkp1.b	$$⊢\phi \to B\in W$$
	wlkp1.c	$$⊢\phi \to C\in V$$
	wlkp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
	wlkp1.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
	wlkp1.n	$$⊢N=\left|F\right|$$
	wlkp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
	wlkp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
	wlkp1.u	$$⊢\phi \to \mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
	wlkp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
	wlkp1.q	$$⊢Q=P\cup \left\{⟨N+1,C⟩\right\}$$
	wlkp1.s	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
Assertion	wlkp1lem5	$$⊢\phi \to \forall k\in \left(0\dots N\right)Q\left(k\right)=P\left(k\right)$$

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		wlkp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		wlkp1.f	$$⊢\phi \to \mathrm{Fun}I$$
4		wlkp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
5		wlkp1.b	$$⊢\phi \to B\in W$$
6		wlkp1.c	$$⊢\phi \to C\in V$$
7		wlkp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
8		wlkp1.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
9		wlkp1.n	$$⊢N=\left|F\right|$$
10		wlkp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
11		wlkp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
12		wlkp1.u	$$⊢\phi \to \mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
13		wlkp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
14		wlkp1.q	$$⊢Q=P\cup \left\{⟨N+1,C⟩\right\}$$
15		wlkp1.s	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
16	14	fveq1i	$$⊢Q\left(k\right)=\left(P\cup \left\{⟨N+1,C⟩\right\}\right)\left(k\right)$$
17		fzp1nel	$$⊢\neg N+1\in \left(0\dots N\right)$$
18		eleq1	$$⊢k=N+1\to \left(k\in \left(0\dots N\right)\leftrightarrow N+1\in \left(0\dots N\right)\right)$$
19	18	notbid	$$⊢k=N+1\to \left(\neg k\in \left(0\dots N\right)\leftrightarrow \neg N+1\in \left(0\dots N\right)\right)$$
20	19	eqcoms	$$⊢N+1=k\to \left(\neg k\in \left(0\dots N\right)\leftrightarrow \neg N+1\in \left(0\dots N\right)\right)$$
21	17 20	mpbiri	$$⊢N+1=k\to \neg k\in \left(0\dots N\right)$$
22	21	a1i	$$⊢\phi \to \left(N+1=k\to \neg k\in \left(0\dots N\right)\right)$$
23	22	con2d	$$⊢\phi \to \left(k\in \left(0\dots N\right)\to \neg N+1=k\right)$$
24	23	imp	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to \neg N+1=k$$
25	24	neqned	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to N+1\ne k$$
26		fvunsn	$$⊢N+1\ne k\to \left(P\cup \left\{⟨N+1,C⟩\right\}\right)\left(k\right)=P\left(k\right)$$
27	25 26	syl	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to \left(P\cup \left\{⟨N+1,C⟩\right\}\right)\left(k\right)=P\left(k\right)$$
28	16 27	eqtrid	$$⊢\left(\phi \wedge k\in \left(0\dots N\right)\right)\to Q\left(k\right)=P\left(k\right)$$
29	28	ralrimiva	$$⊢\phi \to \forall k\in \left(0\dots N\right)Q\left(k\right)=P\left(k\right)$$