Theorem wlk2v2elem2

Description: Lemma 2 for wlk2v2e : The values of I after F are edges between two vertices enumerated by P . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)

	Ref	Expression
Hypotheses	wlk2v2e.i	$$⊢I=⟨“\left\{X,Y\right\}”⟩$$
	wlk2v2e.f	$$⊢F=⟨“00”⟩$$
	wlk2v2e.x	$$⊢X\in \mathrm{V}$$
	wlk2v2e.y	$$⊢Y\in \mathrm{V}$$
	wlk2v2e.p	$$⊢P=⟨“XYX”⟩$$
Assertion	wlk2v2elem2	$$⊢\forall k\in \left(0..^\left|F\right|\right)I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		wlk2v2e.i	$$⊢I=⟨“\left\{X,Y\right\}”⟩$$
2		wlk2v2e.f	$$⊢F=⟨“00”⟩$$
3		wlk2v2e.x	$$⊢X\in \mathrm{V}$$
4		wlk2v2e.y	$$⊢Y\in \mathrm{V}$$
5		wlk2v2e.p	$$⊢P=⟨“XYX”⟩$$
6	2	fveq1i	$$⊢F\left(0\right)=⟨“00”⟩\left(0\right)$$
7		0z	$$⊢0\in \mathbb{Z}$$
8		s2fv0	$$⊢0\in \mathbb{Z}\to ⟨“00”⟩\left(0\right)=0$$
9	7 8	ax-mp	$$⊢⟨“00”⟩\left(0\right)=0$$
10	6 9	eqtri	$$⊢F\left(0\right)=0$$
11	10	fveq2i	$$⊢I\left(F\left(0\right)\right)=I\left(0\right)$$
12	1	fveq1i	$$⊢I\left(0\right)=⟨“\left\{X,Y\right\}”⟩\left(0\right)$$
13		prex	$$⊢\left\{X,Y\right\}\in \mathrm{V}$$
14		s1fv	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to ⟨“\left\{X,Y\right\}”⟩\left(0\right)=\left\{X,Y\right\}$$
15	13 14	ax-mp	$$⊢⟨“\left\{X,Y\right\}”⟩\left(0\right)=\left\{X,Y\right\}$$
16	12 15	eqtri	$$⊢I\left(0\right)=\left\{X,Y\right\}$$
17	5	fveq1i	$$⊢P\left(0\right)=⟨“XYX”⟩\left(0\right)$$
18		s3fv0	$$⊢X\in \mathrm{V}\to ⟨“XYX”⟩\left(0\right)=X$$
19	3 18	ax-mp	$$⊢⟨“XYX”⟩\left(0\right)=X$$
20	17 19	eqtri	$$⊢P\left(0\right)=X$$
21	5	fveq1i	$$⊢P\left(1\right)=⟨“XYX”⟩\left(1\right)$$
22		s3fv1	$$⊢Y\in \mathrm{V}\to ⟨“XYX”⟩\left(1\right)=Y$$
23	4 22	ax-mp	$$⊢⟨“XYX”⟩\left(1\right)=Y$$
24	21 23	eqtri	$$⊢P\left(1\right)=Y$$
25	20 24	preq12i	$$⊢\left\{P\left(0\right),P\left(1\right)\right\}=\left\{X,Y\right\}$$
26	25	eqcomi	$$⊢\left\{X,Y\right\}=\left\{P\left(0\right),P\left(1\right)\right\}$$
27	11 16 26	3eqtri	$$⊢I\left(F\left(0\right)\right)=\left\{P\left(0\right),P\left(1\right)\right\}$$
28	2	fveq1i	$$⊢F\left(1\right)=⟨“00”⟩\left(1\right)$$
29		s2fv1	$$⊢0\in \mathbb{Z}\to ⟨“00”⟩\left(1\right)=0$$
30	7 29	ax-mp	$$⊢⟨“00”⟩\left(1\right)=0$$
31	28 30	eqtri	$$⊢F\left(1\right)=0$$
32	31	fveq2i	$$⊢I\left(F\left(1\right)\right)=I\left(0\right)$$
33		prcom	$$⊢\left\{X,Y\right\}=\left\{Y,X\right\}$$
34	5	fveq1i	$$⊢P\left(2\right)=⟨“XYX”⟩\left(2\right)$$
35		s3fv2	$$⊢X\in \mathrm{V}\to ⟨“XYX”⟩\left(2\right)=X$$
36	3 35	ax-mp	$$⊢⟨“XYX”⟩\left(2\right)=X$$
37	34 36	eqtri	$$⊢P\left(2\right)=X$$
38	24 37	preq12i	$$⊢\left\{P\left(1\right),P\left(2\right)\right\}=\left\{Y,X\right\}$$
39	38	eqcomi	$$⊢\left\{Y,X\right\}=\left\{P\left(1\right),P\left(2\right)\right\}$$
40	33 39	eqtri	$$⊢\left\{X,Y\right\}=\left\{P\left(1\right),P\left(2\right)\right\}$$
41	32 16 40	3eqtri	$$⊢I\left(F\left(1\right)\right)=\left\{P\left(1\right),P\left(2\right)\right\}$$
42		2wlklem	$$⊢\forall k\in \left\{0,1\right\}I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow \left(I\left(F\left(0\right)\right)=\left\{P\left(0\right),P\left(1\right)\right\}\wedge I\left(F\left(1\right)\right)=\left\{P\left(1\right),P\left(2\right)\right\}\right)$$
43	27 41 42	mpbir2an	$$⊢\forall k\in \left\{0,1\right\}I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}$$
44	5 2	2wlkdlem2	$$⊢\left(0..^\left|F\right|\right)=\left\{0,1\right\}$$
45	44	raleqi	$$⊢\forall k\in \left(0..^\left|F\right|\right)I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow \forall k\in \left\{0,1\right\}I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}$$
46	43 45	mpbir	$$⊢\forall k\in \left(0..^\left|F\right|\right)I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}$$