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 
|- ( 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 >. ) )