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
|- ( S e. Word A -> ( S prefix L ) = ( S substr <. 0 , L >. ) )

Proof

Step Hyp Ref Expression
1 pfxval
 |-  ( ( S e. Word A /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
2 simpr
 |-  ( ( S e. _V /\ L e. NN0 ) -> L e. NN0 )
3 2 con3i
 |-  ( -. L e. NN0 -> -. ( S e. _V /\ L e. NN0 ) )
4 3 adantl
 |-  ( ( S e. Word A /\ -. L e. NN0 ) -> -. ( S e. _V /\ L e. NN0 ) )
5 pfxnndmnd
 |-  ( -. ( S e. _V /\ L e. NN0 ) -> ( S prefix L ) = (/) )
6 4 5 syl
 |-  ( ( S e. Word A /\ -. L e. NN0 ) -> ( S prefix L ) = (/) )
7 simpr
 |-  ( ( 0 e. NN0 /\ L e. NN0 ) -> L e. NN0 )
8 7 con3i
 |-  ( -. L e. NN0 -> -. ( 0 e. NN0 /\ L e. NN0 ) )
9 swrdnnn0nd
 |-  ( ( S e. Word A /\ -. ( 0 e. NN0 /\ L e. NN0 ) ) -> ( S substr <. 0 , L >. ) = (/) )
10 8 9 sylan2
 |-  ( ( S e. Word A /\ -. L e. NN0 ) -> ( S substr <. 0 , L >. ) = (/) )
11 6 10 eqtr4d
 |-  ( ( S e. Word A /\ -. L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
12 1 11 pm2.61dan
 |-  ( S e. Word A -> ( S prefix L ) = ( S substr <. 0 , L >. ) )