Metamath Proof Explorer


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 φ X V
1wlkd.y φ Y V
Assertion 1wlkdlem1 φ P : 0 F V

Proof

Step Hyp Ref Expression
1 1wlkd.p P = ⟨“ XY ”⟩
2 1wlkd.f F = ⟨“ J ”⟩
3 1wlkd.x φ X V
4 1wlkd.y φ Y V
5 3 4 s2cld φ ⟨“ XY ”⟩ Word V
6 wrdf ⟨“ XY ”⟩ Word V ⟨“ XY ”⟩ : 0 ..^ ⟨“ XY ”⟩ V
7 1z 1
8 fzval3 1 0 1 = 0 ..^ 1 + 1
9 7 8 ax-mp 0 1 = 0 ..^ 1 + 1
10 2 fveq2i F = ⟨“ J ”⟩
11 s1len ⟨“ J ”⟩ = 1
12 10 11 eqtri F = 1
13 12 oveq2i 0 F = 0 1
14 s2len ⟨“ XY ”⟩ = 2
15 df-2 2 = 1 + 1
16 14 15 eqtri ⟨“ XY ”⟩ = 1 + 1
17 16 oveq2i 0 ..^ ⟨“ XY ”⟩ = 0 ..^ 1 + 1
18 9 13 17 3eqtr4i 0 F = 0 ..^ ⟨“ XY ”⟩
19 18 a1i ⟨“ XY ”⟩ Word V 0 F = 0 ..^ ⟨“ XY ”⟩
20 19 feq2d ⟨“ XY ”⟩ Word V ⟨“ XY ”⟩ : 0 F V ⟨“ XY ”⟩ : 0 ..^ ⟨“ XY ”⟩ V
21 6 20 mpbird ⟨“ XY ”⟩ Word V ⟨“ XY ”⟩ : 0 F V
22 5 21 syl φ ⟨“ XY ”⟩ : 0 F V
23 1 feq1i P : 0 F V ⟨“ XY ”⟩ : 0 F V
24 22 23 sylibr φ P : 0 F V