Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . . 4
⢠ð = (ð ClWWalksN ðº) |
2 | | erclwwlkn.r |
. . . 4
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð ⧠ð¢ â ð ⧠âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
3 | 1, 2 | erclwwlkneqlen 29061 |
. . 3
⢠((ð¥ â V ⧠ðŠ â V) â (ð¥ ⌠ðŠ â (â¯âð¥) = (â¯âðŠ))) |
4 | 1, 2 | erclwwlkneq 29060 |
. . . 4
⢠((ð¥ â V ⧠ðŠ â V) â (ð¥ ⌠ðŠ â (ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)))) |
5 | | simpl2 1193 |
. . . . . . 7
⢠(((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) ⧠(â¯âð¥) = (â¯âðŠ)) â ðŠ â ð) |
6 | | simpl1 1192 |
. . . . . . 7
⢠(((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) ⧠(â¯âð¥) = (â¯âðŠ)) â ð¥ â ð) |
7 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
â¢
(Vtxâðº) =
(Vtxâðº) |
8 | 7 | clwwlknbp 29028 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
9 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . 20
â¢
((â¯âð¥) =
ð â ð = (â¯âð¥)) |
10 | 9 | biimpi 215 |
. . . . . . . . . . . . . . . . . . 19
â¢
((â¯âð¥) =
ð â ð = (â¯âð¥)) |
11 | 8, 10 | simpl2im 505 |
. . . . . . . . . . . . . . . . . 18
⢠(ð¥ â (ð ClWWalksN ðº) â ð = (â¯âð¥)) |
12 | 11, 1 | eleq2s 2852 |
. . . . . . . . . . . . . . . . 17
⢠(ð¥ â ð â ð = (â¯âð¥)) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . . . 16
⢠((ð¥ â ð ⧠ðŠ â ð) â ð = (â¯âð¥)) |
14 | 13 | adantr 482 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ)) â ð = (â¯âð¥)) |
15 | 7 | clwwlknwrd 29027 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ðŠ â (ð ClWWalksN ðº) â ðŠ â Word (Vtxâðº)) |
16 | 15, 1 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ðŠ â ð â ðŠ â Word (Vtxâðº)) |
17 | 16 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
⢠((ð¥ â ð ⧠ðŠ â ð) â ðŠ â Word (Vtxâðº)) |
18 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ)) â ðŠ â Word (Vtxâðº)) |
19 | 18 | adantl 483 |
. . . . . . . . . . . . . . . . 17
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â ðŠ â Word (Vtxâðº)) |
20 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â (â¯âð¥) = (â¯âðŠ)) |
21 | 19, 20 | cshwcshid 14725 |
. . . . . . . . . . . . . . . 16
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â ((ð â (0...(â¯âðŠ)) ⧠ð¥ = (ðŠ cyclShift ð)) â âð â (0...(â¯âð¥))ðŠ = (ð¥ cyclShift ð))) |
22 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð = (â¯âð¥) â (0...ð) = (0...(â¯âð¥))) |
23 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . 20
â¢
((â¯âð¥) =
(â¯âðŠ) â
(0...(â¯âð¥)) =
(0...(â¯âðŠ))) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ)) â (0...(â¯âð¥)) = (0...(â¯âðŠ))) |
25 | 22, 24 | sylan9eq 2793 |
. . . . . . . . . . . . . . . . . 18
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â (0...ð) = (0...(â¯âðŠ))) |
26 | 25 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â (ð â (0...ð) â ð â (0...(â¯âðŠ)))) |
27 | 26 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â ((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) â (ð â (0...(â¯âðŠ)) ⧠ð¥ = (ðŠ cyclShift ð)))) |
28 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . 17
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â (0...ð) = (0...(â¯âð¥))) |
29 | 28 | rexeqdv 3313 |
. . . . . . . . . . . . . . . 16
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â (âð â (0...ð)ðŠ = (ð¥ cyclShift ð) â âð â (0...(â¯âð¥))ðŠ = (ð¥ cyclShift ð))) |
30 | 21, 27, 29 | 3imtr4d 294 |
. . . . . . . . . . . . . . 15
⢠((ð = (â¯âð¥) ⧠((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ))) â ((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð))) |
31 | 14, 30 | mpancom 687 |
. . . . . . . . . . . . . 14
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ)) â ((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð))) |
32 | 31 | expd 417 |
. . . . . . . . . . . . 13
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ)) â (ð â (0...ð) â (ð¥ = (ðŠ cyclShift ð) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð)))) |
33 | 32 | rexlimdv 3147 |
. . . . . . . . . . . 12
⢠(((ð¥ â ð ⧠ðŠ â ð) ⧠(â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð))) |
34 | 33 | ex 414 |
. . . . . . . . . . 11
⢠((ð¥ â ð ⧠ðŠ â ð) â ((â¯âð¥) = (â¯âðŠ) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð)))) |
35 | 34 | com23 86 |
. . . . . . . . . 10
⢠((ð¥ â ð ⧠ðŠ â ð) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((â¯âð¥) = (â¯âðŠ) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð)))) |
36 | 35 | 3impia 1118 |
. . . . . . . . 9
⢠((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((â¯âð¥) = (â¯âðŠ) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð))) |
37 | 36 | imp 408 |
. . . . . . . 8
⢠(((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) ⧠(â¯âð¥) = (â¯âðŠ)) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð)) |
38 | | oveq2 7369 |
. . . . . . . . . 10
⢠(ð = ð â (ð¥ cyclShift ð) = (ð¥ cyclShift ð)) |
39 | 38 | eqeq2d 2744 |
. . . . . . . . 9
⢠(ð = ð â (ðŠ = (ð¥ cyclShift ð) â ðŠ = (ð¥ cyclShift ð))) |
40 | 39 | cbvrexvw 3225 |
. . . . . . . 8
â¢
(âð â
(0...ð)ðŠ = (ð¥ cyclShift ð) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð)) |
41 | 37, 40 | sylibr 233 |
. . . . . . 7
⢠(((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) ⧠(â¯âð¥) = (â¯âðŠ)) â âð â (0...ð)ðŠ = (ð¥ cyclShift ð)) |
42 | 5, 6, 41 | 3jca 1129 |
. . . . . 6
⢠(((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) ⧠(â¯âð¥) = (â¯âðŠ)) â (ðŠ â ð ⧠ð¥ â ð ⧠âð â (0...ð)ðŠ = (ð¥ cyclShift ð))) |
43 | 1, 2 | erclwwlkneq 29060 |
. . . . . . 7
⢠((ðŠ â V ⧠ð¥ â V) â (ðŠ ⌠ð¥ â (ðŠ â ð ⧠ð¥ â ð ⧠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)))) |
44 | 43 | ancoms 460 |
. . . . . 6
⢠((ð¥ â V ⧠ðŠ â V) â (ðŠ ⌠ð¥ â (ðŠ â ð ⧠ð¥ â ð ⧠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)))) |
45 | 42, 44 | syl5ibr 246 |
. . . . 5
⢠((ð¥ â V ⧠ðŠ â V) â (((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) ⧠(â¯âð¥) = (â¯âðŠ)) â ðŠ ⌠ð¥)) |
46 | 45 | expd 417 |
. . . 4
⢠((ð¥ â V ⧠ðŠ â V) â ((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((â¯âð¥) = (â¯âðŠ) â ðŠ ⌠ð¥))) |
47 | 4, 46 | sylbid 239 |
. . 3
⢠((ð¥ â V ⧠ðŠ â V) â (ð¥ ⌠ðŠ â ((â¯âð¥) = (â¯âðŠ) â ðŠ ⌠ð¥))) |
48 | 3, 47 | mpdd 43 |
. 2
⢠((ð¥ â V ⧠ðŠ â V) â (ð¥ ⌠ðŠ â ðŠ ⌠ð¥)) |
49 | 48 | el2v 3455 |
1
⢠(ð¥ ⌠ðŠ â ðŠ ⌠ð¥) |