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 ) = (/) )