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

Metamath Proof Explorer

Theorem wrdsymb0

Description: A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion wrdsymb0 
|- ( ( W e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ ( # ` W ) <_ I ) -> ( W ` I ) = (/) ) )

Proof

Step Hyp Ref Expression
1 wrddm 
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
2 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
3 2 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
4 simpr 
 |-  ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) -> I e. ZZ )
5 0zd 
 |-  ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) -> 0 e. ZZ )
6 simpl 
 |-  ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) -> ( # ` W ) e. ZZ )
7 nelfzo 
 |-  ( ( I e. ZZ /\ 0 e. ZZ /\ ( # ` W ) e. ZZ ) -> ( I e/ ( 0 ..^ ( # ` W ) ) <-> ( I < 0 \/ ( # ` W ) <_ I ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) -> ( I e/ ( 0 ..^ ( # ` W ) ) <-> ( I < 0 \/ ( # ` W ) <_ I ) ) )
9 8 biimpar 
 |-  ( ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) /\ ( I < 0 \/ ( # ` W ) <_ I ) ) -> I e/ ( 0 ..^ ( # ` W ) ) )
10 df-nel 
 |-  ( I e/ ( 0 ..^ ( # ` W ) ) <-> -. I e. ( 0 ..^ ( # ` W ) ) )
11 9 10 sylib 
 |-  ( ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) /\ ( I < 0 \/ ( # ` W ) <_ I ) ) -> -. I e. ( 0 ..^ ( # ` W ) ) )
12 eleq2 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( I e. dom W <-> I e. ( 0 ..^ ( # ` W ) ) ) )
13 12 notbid 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( -. I e. dom W <-> -. I e. ( 0 ..^ ( # ` W ) ) ) )
14 11 13 imbitrrid 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( ( ( # ` W ) e. ZZ /\ I e. ZZ ) /\ ( I < 0 \/ ( # ` W ) <_ I ) ) -> -. I e. dom W ) )
15 14 exp4c 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) e. ZZ -> ( I e. ZZ -> ( ( I < 0 \/ ( # ` W ) <_ I ) -> -. I e. dom W ) ) ) )
16 1 3 15 sylc 
 |-  ( W e. Word V -> ( I e. ZZ -> ( ( I < 0 \/ ( # ` W ) <_ I ) -> -. I e. dom W ) ) )
17 16 imp 
 |-  ( ( W e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ ( # ` W ) <_ I ) -> -. I e. dom W ) )
18 ndmfv 
 |-  ( -. I e. dom W -> ( W ` I ) = (/) )
19 17 18 syl6 
 |-  ( ( W e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ ( # ` W ) <_ I ) -> ( W ` I ) = (/) ) )