Metamath Proof Explorer


Theorem swrdnd0

Description: The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022)

Ref Expression
Assertion swrdnd0 SWordV¬F0LL0SSsubstrFL=

Proof

Step Hyp Ref Expression
1 ianor ¬F0LL0S¬F0L¬L0S
2 3ianor ¬F0L0FL¬F0¬L0¬FL
3 elfz2nn0 F0LF0L0FL
4 2 3 xchnxbir ¬F0L¬F0¬L0¬FL
5 3ianor ¬L0S0LS¬L0¬S0¬LS
6 elfz2nn0 L0SL0S0LS
7 5 6 xchnxbir ¬L0S¬L0¬S0¬LS
8 4 7 orbi12i ¬F0L¬L0S¬F0¬L0¬FL¬L0¬S0¬LS
9 1 8 bitri ¬F0LL0S¬F0¬L0¬FL¬L0¬S0¬LS
10 df-3or ¬F0¬L0¬FL¬F0¬L0¬FL
11 ianor ¬F0L0¬F0¬L0
12 swrdnnn0nd SWordV¬F0L0SsubstrFL=
13 12 expcom ¬F0L0SWordVSsubstrFL=
14 11 13 sylbir ¬F0¬L0SWordVSsubstrFL=
15 anor F0L0¬¬F0¬L0
16 nn0re L0L
17 nn0re F0F
18 ltnle LFL<F¬FL
19 16 17 18 syl2anr F0L0L<F¬FL
20 nn0z F0F
21 nn0z L0L
22 20 21 anim12i F0L0FL
23 22 anim2i SWordVF0L0SWordVFL
24 3anass SWordVFLSWordVFL
25 23 24 sylibr SWordVF0L0SWordVFL
26 25 adantr SWordVF0L0L<FSWordVFL
27 17 16 anim12ci F0L0LF
28 27 adantl SWordVF0L0LF
29 ltle LFL<FLF
30 28 29 syl SWordVF0L0L<FLF
31 30 imp SWordVF0L0L<FLF
32 31 3mix2d SWordVF0L0L<FF<0LFS<L
33 swrdnd SWordVFLF<0LFS<LSsubstrFL=
34 26 32 33 sylc SWordVF0L0L<FSsubstrFL=
35 34 ex SWordVF0L0L<FSsubstrFL=
36 35 expcom F0L0SWordVL<FSsubstrFL=
37 36 com23 F0L0L<FSWordVSsubstrFL=
38 19 37 sylbird F0L0¬FLSWordVSsubstrFL=
39 15 38 sylbir ¬¬F0¬L0¬FLSWordVSsubstrFL=
40 39 imp ¬¬F0¬L0¬FLSWordVSsubstrFL=
41 14 40 jaoi3 ¬F0¬L0¬FLSWordVSsubstrFL=
42 10 41 sylbi ¬F0¬L0¬FLSWordVSsubstrFL=
43 3anor F0L0FL¬¬F0¬L0¬FL
44 pm2.24 L0¬L0SWordVSsubstrFL=
45 44 3ad2ant2 F0L0FL¬L0SWordVSsubstrFL=
46 45 com12 ¬L0F0L0FLSWordVSsubstrFL=
47 pm2.24 S0¬S0SsubstrFL=
48 lencl SWordVS0
49 47 48 syl11 ¬S0SWordVSsubstrFL=
50 49 a1d ¬S0F0L0FLSWordVSsubstrFL=
51 48 nn0red SWordVS
52 16 3ad2ant2 F0L0FLL
53 ltnle SLS<L¬LS
54 51 52 53 syl2anr F0L0FLSWordVS<L¬LS
55 simpr F0L0FLSWordVSWordV
56 20 3ad2ant1 F0L0FLF
57 56 adantr F0L0FLSWordVF
58 21 3ad2ant2 F0L0FLL
59 58 adantr F0L0FLSWordVL
60 55 57 59 3jca F0L0FLSWordVSWordVFL
61 3mix3 S<LF<0LFS<L
62 60 61 33 syl2im F0L0FLSWordVS<LSsubstrFL=
63 54 62 sylbird F0L0FLSWordV¬LSSsubstrFL=
64 63 com12 ¬LSF0L0FLSWordVSsubstrFL=
65 64 expd ¬LSF0L0FLSWordVSsubstrFL=
66 46 50 65 3jaoi ¬L0¬S0¬LSF0L0FLSWordVSsubstrFL=
67 43 66 syl5bir ¬L0¬S0¬LS¬¬F0¬L0¬FLSWordVSsubstrFL=
68 67 impcom ¬¬F0¬L0¬FL¬L0¬S0¬LSSWordVSsubstrFL=
69 42 68 jaoi3 ¬F0¬L0¬FL¬L0¬S0¬LSSWordVSsubstrFL=
70 69 com12 SWordV¬F0¬L0¬FL¬L0¬S0¬LSSsubstrFL=
71 9 70 syl5bi SWordV¬F0LL0SSsubstrFL=