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

Metamath Proof Explorer

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