Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . 5
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ð â (0...ð)) |
2 | 1 | anim1i 616 |
. . . 4
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð â (0...ð) ⧠(ð â ð ⧠ð¥ â ð))) |
3 | 2 | adantr 482 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â (ð â (0...ð) ⧠(ð â ð ⧠ð¥ â ð))) |
4 | | simpr 486 |
. . . . 5
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ð = (ð¥ cyclShift ð)) |
5 | 4 | adantr 482 |
. . . 4
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â ð = (ð¥ cyclShift ð)) |
6 | 5 | anim1i 616 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â (ð = (ð¥ cyclShift ð) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð))) |
7 | | erclwwlkn1.w |
. . . 4
⢠ð = (ð ClWWalksN ðº) |
8 | 7 | eleclclwwlknlem1 29053 |
. . 3
⢠((ð â (0...ð) ⧠(ð â ð ⧠ð¥ â ð)) â ((ð = (ð¥ cyclShift ð) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â âð â (0...ð)ð = (ð cyclShift ð))) |
9 | 3, 6, 8 | sylc 65 |
. 2
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â âð â (0...ð)ð = (ð cyclShift ð)) |
10 | | eqid 2733 |
. . . . . . . . . . . 12
â¢
(Vtxâðº) =
(Vtxâðº) |
11 | 10 | clwwlknbp 29028 |
. . . . . . . . . . 11
⢠(ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
12 | 11, 7 | eleq2s 2852 |
. . . . . . . . . 10
⢠(ð¥ â ð â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
13 | | fznn0sub2 13557 |
. . . . . . . . . . . 12
⢠(ð â (0...ð) â (ð â ð) â (0...ð)) |
14 | | oveq1 7368 |
. . . . . . . . . . . . 13
â¢
((â¯âð¥) =
ð â
((â¯âð¥) â
ð) = (ð â ð)) |
15 | 14 | eleq1d 2819 |
. . . . . . . . . . . 12
â¢
((â¯âð¥) =
ð â
(((â¯âð¥) â
ð) â (0...ð) â (ð â ð) â (0...ð))) |
16 | 13, 15 | syl5ibr 246 |
. . . . . . . . . . 11
â¢
((â¯âð¥) =
ð â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
17 | 16 | adantl 483 |
. . . . . . . . . 10
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
18 | 12, 17 | syl 17 |
. . . . . . . . 9
⢠(ð¥ â ð â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
19 | 18 | adantl 483 |
. . . . . . . 8
⢠((ð â ð ⧠ð¥ â ð) â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
20 | 19 | com12 32 |
. . . . . . 7
⢠(ð â (0...ð) â ((ð â ð ⧠ð¥ â ð) â ((â¯âð¥) â ð) â (0...ð))) |
21 | 20 | adantr 482 |
. . . . . 6
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ((ð â ð ⧠ð¥ â ð) â ((â¯âð¥) â ð) â (0...ð))) |
22 | 21 | imp 408 |
. . . . 5
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â ((â¯âð¥) â ð) â (0...ð)) |
23 | 22 | adantr 482 |
. . . 4
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â ((â¯âð¥) â ð) â (0...ð)) |
24 | | simpr 486 |
. . . . . 6
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð â ð ⧠ð¥ â ð)) |
25 | 24 | ancomd 463 |
. . . . 5
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð¥ â ð ⧠ð â ð)) |
26 | 25 | adantr 482 |
. . . 4
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â (ð¥ â ð ⧠ð â ð)) |
27 | 23, 26 | jca 513 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â (((â¯âð¥) â ð) â (0...ð) ⧠(ð¥ â ð ⧠ð â ð))) |
28 | | simpll 766 |
. . . . . . . . . . . . 13
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â (0...ð)) â ð¥ â Word (Vtxâðº)) |
29 | | oveq2 7369 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â (0...ð) = (0...(â¯âð¥))) |
30 | 29 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (ð â (0...ð) â ð â (0...(â¯âð¥)))) |
31 | 30 | eqcoms 2741 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð¥) =
ð â (ð â (0...ð) â ð â (0...(â¯âð¥)))) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â (0...ð) â ð â (0...(â¯âð¥)))) |
33 | 32 | biimpa 478 |
. . . . . . . . . . . . 13
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â (0...ð)) â ð â (0...(â¯âð¥))) |
34 | 28, 33 | jca 513 |
. . . . . . . . . . . 12
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â (0...ð)) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥)))) |
35 | 34 | ex 414 |
. . . . . . . . . . 11
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â (0...ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
36 | 12, 35 | syl 17 |
. . . . . . . . . 10
⢠(ð¥ â ð â (ð â (0...ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
37 | 36 | adantl 483 |
. . . . . . . . 9
⢠((ð â ð ⧠ð¥ â ð) â (ð â (0...ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
38 | 37 | com12 32 |
. . . . . . . 8
⢠(ð â (0...ð) â ((ð â ð ⧠ð¥ â ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
39 | 38 | adantr 482 |
. . . . . . 7
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ((ð â ð ⧠ð¥ â ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
40 | 39 | imp 408 |
. . . . . 6
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥)))) |
41 | 4 | eqcomd 2739 |
. . . . . . 7
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â (ð¥ cyclShift ð) = ð) |
42 | 41 | adantr 482 |
. . . . . 6
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð¥ cyclShift ð) = ð) |
43 | | oveq1 7368 |
. . . . . . . 8
⢠(ð = (ð¥ cyclShift ð) â (ð cyclShift ((â¯âð¥) â ð)) = ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð))) |
44 | 43 | eqcoms 2741 |
. . . . . . 7
⢠((ð¥ cyclShift ð) = ð â (ð cyclShift ((â¯âð¥) â ð)) = ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð))) |
45 | | elfzelz 13450 |
. . . . . . . 8
⢠(ð â
(0...(â¯âð¥))
â ð â
â€) |
46 | | 2cshwid 14711 |
. . . . . . . 8
⢠((ð¥ â Word (Vtxâðº) ⧠ð â â€) â ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð)) = ð¥) |
47 | 45, 46 | sylan2 594 |
. . . . . . 7
⢠((ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))) â ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð)) = ð¥) |
48 | 44, 47 | sylan9eqr 2795 |
. . . . . 6
⢠(((ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))) ⧠(ð¥ cyclShift ð) = ð) â (ð cyclShift ((â¯âð¥) â ð)) = ð¥) |
49 | 40, 42, 48 | syl2anc 585 |
. . . . 5
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð cyclShift ((â¯âð¥) â ð)) = ð¥) |
50 | 49 | eqcomd 2739 |
. . . 4
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â ð¥ = (ð cyclShift ((â¯âð¥) â ð))) |
51 | 50 | anim1i 616 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â (ð¥ = (ð cyclShift ((â¯âð¥) â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð))) |
52 | 7 | eleclclwwlknlem1 29053 |
. . 3
â¢
((((â¯âð¥)
â ð) â
(0...ð) ⧠(ð¥ â ð ⧠ð â ð)) â ((ð¥ = (ð cyclShift ((â¯âð¥) â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â âð â (0...ð)ð = (ð¥ cyclShift ð))) |
53 | 27, 51, 52 | sylc 65 |
. 2
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â âð â (0...ð)ð = (ð¥ cyclShift ð)) |
54 | 9, 53 | impbida 800 |
1
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (âð â (0...ð)ð = (ð¥ cyclShift ð) â âð â (0...ð)ð = (ð cyclShift ð))) |