Theorem wlkdlem1

Description: Lemma 1 for wlkd . (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
	wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
	wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
	wlkdlem1.v	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
Assertion	wlkdlem1	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
2		wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
3		wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
4		wlkdlem1.v	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
5		wrdf	⊢ ( 𝑃 ∈ Word V → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V )
6	1 5	syl	⊢ ( 𝜑 → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V )
7	3	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
8		lencl	⊢ ( 𝐹 ∈ Word V → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
9	2 8	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
10	9	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
11		fzval3	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
12	10 11	syl	⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
13	7 12	eqtr4d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
14	13	feq2d	⊢ ( 𝜑 → ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ V ) )
15		ssv	⊢ 𝑉 ⊆ V
16		frnssb	⊢ ( ( 𝑉 ⊆ V ∧ ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ V ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
17	15 4 16	sylancr	⊢ ( 𝜑 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ V ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
18	14 17	bitrd	⊢ ( 𝜑 → ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
19	6 18	mpbid	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )