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