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