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 
|- ( ph -> .< Po A )
chnlt.2 
|- ( ph -> C e. ( .< Chain A ) )
chnlt.3 
|- ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
chnlt.4 
|- ( ph -> I e. ( 0 ..^ J ) )
Assertion chnlt 
|- ( ph -> ( C ` I ) .< ( C ` J ) )

Proof

Step Hyp Ref Expression
1 chnlt.1 
 |-  ( ph -> .< Po A )
2 chnlt.2 
 |-  ( ph -> C e. ( .< Chain A ) )
3 chnlt.3 
 |-  ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
4 chnlt.4 
 |-  ( ph -> I e. ( 0 ..^ J ) )
5 fzofzp1 
 |-  ( J e. ( 0 ..^ ( # ` C ) ) -> ( J + 1 ) e. ( 0 ... ( # ` C ) ) )
6 3 5 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... ( # ` C ) ) )
7 2 6 pfxchn 
 |-  ( ph -> ( C prefix ( J + 1 ) ) e. ( .< Chain A ) )
8 fzossz 
 |-  ( 0 ..^ ( # ` C ) ) C_ ZZ
9 8 3 sselid 
 |-  ( ph -> J e. ZZ )
10 9 zcnd 
 |-  ( ph -> J e. CC )
11 1cnd 
 |-  ( ph -> 1 e. CC )
12 2 chnwrd 
 |-  ( ph -> C e. Word A )
13 pfxlen 
 |-  ( ( C e. Word A /\ ( J + 1 ) e. ( 0 ... ( # ` C ) ) ) -> ( # ` ( C prefix ( J + 1 ) ) ) = ( J + 1 ) )
14 12 6 13 syl2anc 
 |-  ( ph -> ( # ` ( C prefix ( J + 1 ) ) ) = ( J + 1 ) )
15 10 11 14 mvrraddd 
 |-  ( ph -> ( ( # ` ( C prefix ( J + 1 ) ) ) - 1 ) = J )
16 15 oveq2d 
 |-  ( ph -> ( 0 ..^ ( ( # ` ( C prefix ( J + 1 ) ) ) - 1 ) ) = ( 0 ..^ J ) )
17 4 16 eleqtrrd 
 |-  ( ph -> I e. ( 0 ..^ ( ( # ` ( C prefix ( J + 1 ) ) ) - 1 ) ) )
18 1 7 17 chnub 
 |-  ( ph -> ( ( C prefix ( J + 1 ) ) ` I ) .< ( lastS ` ( C prefix ( J + 1 ) ) ) )
19 fzo0ssnn0 
 |-  ( 0 ..^ ( # ` C ) ) C_ NN0
20 19 3 sselid 
 |-  ( ph -> J e. NN0 )
21 fzossfzop1 
 |-  ( J e. NN0 -> ( 0 ..^ J ) C_ ( 0 ..^ ( J + 1 ) ) )
22 20 21 syl 
 |-  ( ph -> ( 0 ..^ J ) C_ ( 0 ..^ ( J + 1 ) ) )
23 22 4 sseldd 
 |-  ( ph -> I e. ( 0 ..^ ( J + 1 ) ) )
24 pfxfv 
 |-  ( ( C e. Word A /\ ( J + 1 ) e. ( 0 ... ( # ` C ) ) /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> ( ( C prefix ( J + 1 ) ) ` I ) = ( C ` I ) )
25 12 6 23 24 syl3anc 
 |-  ( ph -> ( ( C prefix ( J + 1 ) ) ` I ) = ( C ` I ) )
26 lencl 
 |-  ( C e. Word A -> ( # ` C ) e. NN0 )
27 12 26 syl 
 |-  ( ph -> ( # ` C ) e. NN0 )
28 fz0add1fz1 
 |-  ( ( ( # ` C ) e. NN0 /\ J e. ( 0 ..^ ( # ` C ) ) ) -> ( J + 1 ) e. ( 1 ... ( # ` C ) ) )
29 27 3 28 syl2anc 
 |-  ( ph -> ( J + 1 ) e. ( 1 ... ( # ` C ) ) )
30 pfxfvlsw 
 |-  ( ( C e. Word A /\ ( J + 1 ) e. ( 1 ... ( # ` C ) ) ) -> ( lastS ` ( C prefix ( J + 1 ) ) ) = ( C ` ( ( J + 1 ) - 1 ) ) )
31 12 29 30 syl2anc 
 |-  ( ph -> ( lastS ` ( C prefix ( J + 1 ) ) ) = ( C ` ( ( J + 1 ) - 1 ) ) )
32 10 11 pncand 
 |-  ( ph -> ( ( J + 1 ) - 1 ) = J )
33 32 fveq2d 
 |-  ( ph -> ( C ` ( ( J + 1 ) - 1 ) ) = ( C ` J ) )
34 31 33 eqtrd 
 |-  ( ph -> ( lastS ` ( C prefix ( J + 1 ) ) ) = ( C ` J ) )
35 18 25 34 3brtr3d 
 |-  ( ph -> ( C ` I ) .< ( C ` J ) )