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