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