Proof of Theorem clwlksf1clwwlklem
Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.1 |
. . . . . . . . . . . 12
|
2 | | clwlksfclwwlk.2 |
. . . . . . . . . . . 12
|
3 | | clwlksfclwwlk.c |
. . . . . . . . . . . 12
ClWalks |
4 | | clwlksfclwwlk.f |
. . . . . . . . . . . 12
substr |
5 | 1, 2, 3, 4 | clwlksf1clwwlklem3 26967 |
. . . . . . . . . . 11
Word Vtx |
6 | 1, 2, 3, 4 | clwlksf1clwwlklem3 26967 |
. . . . . . . . . . 11
Word Vtx |
7 | 5, 6 | anim12ci 591 |
. . . . . . . . . 10
Word
Vtx
Word Vtx |
8 | 7 | adantr 481 |
. . . . . . . . 9
Word Vtx
Word Vtx |
9 | | nnnn0 11299 |
. . . . . . . . . . 11
|
10 | 9 | adantl 482 |
. . . . . . . . . 10
|
11 | 1, 2, 3, 4 | clwlksf1clwwlklem1 26965 |
. . . . . . . . . . . 12
|
12 | 11 | adantl 482 |
. . . . . . . . . . 11
|
13 | 12 | adantr 481 |
. . . . . . . . . 10
|
14 | 1, 2, 3, 4 | clwlksf1clwwlklem1 26965 |
. . . . . . . . . . . 12
|
15 | 14 | adantr 481 |
. . . . . . . . . . 11
|
16 | 15 | adantr 481 |
. . . . . . . . . 10
|
17 | 10, 13, 16 | 3jca 1242 |
. . . . . . . . 9
|
18 | 8, 17 | jca 554 |
. . . . . . . 8
Word
Vtx
Word Vtx
|
19 | 18 | exp31 630 |
. . . . . . 7
Word
Vtx
Word Vtx
|
20 | 19 | 3imp31 1257 |
. . . . . 6
Word Vtx Word Vtx
|
21 | 20 | adantr 481 |
. . . . 5
substr substr
Word
Vtx
Word Vtx
|
22 | 1, 2, 3, 4 | clwlksfclwwlk1hashn 26959 |
. . . . . . . . . 10
|
23 | 22 | 3ad2ant2 1083 |
. . . . . . . . 9
|
24 | 23 | opeq2d 4409 |
. . . . . . . 8
|
25 | 24 | oveq2d 6666 |
. . . . . . 7
substr substr |
26 | 1, 2, 3, 4 | clwlksfclwwlk1hashn 26959 |
. . . . . . . . . 10
|
27 | 26 | 3ad2ant3 1084 |
. . . . . . . . 9
|
28 | 27 | opeq2d 4409 |
. . . . . . . 8
|
29 | 28 | oveq2d 6666 |
. . . . . . 7
substr substr |
30 | 25, 29 | eqeq12d 2637 |
. . . . . 6
substr
substr substr substr |
31 | 30 | biimpa 501 |
. . . . 5
substr substr
substr
substr |
32 | | simpl 473 |
. . . . . . 7
Word
Vtx
Word Vtx
Word Vtx Word Vtx |
33 | | id 22 |
. . . . . . . . . 10
|
34 | 33, 33 | jca 554 |
. . . . . . . . 9
|
35 | 34 | 3ad2ant1 1082 |
. . . . . . . 8
|
36 | 35 | adantl 482 |
. . . . . . 7
Word
Vtx
Word Vtx
|
37 | | 3simpc 1060 |
. . . . . . . 8
|
38 | 37 | adantl 482 |
. . . . . . 7
Word
Vtx
Word Vtx
|
39 | | swrdeq 13444 |
. . . . . . 7
Word
Vtx
Word Vtx
substr substr ..^ |
40 | 32, 36, 38, 39 | syl3anc 1326 |
. . . . . 6
Word
Vtx
Word Vtx
substr substr
..^ |
41 | | simpr 477 |
. . . . . 6
..^
..^ |
42 | 40, 41 | syl6bi 243 |
. . . . 5
Word
Vtx
Word Vtx
substr substr ..^ |
43 | 21, 31, 42 | sylc 65 |
. . . 4
substr substr
..^ |
44 | | lbfzo0 12507 |
. . . . . . . . 9
..^
|
45 | 44 | biimpri 218 |
. . . . . . . 8
..^ |
46 | 45 | 3ad2ant1 1082 |
. . . . . . 7
..^ |
47 | 46 | adantr 481 |
. . . . . 6
substr substr
..^ |
48 | | fveq2 6191 |
. . . . . . . 8
|
49 | | fveq2 6191 |
. . . . . . . 8
|
50 | 48, 49 | eqeq12d 2637 |
. . . . . . 7
|
51 | 50 | rspcv 3305 |
. . . . . 6
..^
..^ |
52 | 47, 51 | syl 17 |
. . . . 5
substr substr
..^ |
53 | 1, 2, 3, 4 | clwlksf1clwwlklem2 26966 |
. . . . . . . 8
|
54 | 53 | 3ad2ant2 1083 |
. . . . . . 7
|
55 | 54 | adantr 481 |
. . . . . 6
substr substr
|
56 | 1, 2, 3, 4 | clwlksf1clwwlklem2 26966 |
. . . . . . . 8
|
57 | 56 | 3ad2ant3 1084 |
. . . . . . 7
|
58 | 57 | adantr 481 |
. . . . . 6
substr substr
|
59 | 55, 58 | eqeq12d 2637 |
. . . . 5
substr substr
|
60 | 52, 59 | sylibd 229 |
. . . 4
substr substr
..^ |
61 | 43, 60 | jcai 559 |
. . 3
substr substr
..^ |
62 | | elnn0uz 11725 |
. . . . . . . . 9
|
63 | 9, 62 | sylib 208 |
. . . . . . . 8
|
64 | 63 | 3ad2ant1 1082 |
. . . . . . 7
|
65 | 64 | adantr 481 |
. . . . . 6
substr substr
|
66 | | fzisfzounsn 12580 |
. . . . . 6
..^ |
67 | 65, 66 | syl 17 |
. . . . 5
substr substr
..^ |
68 | 67 | raleqdv 3144 |
. . . 4
substr substr
..^ |
69 | | simpl1 1064 |
. . . . 5
substr substr
|
70 | | fveq2 6191 |
. . . . . . 7
|
71 | | fveq2 6191 |
. . . . . . 7
|
72 | 70, 71 | eqeq12d 2637 |
. . . . . 6
|
73 | 72 | ralunsn 4422 |
. . . . 5
..^
..^ |
74 | 69, 73 | syl 17 |
. . . 4
substr substr
..^ ..^
|
75 | 68, 74 | bitrd 268 |
. . 3
substr substr
..^
|
76 | 61, 75 | mpbird 247 |
. 2
substr substr
|
77 | 76 | ex 450 |
1
substr
substr
|