Metamath Proof Explorer

Theorem chnerlem2

Description: Lemma for chner where the I-th element comes before the J-th. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses chner.1 ⊢ φ → ∼ ˙ Er A
chner.2 ⊢ φ → C ∈ Chain A ∼ ˙
chner.3 ⊢ φ → J ∈ 0 ..^ C
Assertion chnerlem2 ⊢ φ ∧ I ∈ 0 ..^ J → C ⁡ I ∼ ˙ C ⁡ J

Proof

Step Hyp Ref Expression
1 chner.1 ⊢ φ → ∼ ˙ Er A
2 chner.2 ⊢ φ → C ∈ Chain A ∼ ˙
3 chner.3 ⊢ φ → J ∈ 0 ..^ C
4 1 adantr ⊢ φ ∧ I ∈ 0 ..^ J → ∼ ˙ Er A
5 2 adantr ⊢ φ ∧ I ∈ 0 ..^ J → C ∈ Chain A ∼ ˙
6 3 adantr ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ 0 ..^ C
7 fzofzp1 ⊢ J ∈ 0 ..^ C → J + 1 ∈ 0 … C
8 6 7 syl ⊢ φ ∧ I ∈ 0 ..^ J → J + 1 ∈ 0 … C
9 5 8 pfxchn ⊢ φ ∧ I ∈ 0 ..^ J → C prefix J + 1 ∈ Chain A ∼ ˙
10 simpl ⊢ φ ∧ I ∈ 0 ..^ J → φ
11 animorrl ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ J ∨ I = J
12 elfzonn0 ⊢ J ∈ 0 ..^ C → J ∈ ℕ 0
13 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
14 13 eleq2i ⊢ J ∈ ℕ 0 ↔ J ∈ ℤ ≥ 0
15 14 biimpi ⊢ J ∈ ℕ 0 → J ∈ ℤ ≥ 0
16 3 12 15 3syl ⊢ φ → J ∈ ℤ ≥ 0
17 16 adantr ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ ℤ ≥ 0
18 fzosplitsni ⊢ J ∈ ℤ ≥ 0 → I ∈ 0 ..^ J + 1 ↔ I ∈ 0 ..^ J ∨ I = J
19 17 18 syl ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ J + 1 ↔ I ∈ 0 ..^ J ∨ I = J
20 11 19 mpbird ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ J + 1
21 10 20 jca ⊢ φ ∧ I ∈ 0 ..^ J → φ ∧ I ∈ 0 ..^ J + 1
22 simpr ⊢ φ ∧ I ∈ 0 ..^ J + 1 → I ∈ 0 ..^ J + 1
23 2 chnwrd ⊢ φ → C ∈ Word A
24 23 adantr ⊢ φ ∧ I ∈ 0 ..^ J + 1 → C ∈ Word A
25 3 7 syl ⊢ φ → J + 1 ∈ 0 … C
26 25 adantr ⊢ φ ∧ I ∈ 0 ..^ J + 1 → J + 1 ∈ 0 … C
27 pfxlen ⊢ C ∈ Word A ∧ J + 1 ∈ 0 … C → C prefix J + 1 = J + 1
28 24 26 27 syl2anc ⊢ φ ∧ I ∈ 0 ..^ J + 1 → C prefix J + 1 = J + 1
29 28 oveq2d ⊢ φ ∧ I ∈ 0 ..^ J + 1 → 0 ..^ C prefix J + 1 = 0 ..^ J + 1
30 22 29 eleqtrrd ⊢ φ ∧ I ∈ 0 ..^ J + 1 → I ∈ 0 ..^ C prefix J + 1
31 21 30 syl ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ C prefix J + 1
32 4 9 31 chnerlem1 ⊢ φ ∧ I ∈ 0 ..^ J → C prefix J + 1 ⁡ I ∼ ˙ lastS ⁡ C prefix J + 1
33 23 adantr ⊢ φ ∧ I ∈ 0 ..^ J → C ∈ Word A
34 pfxfv ⊢ C ∈ Word A ∧ J + 1 ∈ 0 … C ∧ I ∈ 0 ..^ J + 1 → C prefix J + 1 ⁡ I = C ⁡ I
35 33 8 20 34 syl3anc ⊢ φ ∧ I ∈ 0 ..^ J → C prefix J + 1 ⁡ I = C ⁡ I
36 lencl ⊢ C ∈ Word A → C ∈ ℕ 0
37 23 36 syl ⊢ φ → C ∈ ℕ 0
38 fz0add1fz1 ⊢ C ∈ ℕ 0 ∧ J ∈ 0 ..^ C → J + 1 ∈ 1 … C
39 37 3 38 syl2anc ⊢ φ → J + 1 ∈ 1 … C
40 39 adantr ⊢ φ ∧ I ∈ 0 ..^ J → J + 1 ∈ 1 … C
41 pfxfvlsw ⊢ C ∈ Word A ∧ J + 1 ∈ 1 … C → lastS ⁡ C prefix J + 1 = C ⁡ J + 1 - 1
42 33 40 41 syl2anc ⊢ φ ∧ I ∈ 0 ..^ J → lastS ⁡ C prefix J + 1 = C ⁡ J + 1 - 1
43 elfzoel2 ⊢ I ∈ 0 ..^ J → J ∈ ℤ
44 43 adantl ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ ℤ
45 44 zcnd ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ ℂ
46 1cnd ⊢ φ ∧ I ∈ 0 ..^ J → 1 ∈ ℂ
47 45 46 pncand ⊢ φ ∧ I ∈ 0 ..^ J → J + 1 - 1 = J
48 47 fveq2d ⊢ φ ∧ I ∈ 0 ..^ J → C ⁡ J + 1 - 1 = C ⁡ J
49 42 48 eqtrd ⊢ φ ∧ I ∈ 0 ..^ J → lastS ⁡ C prefix J + 1 = C ⁡ J
50 32 35 49 3brtr3d ⊢ φ ∧ I ∈ 0 ..^ J → C ⁡ I ∼ ˙ C ⁡ J