Theorem pfxval0

Description: Value of a prefix operation. This theorem should only be used in proofs if L e. NN0 is not available. Otherwise (and usually), pfxval should be used. (Contributed by AV, 3-Dec-2022) (New usage is discouraged.)

	Ref	Expression
Assertion	pfxval0	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		pfxval	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )
2		simpr	⊢ ( ( 𝑆 ∈ V ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ0 )
3	2	con3i	⊢ ( ¬ 𝐿 ∈ ℕ0 → ¬ ( 𝑆 ∈ V ∧ 𝐿 ∈ ℕ0 ) )
4	3	adantl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ¬ 𝐿 ∈ ℕ0 ) → ¬ ( 𝑆 ∈ V ∧ 𝐿 ∈ ℕ0 ) )
5		pfxnndmnd	⊢ ( ¬ ( 𝑆 ∈ V ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ∅ )
6	4 5	syl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ¬ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ∅ )
7		simpr	⊢ ( ( 0 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ0 )
8	7	con3i	⊢ ( ¬ 𝐿 ∈ ℕ0 → ¬ ( 0 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) )
9		swrdnnn0nd	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ¬ ( 0 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) = ∅ )
10	8 9	sylan2	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ¬ 𝐿 ∈ ℕ0 ) → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) = ∅ )
11	6 10	eqtr4d	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ¬ 𝐿 ∈ ℕ0 ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )
12	1 11	pm2.61dan	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )