Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . 5
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ð â (0...ð)) |
2 | 1 | anim1i 615 |
. . . 4
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð â (0...ð) ⧠(ð â ð ⧠ð¥ â ð))) |
3 | 2 | adantr 481 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â (ð â (0...ð) ⧠(ð â ð ⧠ð¥ â ð))) |
4 | | simpr 485 |
. . . . 5
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ð = (ð¥ cyclShift ð)) |
5 | 4 | adantr 481 |
. . . 4
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â ð = (ð¥ cyclShift ð)) |
6 | 5 | anim1i 615 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â (ð = (ð¥ cyclShift ð) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð))) |
7 | | erclwwlkn1.w |
. . . 4
⢠ð = (ð ClWWalksN ðº) |
8 | 7 | eleclclwwlknlem1 29310 |
. . 3
⢠((ð â (0...ð) ⧠(ð â ð ⧠ð¥ â ð)) â ((ð = (ð¥ cyclShift ð) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â âð â (0...ð)ð = (ð cyclShift ð))) |
9 | 3, 6, 8 | sylc 65 |
. 2
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð¥ cyclShift ð)) â âð â (0...ð)ð = (ð cyclShift ð)) |
10 | | eqid 2732 |
. . . . . . . . . . . 12
â¢
(Vtxâðº) =
(Vtxâðº) |
11 | 10 | clwwlknbp 29285 |
. . . . . . . . . . 11
⢠(ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
12 | 11, 7 | eleq2s 2851 |
. . . . . . . . . 10
⢠(ð¥ â ð â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
13 | | fznn0sub2 13607 |
. . . . . . . . . . . 12
⢠(ð â (0...ð) â (ð â ð) â (0...ð)) |
14 | | oveq1 7415 |
. . . . . . . . . . . . 13
â¢
((â¯âð¥) =
ð â
((â¯âð¥) â
ð) = (ð â ð)) |
15 | 14 | eleq1d 2818 |
. . . . . . . . . . . 12
â¢
((â¯âð¥) =
ð â
(((â¯âð¥) â
ð) â (0...ð) â (ð â ð) â (0...ð))) |
16 | 13, 15 | imbitrrid 245 |
. . . . . . . . . . 11
â¢
((â¯âð¥) =
ð â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
17 | 16 | adantl 482 |
. . . . . . . . . 10
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
18 | 12, 17 | syl 17 |
. . . . . . . . 9
⢠(ð¥ â ð â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
19 | 18 | adantl 482 |
. . . . . . . 8
⢠((ð â ð ⧠ð¥ â ð) â (ð â (0...ð) â ((â¯âð¥) â ð) â (0...ð))) |
20 | 19 | com12 32 |
. . . . . . 7
⢠(ð â (0...ð) â ((ð â ð ⧠ð¥ â ð) â ((â¯âð¥) â ð) â (0...ð))) |
21 | 20 | adantr 481 |
. . . . . 6
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ((ð â ð ⧠ð¥ â ð) â ((â¯âð¥) â ð) â (0...ð))) |
22 | 21 | imp 407 |
. . . . 5
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â ((â¯âð¥) â ð) â (0...ð)) |
23 | 22 | adantr 481 |
. . . 4
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â ((â¯âð¥) â ð) â (0...ð)) |
24 | | simpr 485 |
. . . . . 6
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð â ð ⧠ð¥ â ð)) |
25 | 24 | ancomd 462 |
. . . . 5
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð¥ â ð ⧠ð â ð)) |
26 | 25 | adantr 481 |
. . . 4
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â (ð¥ â ð ⧠ð â ð)) |
27 | 23, 26 | jca 512 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â (((â¯âð¥) â ð) â (0...ð) ⧠(ð¥ â ð ⧠ð â ð))) |
28 | | simpll 765 |
. . . . . . . . . . . . 13
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â (0...ð)) â ð¥ â Word (Vtxâðº)) |
29 | | oveq2 7416 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â (0...ð) = (0...(â¯âð¥))) |
30 | 29 | eleq2d 2819 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (ð â (0...ð) â ð â (0...(â¯âð¥)))) |
31 | 30 | eqcoms 2740 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð¥) =
ð â (ð â (0...ð) â ð â (0...(â¯âð¥)))) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â (0...ð) â ð â (0...(â¯âð¥)))) |
33 | 32 | biimpa 477 |
. . . . . . . . . . . . 13
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â (0...ð)) â ð â (0...(â¯âð¥))) |
34 | 28, 33 | jca 512 |
. . . . . . . . . . . 12
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â (0...ð)) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥)))) |
35 | 34 | ex 413 |
. . . . . . . . . . 11
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â (0...ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
36 | 12, 35 | syl 17 |
. . . . . . . . . 10
⢠(ð¥ â ð â (ð â (0...ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
37 | 36 | adantl 482 |
. . . . . . . . 9
⢠((ð â ð ⧠ð¥ â ð) â (ð â (0...ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
38 | 37 | com12 32 |
. . . . . . . 8
⢠(ð â (0...ð) â ((ð â ð ⧠ð¥ â ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
39 | 38 | adantr 481 |
. . . . . . 7
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â ((ð â ð ⧠ð¥ â ð) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))))) |
40 | 39 | imp 407 |
. . . . . 6
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥)))) |
41 | 4 | eqcomd 2738 |
. . . . . . 7
⢠((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) â (ð¥ cyclShift ð) = ð) |
42 | 41 | adantr 481 |
. . . . . 6
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð¥ cyclShift ð) = ð) |
43 | | oveq1 7415 |
. . . . . . . 8
⢠(ð = (ð¥ cyclShift ð) â (ð cyclShift ((â¯âð¥) â ð)) = ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð))) |
44 | 43 | eqcoms 2740 |
. . . . . . 7
⢠((ð¥ cyclShift ð) = ð â (ð cyclShift ((â¯âð¥) â ð)) = ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð))) |
45 | | elfzelz 13500 |
. . . . . . . 8
⢠(ð â
(0...(â¯âð¥))
â ð â
â€) |
46 | | 2cshwid 14763 |
. . . . . . . 8
⢠((ð¥ â Word (Vtxâðº) ⧠ð â â€) â ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð)) = ð¥) |
47 | 45, 46 | sylan2 593 |
. . . . . . 7
⢠((ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))) â ((ð¥ cyclShift ð) cyclShift ((â¯âð¥) â ð)) = ð¥) |
48 | 44, 47 | sylan9eqr 2794 |
. . . . . 6
⢠(((ð¥ â Word (Vtxâðº) ⧠ð â (0...(â¯âð¥))) ⧠(ð¥ cyclShift ð) = ð) â (ð cyclShift ((â¯âð¥) â ð)) = ð¥) |
49 | 40, 42, 48 | syl2anc 584 |
. . . . 5
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (ð cyclShift ((â¯âð¥) â ð)) = ð¥) |
50 | 49 | eqcomd 2738 |
. . . 4
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â ð¥ = (ð cyclShift ((â¯âð¥) â ð))) |
51 | 50 | anim1i 615 |
. . 3
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â (ð¥ = (ð cyclShift ((â¯âð¥) â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð))) |
52 | 7 | eleclclwwlknlem1 29310 |
. . 3
â¢
((((â¯âð¥)
â ð) â
(0...ð) ⧠(ð¥ â ð ⧠ð â ð)) â ((ð¥ = (ð cyclShift ((â¯âð¥) â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â âð â (0...ð)ð = (ð¥ cyclShift ð))) |
53 | 27, 51, 52 | sylc 65 |
. 2
⢠((((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) ⧠âð â (0...ð)ð = (ð cyclShift ð)) â âð â (0...ð)ð = (ð¥ cyclShift ð)) |
54 | 9, 53 | impbida 799 |
1
⢠(((ð â (0...ð) ⧠ð = (ð¥ cyclShift ð)) ⧠(ð â ð ⧠ð¥ â ð)) â (âð â (0...ð)ð = (ð¥ cyclShift ð) â âð â (0...ð)ð = (ð cyclShift ð))) |