Metamath Proof Explorer

Theorem pfxchn

Description: A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnwrd.1 ⊢ ( 𝜑 → 𝐶 ∈ ( < Chain 𝐴 ) )
pfxchn.2 ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) )
Assertion pfxchn ( 𝜑 → ( 𝐶 prefix 𝐿 ) ∈ ( < Chain 𝐴 ) )

Proof

Step Hyp Ref Expression
1 chnwrd.1 ⊢ ( 𝜑 → 𝐶 ∈ ( < Chain 𝐴 ) )
2 pfxchn.2 ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) )
3 1 chnwrd ⊢ ( 𝜑 → 𝐶 ∈ Word 𝐴 )
4 pfxcl ⊢ ( 𝐶 ∈ Word 𝐴 → ( 𝐶 prefix 𝐿 ) ∈ Word 𝐴 )
5 3 4 syl ⊢ ( 𝜑 → ( 𝐶 prefix 𝐿 ) ∈ Word 𝐴 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝐶 ∈ ( < Chain 𝐴 ) )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) )
8 elfzuz3 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
9 fzoss2 ⊢ ( ( ♯ ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐿 ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
10 7 8 9 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) )
12 11 eldifad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ∈ dom ( 𝐶 prefix 𝐿 ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝐶 ∈ Word 𝐴 )
14 pfxlen ⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) ) → ( ♯ ‘ ( 𝐶 prefix 𝐿 ) ) = 𝐿 )
15 13 7 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( ♯ ‘ ( 𝐶 prefix 𝐿 ) ) = 𝐿 )
16 15 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝐿 = ( ♯ ‘ ( 𝐶 prefix 𝐿 ) ) )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 𝐶 prefix 𝐿 ) ∈ Word 𝐴 )
18 16 17 wrdfd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 𝐶 prefix 𝐿 ) : ( 0 ..^ 𝐿 ) ⟶ 𝐴 )
19 18 fdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → dom ( 𝐶 prefix 𝐿 ) = ( 0 ..^ 𝐿 ) )
20 12 19 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ∈ ( 0 ..^ 𝐿 ) )
21 10 20 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 ) )
23 22 13 wrdfd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
24 23 fdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → dom 𝐶 = ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
25 21 24 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ∈ dom 𝐶 )
26 eldifsni ⊢ ( 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) → 𝑛 ≠ 0 )
27 11 26 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ≠ 0 )
28 25 27 eldifsnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝑛 ∈ ( dom 𝐶 ∖ { 0 } ) )
29 6 28 chnltm1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 𝐶 ‘ ( 𝑛 − 1 ) ) < ( 𝐶 ‘ 𝑛 ) )
30 7 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → 𝐿 ∈ ℤ )
31 fzossrbm1 ⊢ ( 𝐿 ∈ ℤ → ( 0 ..^ ( 𝐿 − 1 ) ) ⊆ ( 0 ..^ 𝐿 ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 0 ..^ ( 𝐿 − 1 ) ) ⊆ ( 0 ..^ 𝐿 ) )
33 fzom1ne1 ⊢ ( ( 𝑛 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑛 ≠ 0 ) → ( 𝑛 − 1 ) ∈ ( 0 ..^ ( 𝐿 − 1 ) ) )
34 20 27 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 𝑛 − 1 ) ∈ ( 0 ..^ ( 𝐿 − 1 ) ) )
35 32 34 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( 𝑛 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
36 pfxfv ⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) ∧ ( 𝑛 − 1 ) ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝐶 prefix 𝐿 ) ‘ ( 𝑛 − 1 ) ) = ( 𝐶 ‘ ( 𝑛 − 1 ) ) )
37 13 7 35 36 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( ( 𝐶 prefix 𝐿 ) ‘ ( 𝑛 − 1 ) ) = ( 𝐶 ‘ ( 𝑛 − 1 ) ) )
38 pfxfv ⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐶 ) ) ∧ 𝑛 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝐶 prefix 𝐿 ) ‘ 𝑛 ) = ( 𝐶 ‘ 𝑛 ) )
39 13 7 20 38 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( ( 𝐶 prefix 𝐿 ) ‘ 𝑛 ) = ( 𝐶 ‘ 𝑛 ) )
40 29 37 39 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ) → ( ( 𝐶 prefix 𝐿 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝐶 prefix 𝐿 ) ‘ 𝑛 ) )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ( ( 𝐶 prefix 𝐿 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝐶 prefix 𝐿 ) ‘ 𝑛 ) )
42 ischn ⊢ ( ( 𝐶 prefix 𝐿 ) ∈ ( < Chain 𝐴 ) ↔ ( ( 𝐶 prefix 𝐿 ) ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom ( 𝐶 prefix 𝐿 ) ∖ { 0 } ) ( ( 𝐶 prefix 𝐿 ) ‘ ( 𝑛 − 1 ) ) < ( ( 𝐶 prefix 𝐿 ) ‘ 𝑛 ) ) )
43 5 41 42 sylanbrc ⊢ ( 𝜑 → ( 𝐶 prefix 𝐿 ) ∈ ( < Chain 𝐴 ) )