This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 fcdmssb ⊢ ( ( 𝑉 ⊆ 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 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )