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

Metamath Proof Explorer

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 , 𝐿 ⟩ ) )