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 
|- ( ph -> .~ Er A )
chner.2 
|- ( ph -> C e. ( .~ Chain A ) )
chner.3 
|- ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
Assertion chnerlem2 
|- ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( C ` I ) .~ ( C ` J ) )

Proof

Step Hyp Ref Expression
1 chner.1 
 |-  ( ph -> .~ Er A )
2 chner.2 
 |-  ( ph -> C e. ( .~ Chain A ) )
3 chner.3 
 |-  ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
4 1 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> .~ Er A )
5 2 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> C e. ( .~ Chain A ) )
6 3 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> J e. ( 0 ..^ ( # ` C ) ) )
7 fzofzp1 
 |-  ( J e. ( 0 ..^ ( # ` C ) ) -> ( J + 1 ) e. ( 0 ... ( # ` C ) ) )
8 6 7 syl 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( J + 1 ) e. ( 0 ... ( # ` C ) ) )
9 5 8 pfxchn 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( C prefix ( J + 1 ) ) e. ( .~ Chain A ) )
10 animorrl 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( I e. ( 0 ..^ J ) \/ I = J ) )
11 elfzonn0 
 |-  ( J e. ( 0 ..^ ( # ` C ) ) -> J e. NN0 )
12 elnn0uz 
 |-  ( J e. NN0 <-> J e. ( ZZ>= ` 0 ) )
13 12 biimpi 
 |-  ( J e. NN0 -> J e. ( ZZ>= ` 0 ) )
14 3 11 13 3syl 
 |-  ( ph -> J e. ( ZZ>= ` 0 ) )
15 14 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> J e. ( ZZ>= ` 0 ) )
16 fzosplitsni 
 |-  ( J e. ( ZZ>= ` 0 ) -> ( I e. ( 0 ..^ ( J + 1 ) ) <-> ( I e. ( 0 ..^ J ) \/ I = J ) ) )
17 15 16 syl 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( I e. ( 0 ..^ ( J + 1 ) ) <-> ( I e. ( 0 ..^ J ) \/ I = J ) ) )
18 10 17 mpbird 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> I e. ( 0 ..^ ( J + 1 ) ) )
19 simpr 
 |-  ( ( ph /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> I e. ( 0 ..^ ( J + 1 ) ) )
20 2 chnwrd 
 |-  ( ph -> C e. Word A )
21 20 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> C e. Word A )
22 3 7 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... ( # ` C ) ) )
23 22 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> ( J + 1 ) e. ( 0 ... ( # ` C ) ) )
24 pfxlen 
 |-  ( ( C e. Word A /\ ( J + 1 ) e. ( 0 ... ( # ` C ) ) ) -> ( # ` ( C prefix ( J + 1 ) ) ) = ( J + 1 ) )
25 21 23 24 syl2anc 
 |-  ( ( ph /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> ( # ` ( C prefix ( J + 1 ) ) ) = ( J + 1 ) )
26 25 oveq2d 
 |-  ( ( ph /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> ( 0 ..^ ( # ` ( C prefix ( J + 1 ) ) ) ) = ( 0 ..^ ( J + 1 ) ) )
27 19 26 eleqtrrd 
 |-  ( ( ph /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> I e. ( 0 ..^ ( # ` ( C prefix ( J + 1 ) ) ) ) )
28 18 27 syldan 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> I e. ( 0 ..^ ( # ` ( C prefix ( J + 1 ) ) ) ) )
29 4 9 28 chnerlem1 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( ( C prefix ( J + 1 ) ) ` I ) .~ ( lastS ` ( C prefix ( J + 1 ) ) ) )
30 20 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> C e. Word A )
31 pfxfv 
 |-  ( ( C e. Word A /\ ( J + 1 ) e. ( 0 ... ( # ` C ) ) /\ I e. ( 0 ..^ ( J + 1 ) ) ) -> ( ( C prefix ( J + 1 ) ) ` I ) = ( C ` I ) )
32 30 8 18 31 syl3anc 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( ( C prefix ( J + 1 ) ) ` I ) = ( C ` I ) )
33 lencl 
 |-  ( C e. Word A -> ( # ` C ) e. NN0 )
34 20 33 syl 
 |-  ( ph -> ( # ` C ) e. NN0 )
35 fz0add1fz1 
 |-  ( ( ( # ` C ) e. NN0 /\ J e. ( 0 ..^ ( # ` C ) ) ) -> ( J + 1 ) e. ( 1 ... ( # ` C ) ) )
36 34 3 35 syl2anc 
 |-  ( ph -> ( J + 1 ) e. ( 1 ... ( # ` C ) ) )
37 36 adantr 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( J + 1 ) e. ( 1 ... ( # ` C ) ) )
38 pfxfvlsw 
 |-  ( ( C e. Word A /\ ( J + 1 ) e. ( 1 ... ( # ` C ) ) ) -> ( lastS ` ( C prefix ( J + 1 ) ) ) = ( C ` ( ( J + 1 ) - 1 ) ) )
39 30 37 38 syl2anc 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( lastS ` ( C prefix ( J + 1 ) ) ) = ( C ` ( ( J + 1 ) - 1 ) ) )
40 elfzoel2 
 |-  ( I e. ( 0 ..^ J ) -> J e. ZZ )
41 40 adantl 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> J e. ZZ )
42 41 zcnd 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> J e. CC )
43 1cnd 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> 1 e. CC )
44 42 43 pncand 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( ( J + 1 ) - 1 ) = J )
45 44 fveq2d 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( C ` ( ( J + 1 ) - 1 ) ) = ( C ` J ) )
46 39 45 eqtrd 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( lastS ` ( C prefix ( J + 1 ) ) ) = ( C ` J ) )
47 29 32 46 3brtr3d 
 |-  ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( C ` I ) .~ ( C ` J ) )