Theorem 1wlkdlem1

Description: Lemma 1 for 1wlkd . (Contributed by AV, 22-Jan-2021)

	Ref	Expression
Hypotheses	1wlkd.p	$$⊢P=⟨“XY”⟩$$
	1wlkd.f	$$⊢F=⟨“J”⟩$$
	1wlkd.x	$$⊢\phi \to X\in V$$
	1wlkd.y	$$⊢\phi \to Y\in V$$
Assertion	1wlkdlem1	$$⊢\phi \to P:\left(0\dots \left|F\right|\right)⟶V$$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$$⊢P=⟨“XY”⟩$$
2		1wlkd.f	$$⊢F=⟨“J”⟩$$
3		1wlkd.x	$$⊢\phi \to X\in V$$
4		1wlkd.y	$$⊢\phi \to Y\in V$$
5	3 4	s2cld	$$⊢\phi \to ⟨“XY”⟩\in \mathrm{Word}V$$
6		wrdf	$$⊢⟨“XY”⟩\in \mathrm{Word}V\to ⟨“XY”⟩:\left(0..^\left|⟨“XY”⟩\right|\right)⟶V$$
7		1z	$$⊢1\in \mathbb{Z}$$
8		fzval3	$$⊢1\in \mathbb{Z}\to \left(0\dots 1\right)=\left(0..^1+1\right)$$
9	7 8	ax-mp	$$⊢\left(0\dots 1\right)=\left(0..^1+1\right)$$
10	2	fveq2i	$$⊢\left|F\right|=\left|⟨“J”⟩\right|$$
11		s1len	$$⊢\left|⟨“J”⟩\right|=1$$
12	10 11	eqtri	$$⊢\left|F\right|=1$$
13	12	oveq2i	$$⊢\left(0\dots \left|F\right|\right)=\left(0\dots 1\right)$$
14		s2len	$$⊢\left|⟨“XY”⟩\right|=2$$
15		df-2	$$⊢2=1+1$$
16	14 15	eqtri	$$⊢\left|⟨“XY”⟩\right|=1+1$$
17	16	oveq2i	$$⊢\left(0..^\left|⟨“XY”⟩\right|\right)=\left(0..^1+1\right)$$
18	9 13 17	3eqtr4i	$$⊢\left(0\dots \left|F\right|\right)=\left(0..^\left|⟨“XY”⟩\right|\right)$$
19	18	a1i	$$⊢⟨“XY”⟩\in \mathrm{Word}V\to \left(0\dots \left|F\right|\right)=\left(0..^\left|⟨“XY”⟩\right|\right)$$
20	19	feq2d	$$⊢⟨“XY”⟩\in \mathrm{Word}V\to \left(⟨“XY”⟩:\left(0\dots \left|F\right|\right)⟶V\leftrightarrow ⟨“XY”⟩:\left(0..^\left|⟨“XY”⟩\right|\right)⟶V\right)$$
21	6 20	mpbird	$$⊢⟨“XY”⟩\in \mathrm{Word}V\to ⟨“XY”⟩:\left(0\dots \left|F\right|\right)⟶V$$
22	5 21	syl	$$⊢\phi \to ⟨“XY”⟩:\left(0\dots \left|F\right|\right)⟶V$$
23	1	feq1i	$$⊢P:\left(0\dots \left|F\right|\right)⟶V\leftrightarrow ⟨“XY”⟩:\left(0\dots \left|F\right|\right)⟶V$$
24	22 23	sylibr	$$⊢\phi \to P:\left(0\dots \left|F\right|\right)⟶V$$