Metamath Proof Explorer

Theorem chnlt

Description: Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnlt.1 ⊢ ( 𝜑 → < Po 𝐴 )
chnlt.2 ⊢ ( 𝜑 → 𝐶 ∈ ( < Chain 𝐴 ) )
chnlt.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
chnlt.4 ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝐽 ) )
Assertion chnlt ( 𝜑 → ( 𝐶 ‘ 𝐼 ) < ( 𝐶 ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 chnlt.1 ⊢ ( 𝜑 → < Po 𝐴 )
2 chnlt.2 ⊢ ( 𝜑 → 𝐶 ∈ ( < Chain 𝐴 ) )
3 chnlt.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
4 chnlt.4 ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝐽 ) )
5 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → ( 𝐽 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) )
6 3 5 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) )
7 2 6 pfxchn ⊢ ( 𝜑 → ( 𝐶 prefix ( 𝐽 + 1 ) ) ∈ ( < Chain 𝐴 ) )
8 fzossz ⊢ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ⊆ ℤ
9 8 3 sselid ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
10 9 zcnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
11 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
12 2 chnwrd ⊢ ( 𝜑 → 𝐶 ∈ Word 𝐴 )
13 pfxlen ⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ ( 𝐽 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) ) → ( ♯ ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) = ( 𝐽 + 1 ) )
14 12 6 13 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) = ( 𝐽 + 1 ) )
15 10 11 14 mvrraddd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) − 1 ) = 𝐽 )
16 15 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) − 1 ) ) = ( 0 ..^ 𝐽 ) )
17 4 16 eleqtrrd ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) − 1 ) ) )
18 1 7 17 chnub ⊢ ( 𝜑 → ( ( 𝐶 prefix ( 𝐽 + 1 ) ) ‘ 𝐼 ) < ( lastS ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) )
19 fzo0ssnn0 ⊢ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ⊆ ℕ0
20 19 3 sselid ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
21 fzossfzop1 ⊢ ( 𝐽 ∈ ℕ0 → ( 0 ..^ 𝐽 ) ⊆ ( 0 ..^ ( 𝐽 + 1 ) ) )
22 20 21 syl ⊢ ( 𝜑 → ( 0 ..^ 𝐽 ) ⊆ ( 0 ..^ ( 𝐽 + 1 ) ) )
23 22 4 sseldd ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) )
24 pfxfv ⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ ( 𝐽 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) ∧ 𝐼 ∈ ( 0 ..^ ( 𝐽 + 1 ) ) ) → ( ( 𝐶 prefix ( 𝐽 + 1 ) ) ‘ 𝐼 ) = ( 𝐶 ‘ 𝐼 ) )
25 12 6 23 24 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 prefix ( 𝐽 + 1 ) ) ‘ 𝐼 ) = ( 𝐶 ‘ 𝐼 ) )
26 lencl ⊢ ( 𝐶 ∈ Word 𝐴 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
27 12 26 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
28 fz0add1fz1 ⊢ ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ0 ∧ 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) → ( 𝐽 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) )
29 27 3 28 syl2anc ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) )
30 pfxfvlsw ⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ ( 𝐽 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( lastS ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) = ( 𝐶 ‘ ( ( 𝐽 + 1 ) − 1 ) ) )
31 12 29 30 syl2anc ⊢ ( 𝜑 → ( lastS ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) = ( 𝐶 ‘ ( ( 𝐽 + 1 ) − 1 ) ) )
32 10 11 pncand ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) − 1 ) = 𝐽 )
33 32 fveq2d ⊢ ( 𝜑 → ( 𝐶 ‘ ( ( 𝐽 + 1 ) − 1 ) ) = ( 𝐶 ‘ 𝐽 ) )
34 31 33 eqtrd ⊢ ( 𝜑 → ( lastS ‘ ( 𝐶 prefix ( 𝐽 + 1 ) ) ) = ( 𝐶 ‘ 𝐽 ) )
35 18 25 34 3brtr3d ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐼 ) < ( 𝐶 ‘ 𝐽 ) )