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 𝐴 )
chner.2 ⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
chner.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
Assertion chnerlem2 ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝐽 ) ) → ( 𝐶 ‘ 𝐼 ) ∼ ( 𝐶 ‘ 𝐽 ) )

Proof

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