Metamath Proof Explorer

Theorem pfx2

Description: A prefix of length two. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion pfx2 ⊢ W ∈ Word V ∧ 2 ≤ W → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ 0
2 1 a1i ⊢ W ∈ Word V ∧ 2 ≤ W → 2 ∈ ℕ 0
3 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
4 3 adantr ⊢ W ∈ Word V ∧ 2 ≤ W → W ∈ ℕ 0
5 simpr ⊢ W ∈ Word V ∧ 2 ≤ W → 2 ≤ W
6 elfz2nn0 ⊢ 2 ∈ 0 … W ↔ 2 ∈ ℕ 0 ∧ W ∈ ℕ 0 ∧ 2 ≤ W
7 2 4 5 6 syl3anbrc ⊢ W ∈ Word V ∧ 2 ≤ W → 2 ∈ 0 … W
8 pfxlen ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 = 2
9 s2len ⊢ ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ = 2
10 9 eqcomi ⊢ 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩
11 10 a1i ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩
12 2nn ⊢ 2 ∈ ℕ
13 lbfzo0 ⊢ 0 ∈ 0 ..^ 2 ↔ 2 ∈ ℕ
14 12 13 mpbir ⊢ 0 ∈ 0 ..^ 2
15 pfxfv ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ 0 ∈ 0 ..^ 2 → W prefix 2 ⁡ 0 = W ⁡ 0
16 14 15 mp3an3 ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 ⁡ 0 = W ⁡ 0
17 16 adantr ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → W prefix 2 ⁡ 0 = W ⁡ 0
18 fvex ⊢ W ⁡ 0 ∈ V
19 s2fv0 ⊢ W ⁡ 0 ∈ V → ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0 = W ⁡ 0
20 18 19 ax-mp ⊢ ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0 = W ⁡ 0
21 17 20 eqtr4di ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → W prefix 2 ⁡ 0 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0
22 1nn0 ⊢ 1 ∈ ℕ 0
23 1lt2 ⊢ 1 < 2
24 elfzo0 ⊢ 1 ∈ 0 ..^ 2 ↔ 1 ∈ ℕ 0 ∧ 2 ∈ ℕ ∧ 1 < 2
25 22 12 23 24 mpbir3an ⊢ 1 ∈ 0 ..^ 2
26 pfxfv ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ 1 ∈ 0 ..^ 2 → W prefix 2 ⁡ 1 = W ⁡ 1
27 25 26 mp3an3 ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 ⁡ 1 = W ⁡ 1
28 fvex ⊢ W ⁡ 1 ∈ V
29 s2fv1 ⊢ W ⁡ 1 ∈ V → ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1 = W ⁡ 1
30 28 29 ax-mp ⊢ ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1 = W ⁡ 1
31 27 30 eqtr4di ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 ⁡ 1 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1
32 31 adantr ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → W prefix 2 ⁡ 1 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1
33 0nn0 ⊢ 0 ∈ ℕ 0
34 fveq2 ⊢ i = 0 → W prefix 2 ⁡ i = W prefix 2 ⁡ 0
35 fveq2 ⊢ i = 0 → ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0
36 34 35 eqeq12d ⊢ i = 0 → W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ W prefix 2 ⁡ 0 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0
37 fveq2 ⊢ i = 1 → W prefix 2 ⁡ i = W prefix 2 ⁡ 1
38 fveq2 ⊢ i = 1 → ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1
39 37 38 eqeq12d ⊢ i = 1 → W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ W prefix 2 ⁡ 1 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1
40 36 39 ralprg ⊢ 0 ∈ ℕ 0 ∧ 1 ∈ ℕ 0 → ∀ i ∈ 0 1 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ W prefix 2 ⁡ 0 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0 ∧ W prefix 2 ⁡ 1 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1
41 33 22 40 mp2an ⊢ ∀ i ∈ 0 1 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ W prefix 2 ⁡ 0 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 0 ∧ W prefix 2 ⁡ 1 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ 1
42 21 32 41 sylanbrc ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → ∀ i ∈ 0 1 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
43 eqeq1 ⊢ W prefix 2 = 2 → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ↔ 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩
44 oveq2 ⊢ W prefix 2 = 2 → 0 ..^ W prefix 2 = 0 ..^ 2
45 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
46 44 45 eqtrdi ⊢ W prefix 2 = 2 → 0 ..^ W prefix 2 = 0 1
47 46 raleqdv ⊢ W prefix 2 = 2 → ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ ∀ i ∈ 0 1 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
48 43 47 anbi12d ⊢ W prefix 2 = 2 → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 1 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
49 48 adantl ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i ↔ 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 1 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
50 11 42 49 mpbir2and ⊢ W ∈ Word V ∧ 2 ∈ 0 … W ∧ W prefix 2 = 2 → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
51 8 50 mpdan ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
52 pfxcl ⊢ W ∈ Word V → W prefix 2 ∈ Word V
53 s2cli ⊢ ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∈ Word V
54 eqwrd ⊢ W prefix 2 ∈ Word V ∧ ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∈ Word V → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ↔ W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
55 52 53 54 sylancl ⊢ W ∈ Word V → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ↔ W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
56 55 adantr ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ↔ W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ∧ ∀ i ∈ 0 ..^ W prefix 2 W prefix 2 ⁡ i = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩ ⁡ i
57 51 56 mpbird ⊢ W ∈ Word V ∧ 2 ∈ 0 … W → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩
58 7 57 syldan ⊢ W ∈ Word V ∧ 2 ≤ W → W prefix 2 = ⟨“ W ⁡ 0 W ⁡ 1 ”⟩