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 animorrl ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ J ∨ I = J
11 elfzonn0 ⊢ J ∈ 0 ..^ C → J ∈ ℕ 0
12 elnn0uz ⊢ J ∈ ℕ 0 ↔ J ∈ ℤ ≥ 0
13 12 biimpi ⊢ J ∈ ℕ 0 → J ∈ ℤ ≥ 0
14 3 11 13 3syl ⊢ φ → J ∈ ℤ ≥ 0
15 14 adantr ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ ℤ ≥ 0
16 fzosplitsni ⊢ J ∈ ℤ ≥ 0 → I ∈ 0 ..^ J + 1 ↔ I ∈ 0 ..^ J ∨ I = J
17 15 16 syl ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ J + 1 ↔ I ∈ 0 ..^ J ∨ I = J
18 10 17 mpbird ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ J + 1
19 simpr ⊢ φ ∧ I ∈ 0 ..^ J + 1 → I ∈ 0 ..^ J + 1
20 2 chnwrd ⊢ φ → C ∈ Word A
21 20 adantr ⊢ φ ∧ I ∈ 0 ..^ J + 1 → C ∈ Word A
22 3 7 syl ⊢ φ → J + 1 ∈ 0 … C
23 22 adantr ⊢ φ ∧ I ∈ 0 ..^ J + 1 → J + 1 ∈ 0 … C
24 pfxlen ⊢ C ∈ Word A ∧ J + 1 ∈ 0 … C → C prefix J + 1 = J + 1
25 21 23 24 syl2anc ⊢ φ ∧ I ∈ 0 ..^ J + 1 → C prefix J + 1 = J + 1
26 25 oveq2d ⊢ φ ∧ I ∈ 0 ..^ J + 1 → 0 ..^ C prefix J + 1 = 0 ..^ J + 1
27 19 26 eleqtrrd ⊢ φ ∧ I ∈ 0 ..^ J + 1 → I ∈ 0 ..^ C prefix J + 1
28 18 27 syldan ⊢ φ ∧ I ∈ 0 ..^ J → I ∈ 0 ..^ C prefix J + 1
29 4 9 28 chnerlem1 ⊢ φ ∧ I ∈ 0 ..^ J → C prefix J + 1 ⁡ I ∼ ˙ lastS ⁡ C prefix J + 1
30 20 adantr ⊢ φ ∧ I ∈ 0 ..^ J → C ∈ Word A
31 pfxfv ⊢ C ∈ Word A ∧ J + 1 ∈ 0 … C ∧ I ∈ 0 ..^ J + 1 → C prefix J + 1 ⁡ I = C ⁡ I
32 30 8 18 31 syl3anc ⊢ φ ∧ I ∈ 0 ..^ J → C prefix J + 1 ⁡ I = C ⁡ I
33 lencl ⊢ C ∈ Word A → C ∈ ℕ 0
34 20 33 syl ⊢ φ → C ∈ ℕ 0
35 fz0add1fz1 ⊢ C ∈ ℕ 0 ∧ J ∈ 0 ..^ C → J + 1 ∈ 1 … C
36 34 3 35 syl2anc ⊢ φ → J + 1 ∈ 1 … C
37 36 adantr ⊢ φ ∧ I ∈ 0 ..^ J → J + 1 ∈ 1 … C
38 pfxfvlsw ⊢ C ∈ Word A ∧ J + 1 ∈ 1 … C → lastS ⁡ C prefix J + 1 = C ⁡ J + 1 - 1
39 30 37 38 syl2anc ⊢ φ ∧ I ∈ 0 ..^ J → lastS ⁡ C prefix J + 1 = C ⁡ J + 1 - 1
40 elfzoel2 ⊢ I ∈ 0 ..^ J → J ∈ ℤ
41 40 adantl ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ ℤ
42 41 zcnd ⊢ φ ∧ I ∈ 0 ..^ J → J ∈ ℂ
43 1cnd ⊢ φ ∧ I ∈ 0 ..^ J → 1 ∈ ℂ
44 42 43 pncand ⊢ φ ∧ I ∈ 0 ..^ J → J + 1 - 1 = J
45 44 fveq2d ⊢ φ ∧ I ∈ 0 ..^ J → C ⁡ J + 1 - 1 = C ⁡ J
46 39 45 eqtrd ⊢ φ ∧ I ∈ 0 ..^ J → lastS ⁡ C prefix J + 1 = C ⁡ J
47 29 32 46 3brtr3d ⊢ φ ∧ I ∈ 0 ..^ J → C ⁡ I ∼ ˙ C ⁡ J