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→ 𝑆 )