Metamath Proof Explorer

Theorem chnsubseqwl

Description: A subsequence of a chain has the same length as its indexing sequence. (Contributed by Ender Ting, 22-Jan-2026)

Ref Expression
Hypotheses chnsubseq.1 
|- ( ph -> W e. ( .< Chain A ) )
chnsubseq.2 
|- ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
Assertion chnsubseqwl 
|- ( ph -> ( # ` ( W o. I ) ) = ( # ` I ) )

Proof

Step Hyp Ref Expression
1 chnsubseq.1 
 |-  ( ph -> W e. ( .< Chain A ) )
2 chnsubseq.2 
 |-  ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
3 2 chnwrd 
 |-  ( ph -> I e. Word ( 0 ..^ ( # ` W ) ) )
4 wrdf 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
5 3 4 syl 
 |-  ( ph -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
6 5 frnd 
 |-  ( ph -> ran I C_ ( 0 ..^ ( # ` W ) ) )
7 1 chnwrd 
 |-  ( ph -> W e. Word A )
8 wrddm 
 |-  ( W e. Word A -> dom W = ( 0 ..^ ( # ` W ) ) )
9 7 8 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
10 6 9 sseqtrrd 
 |-  ( ph -> ran I C_ dom W )
11 dmcosseq 
 |-  ( ran I C_ dom W -> dom ( W o. I ) = dom I )
12 10 11 syl 
 |-  ( ph -> dom ( W o. I ) = dom I )
13 1 2 chnsubseqword 
 |-  ( ph -> ( W o. I ) e. Word A )
14 wrddm 
 |-  ( ( W o. I ) e. Word A -> dom ( W o. I ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
15 13 14 syl 
 |-  ( ph -> dom ( W o. I ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
16 wrddm 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> dom I = ( 0 ..^ ( # ` I ) ) )
17 3 16 syl 
 |-  ( ph -> dom I = ( 0 ..^ ( # ` I ) ) )
18 12 15 17 3eqtr3d 
 |-  ( ph -> ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) )
19 0z 
 |-  0 e. ZZ
20 lencl 
 |-  ( ( W o. I ) e. Word A -> ( # ` ( W o. I ) ) e. NN0 )
21 13 20 syl 
 |-  ( ph -> ( # ` ( W o. I ) ) e. NN0 )
22 21 nn0zd 
 |-  ( ph -> ( # ` ( W o. I ) ) e. ZZ )
23 simpr 
 |-  ( ( ph /\ 0 < ( # ` ( W o. I ) ) ) -> 0 < ( # ` ( W o. I ) ) )
24 fzoopth 
 |-  ( ( 0 e. ZZ /\ ( # ` ( W o. I ) ) e. ZZ /\ 0 < ( # ` ( W o. I ) ) ) -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> ( 0 = 0 /\ ( # ` ( W o. I ) ) = ( # ` I ) ) ) )
25 19 22 23 24 mp3an2ani 
 |-  ( ( ph /\ 0 < ( # ` ( W o. I ) ) ) -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> ( 0 = 0 /\ ( # ` ( W o. I ) ) = ( # ` I ) ) ) )
26 eqid 
 |-  0 = 0
27 26 biantrur 
 |-  ( ( # ` ( W o. I ) ) = ( # ` I ) <-> ( 0 = 0 /\ ( # ` ( W o. I ) ) = ( # ` I ) ) )
28 25 27 bitr4di 
 |-  ( ( ph /\ 0 < ( # ` ( W o. I ) ) ) -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> ( # ` ( W o. I ) ) = ( # ` I ) ) )
29 simpr 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> 0 = ( # ` ( W o. I ) ) )
30 29 oveq2d 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( 0 ..^ 0 ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
31 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
32 30 31 eqtr3di 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( 0 ..^ ( # ` ( W o. I ) ) ) = (/) )
33 32 eqeq1d 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> (/) = ( 0 ..^ ( # ` I ) ) ) )
34 eqcom 
 |-  ( (/) = ( 0 ..^ ( # ` I ) ) <-> ( 0 ..^ ( # ` I ) ) = (/) )
35 33 34 bitrdi 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> ( 0 ..^ ( # ` I ) ) = (/) ) )
36 0zd 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> 0 e. ZZ )
37 lencl 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> ( # ` I ) e. NN0 )
38 3 37 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
39 38 nn0zd 
 |-  ( ph -> ( # ` I ) e. ZZ )
40 39 adantr 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( # ` I ) e. ZZ )
41 fzon 
 |-  ( ( 0 e. ZZ /\ ( # ` I ) e. ZZ ) -> ( ( # ` I ) <_ 0 <-> ( 0 ..^ ( # ` I ) ) = (/) ) )
42 36 40 41 syl2anc 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( # ` I ) <_ 0 <-> ( 0 ..^ ( # ` I ) ) = (/) ) )
43 nn0le0eq0 
 |-  ( ( # ` I ) e. NN0 -> ( ( # ` I ) <_ 0 <-> ( # ` I ) = 0 ) )
44 43 biimpa 
 |-  ( ( ( # ` I ) e. NN0 /\ ( # ` I ) <_ 0 ) -> ( # ` I ) = 0 )
45 38 44 sylan 
 |-  ( ( ph /\ ( # ` I ) <_ 0 ) -> ( # ` I ) = 0 )
46 45 adantlr 
 |-  ( ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) /\ ( # ` I ) <_ 0 ) -> ( # ` I ) = 0 )
47 id 
 |-  ( ( # ` I ) = 0 -> ( # ` I ) = 0 )
48 0le0 
 |-  0 <_ 0
49 47 48 eqbrtrdi 
 |-  ( ( # ` I ) = 0 -> ( # ` I ) <_ 0 )
50 49 adantl 
 |-  ( ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) /\ ( # ` I ) = 0 ) -> ( # ` I ) <_ 0 )
51 46 50 impbida 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( # ` I ) <_ 0 <-> ( # ` I ) = 0 ) )
52 eqcom 
 |-  ( ( # ` I ) = 0 <-> 0 = ( # ` I ) )
53 52 a1i 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( # ` I ) = 0 <-> 0 = ( # ` I ) ) )
54 29 eqeq1d 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( 0 = ( # ` I ) <-> ( # ` ( W o. I ) ) = ( # ` I ) ) )
55 51 53 54 3bitrd 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( # ` I ) <_ 0 <-> ( # ` ( W o. I ) ) = ( # ` I ) ) )
56 35 42 55 3bitr2d 
 |-  ( ( ph /\ 0 = ( # ` ( W o. I ) ) ) -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> ( # ` ( W o. I ) ) = ( # ` I ) ) )
57 21 nn0ge0d 
 |-  ( ph -> 0 <_ ( # ` ( W o. I ) ) )
58 0red 
 |-  ( ph -> 0 e. RR )
59 21 nn0red 
 |-  ( ph -> ( # ` ( W o. I ) ) e. RR )
60 58 59 leloed 
 |-  ( ph -> ( 0 <_ ( # ` ( W o. I ) ) <-> ( 0 < ( # ` ( W o. I ) ) \/ 0 = ( # ` ( W o. I ) ) ) ) )
61 57 60 mpbid 
 |-  ( ph -> ( 0 < ( # ` ( W o. I ) ) \/ 0 = ( # ` ( W o. I ) ) ) )
62 28 56 61 mpjaodan 
 |-  ( ph -> ( ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) <-> ( # ` ( W o. I ) ) = ( # ` I ) ) )
63 18 62 mpbid 
 |-  ( ph -> ( # ` ( W o. I ) ) = ( # ` I ) )