Theorem 1wlkdlem1

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

	Ref	Expression
Hypotheses	1wlkd.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
	1wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 ”⟩
	1wlkd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	1wlkd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	1wlkdlem1	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2		1wlkd.f	⊢ 𝐹 = ⟨“ 𝐽 ”⟩
3		1wlkd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4		1wlkd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5	3 4	s2cld	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 )
6		wrdf	⊢ ( ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 → ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) ) ⟶ 𝑉 )
7		1z	⊢ 1 ∈ ℤ
8		fzval3	⊢ ( 1 ∈ ℤ → ( 0 ... 1 ) = ( 0 ..^ ( 1 + 1 ) ) )
9	7 8	ax-mp	⊢ ( 0 ... 1 ) = ( 0 ..^ ( 1 + 1 ) )
10	2	fveq2i	⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 ”⟩ )
11		s1len	⊢ ( ♯ ‘ ⟨“ 𝐽 ”⟩ ) = 1
12	10 11	eqtri	⊢ ( ♯ ‘ 𝐹 ) = 1
13	12	oveq2i	⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 1 )
14		s2len	⊢ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = 2
15		df-2	⊢ 2 = ( 1 + 1 )
16	14 15	eqtri	⊢ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) = ( 1 + 1 )
17	16	oveq2i	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) ) = ( 0 ..^ ( 1 + 1 ) )
18	9 13 17	3eqtr4i	⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) )
19	18	a1i	⊢ ( ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) ) )
20	19	feq2d	⊢ ( ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 → ( ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑋 𝑌 ”⟩ ) ) ⟶ 𝑉 ) )
21	6 20	mpbird	⊢ ( ⟨“ 𝑋 𝑌 ”⟩ ∈ Word 𝑉 → ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
22	5 21	syl	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
23	1	feq1i	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ ⟨“ 𝑋 𝑌 ”⟩ : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
24	22 23	sylibr	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )