This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxf1

Description: Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023)

Ref Expression
Hypotheses pfxf1.1 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
pfxf1.2 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝑆 )
pfxf1.3 ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
Assertion pfxf1 ( 𝜑 → ( 𝑊 prefix 𝐿 ) : dom ( 𝑊 prefix 𝐿 ) –1-1→ 𝑆 )

Proof

Step Hyp Ref Expression
1 pfxf1.1 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
2 pfxf1.2 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝑆 )
3 pfxf1.3 ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 elfzuz3 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
5 fzoss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐿 ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 3 4 5 3syl ⊢ ( 𝜑 → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 wrddm ⊢ ( 𝑊 ∈ Word 𝑆 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
8 1 7 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 6 8 sseqtrrd ⊢ ( 𝜑 → ( 0 ..^ 𝐿 ) ⊆ dom 𝑊 )
10 wrdf ⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
11 1 10 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
12 11 6 fssresd ⊢ ( 𝜑 → ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) : ( 0 ..^ 𝐿 ) ⟶ 𝑆 )
13 f1resf1 ⊢ ( ( 𝑊 : dom 𝑊 –1-1→ 𝑆 ∧ ( 0 ..^ 𝐿 ) ⊆ dom 𝑊 ∧ ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) : ( 0 ..^ 𝐿 ) –1-1→ 𝑆 )
14 2 9 12 13 syl3anc ⊢ ( 𝜑 → ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) : ( 0 ..^ 𝐿 ) –1-1→ 𝑆 )
15 pfxres ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) )
16 1 3 15 syl2anc ⊢ ( 𝜑 → ( 𝑊 prefix 𝐿 ) = ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) )
17 pfxfn ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) Fn ( 0 ..^ 𝐿 ) )
18 1 3 17 syl2anc ⊢ ( 𝜑 → ( 𝑊 prefix 𝐿 ) Fn ( 0 ..^ 𝐿 ) )
19 18 fndmd ⊢ ( 𝜑 → dom ( 𝑊 prefix 𝐿 ) = ( 0 ..^ 𝐿 ) )
20 eqidd ⊢ ( 𝜑 → 𝑆 = 𝑆 )
21 16 19 20 f1eq123d ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐿 ) : dom ( 𝑊 prefix 𝐿 ) –1-1→ 𝑆 ↔ ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) : ( 0 ..^ 𝐿 ) –1-1→ 𝑆 ) )
22 14 21 mpbird ⊢ ( 𝜑 → ( 𝑊 prefix 𝐿 ) : dom ( 𝑊 prefix 𝐿 ) –1-1→ 𝑆 )