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

Metamath Proof Explorer

Theorem pfxnd

Description: The value of a prefix operation for a length argument larger than the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv ). (Contributed by AV, 3-May-2020)

Ref Expression
Assertion pfxnd 
|- ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W prefix L ) = (/) )

Proof

Step Hyp Ref Expression
1 pfxval 
 |-  ( ( W e. Word V /\ L e. NN0 ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
2 1 3adant3 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
3 simp1 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> W e. Word V )
4 0zd 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> 0 e. ZZ )
5 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
6 5 3ad2ant2 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> L e. ZZ )
7 3 4 6 3jca 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W e. Word V /\ 0 e. ZZ /\ L e. ZZ ) )
8 3mix3 
 |-  ( ( # ` W ) < L -> ( 0 < 0 \/ L <_ 0 \/ ( # ` W ) < L ) )
9 8 3ad2ant3 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( 0 < 0 \/ L <_ 0 \/ ( # ` W ) < L ) )
10 swrdnd 
 |-  ( ( W e. Word V /\ 0 e. ZZ /\ L e. ZZ ) -> ( ( 0 < 0 \/ L <_ 0 \/ ( # ` W ) < L ) -> ( W substr <. 0 , L >. ) = (/) ) )
11 7 9 10 sylc 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W substr <. 0 , L >. ) = (/) )
12 2 11 eqtrd 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W prefix L ) = (/) )