Metamath Proof Explorer

Theorem pfxnd0

Description: The value of a prefix operation for a length argument not in the range of 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-Dec-2022)

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

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( L e/ ( 0 ... ( # ` W ) ) <-> -. L e. ( 0 ... ( # ` W ) ) )
2 1 a1i 
 |-  ( W e. Word V -> ( L e/ ( 0 ... ( # ` W ) ) <-> -. L e. ( 0 ... ( # ` W ) ) ) )
3 elfz2nn0 
 |-  ( L e. ( 0 ... ( # ` W ) ) <-> ( L e. NN0 /\ ( # ` W ) e. NN0 /\ L <_ ( # ` W ) ) )
4 3 a1i 
 |-  ( W e. Word V -> ( L e. ( 0 ... ( # ` W ) ) <-> ( L e. NN0 /\ ( # ` W ) e. NN0 /\ L <_ ( # ` W ) ) ) )
5 4 notbid 
 |-  ( W e. Word V -> ( -. L e. ( 0 ... ( # ` W ) ) <-> -. ( L e. NN0 /\ ( # ` W ) e. NN0 /\ L <_ ( # ` W ) ) ) )
6 3ianor 
 |-  ( -. ( L e. NN0 /\ ( # ` W ) e. NN0 /\ L <_ ( # ` W ) ) <-> ( -. L e. NN0 \/ -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) ) )
7 6 a1i 
 |-  ( W e. Word V -> ( -. ( L e. NN0 /\ ( # ` W ) e. NN0 /\ L <_ ( # ` W ) ) <-> ( -. L e. NN0 \/ -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) ) ) )
8 2 5 7 3bitrd 
 |-  ( W e. Word V -> ( L e/ ( 0 ... ( # ` W ) ) <-> ( -. L e. NN0 \/ -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) ) ) )
9 3orrot 
 |-  ( ( -. L e. NN0 \/ -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) ) <-> ( -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) \/ -. L e. NN0 ) )
10 3orass 
 |-  ( ( -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) \/ -. L e. NN0 ) <-> ( -. ( # ` W ) e. NN0 \/ ( -. L <_ ( # ` W ) \/ -. L e. NN0 ) ) )
11 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
12 11 pm2.24d 
 |-  ( W e. Word V -> ( -. ( # ` W ) e. NN0 -> ( W prefix L ) = (/) ) )
13 12 com12 
 |-  ( -. ( # ` W ) e. NN0 -> ( W e. Word V -> ( W prefix L ) = (/) ) )
14 simpr 
 |-  ( ( W e. _V /\ L e. NN0 ) -> L e. NN0 )
15 pfxnndmnd 
 |-  ( -. ( W e. _V /\ L e. NN0 ) -> ( W prefix L ) = (/) )
16 14 15 nsyl5 
 |-  ( -. L e. NN0 -> ( W prefix L ) = (/) )
17 16 a1d 
 |-  ( -. L e. NN0 -> ( W e. Word V -> ( W prefix L ) = (/) ) )
18 notnotb 
 |-  ( L e. NN0 <-> -. -. L e. NN0 )
19 11 nn0red 
 |-  ( W e. Word V -> ( # ` W ) e. RR )
20 nn0re 
 |-  ( L e. NN0 -> L e. RR )
21 ltnle 
 |-  ( ( ( # ` W ) e. RR /\ L e. RR ) -> ( ( # ` W ) < L <-> -. L <_ ( # ` W ) ) )
22 19 20 21 syl2an 
 |-  ( ( W e. Word V /\ L e. NN0 ) -> ( ( # ` W ) < L <-> -. L <_ ( # ` W ) ) )
23 pfxnd 
 |-  ( ( W e. Word V /\ L e. NN0 /\ ( # ` W ) < L ) -> ( W prefix L ) = (/) )
24 23 3expia 
 |-  ( ( W e. Word V /\ L e. NN0 ) -> ( ( # ` W ) < L -> ( W prefix L ) = (/) ) )
25 22 24 sylbird 
 |-  ( ( W e. Word V /\ L e. NN0 ) -> ( -. L <_ ( # ` W ) -> ( W prefix L ) = (/) ) )
26 25 expcom 
 |-  ( L e. NN0 -> ( W e. Word V -> ( -. L <_ ( # ` W ) -> ( W prefix L ) = (/) ) ) )
27 26 com23 
 |-  ( L e. NN0 -> ( -. L <_ ( # ` W ) -> ( W e. Word V -> ( W prefix L ) = (/) ) ) )
28 18 27 sylbir 
 |-  ( -. -. L e. NN0 -> ( -. L <_ ( # ` W ) -> ( W e. Word V -> ( W prefix L ) = (/) ) ) )
29 28 imp 
 |-  ( ( -. -. L e. NN0 /\ -. L <_ ( # ` W ) ) -> ( W e. Word V -> ( W prefix L ) = (/) ) )
30 17 29 jaoi3 
 |-  ( ( -. L e. NN0 \/ -. L <_ ( # ` W ) ) -> ( W e. Word V -> ( W prefix L ) = (/) ) )
31 30 orcoms 
 |-  ( ( -. L <_ ( # ` W ) \/ -. L e. NN0 ) -> ( W e. Word V -> ( W prefix L ) = (/) ) )
32 13 31 jaoi 
 |-  ( ( -. ( # ` W ) e. NN0 \/ ( -. L <_ ( # ` W ) \/ -. L e. NN0 ) ) -> ( W e. Word V -> ( W prefix L ) = (/) ) )
33 10 32 sylbi 
 |-  ( ( -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) \/ -. L e. NN0 ) -> ( W e. Word V -> ( W prefix L ) = (/) ) )
34 9 33 sylbi 
 |-  ( ( -. L e. NN0 \/ -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) ) -> ( W e. Word V -> ( W prefix L ) = (/) ) )
35 34 com12 
 |-  ( W e. Word V -> ( ( -. L e. NN0 \/ -. ( # ` W ) e. NN0 \/ -. L <_ ( # ` W ) ) -> ( W prefix L ) = (/) ) )
36 8 35 sylbid 
 |-  ( W e. Word V -> ( L e/ ( 0 ... ( # ` W ) ) -> ( W prefix L ) = (/) ) )
37 36 imp 
 |-  ( ( W e. Word V /\ L e/ ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) = (/) )