Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . . . 5
⢠ð = (ð ClWWalksN ðº) |
2 | | erclwwlkn.r |
. . . . 5
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð ⧠ð¢ â ð ⧠âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
3 | 1, 2 | eclclwwlkn1 29019 |
. . . 4
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â
âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
4 | | rabeq 3421 |
. . . . . . . . . 10
⢠(ð = (ð ClWWalksN ðº) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
6 | | prmnn 16550 |
. . . . . . . . . . . 12
⢠(ð â â â ð â
â) |
7 | 6 | nnnn0d 12473 |
. . . . . . . . . . 11
⢠(ð â â â ð â
â0) |
8 | 7 | adantl 482 |
. . . . . . . . . 10
⢠((ðº â UMGraph ⧠ð â â) â ð â
â0) |
9 | 1 | eleq2i 2829 |
. . . . . . . . . . 11
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
10 | 9 | biimpi 215 |
. . . . . . . . . 10
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
11 | | clwwlknscsh 29006 |
. . . . . . . . . 10
⢠((ð â â0
⧠ð¥ â (ð ClWWalksN ðº)) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
12 | 8, 10, 11 | syl2an 596 |
. . . . . . . . 9
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
13 | 5, 12 | eqtrd 2776 |
. . . . . . . 8
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
14 | 13 | eqeq2d 2747 |
. . . . . . 7
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
15 | 6 | adantl 482 |
. . . . . . . . . . . 12
⢠((ðº â UMGraph ⧠ð â â) â ð â
â) |
16 | | simpll 765 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â ð¥ â Word (Vtxâðº)) |
17 | | elnnne0 12427 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â â â (ð â â0
⧠ð â
0)) |
18 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = (â¯âð¥) â (ð = 0 â (â¯âð¥) = 0)) |
19 | 18 | eqcoms 2744 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
((â¯âð¥) =
ð â (ð = 0 â (â¯âð¥) = 0)) |
20 | | hasheq0 14263 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ð¥ â Word (Vtxâðº) â ((â¯âð¥) = 0 â ð¥ = â
)) |
21 | 19, 20 | sylan9bbr 511 |
. . . . . . . . . . . . . . . . . . . 20
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð = 0 â ð¥ = â
)) |
22 | 21 | necon3bid 2988 |
. . . . . . . . . . . . . . . . . . 19
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â 0 â ð¥ â â
)) |
23 | 22 | biimpcd 248 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â 0 â ((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ð¥ â â
)) |
24 | 17, 23 | simplbiim 505 |
. . . . . . . . . . . . . . . . 17
⢠(ð â â â ((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ð¥ â â
)) |
25 | 24 | impcom 408 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â ð¥ â â
) |
26 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â (â¯âð¥) = ð) |
27 | 26 | eqcomd 2742 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â ð = (â¯âð¥)) |
28 | 16, 25, 27 | 3jca 1128 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) ⧠ð â â) â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥))) |
29 | 28 | ex 413 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð â â â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
30 | | eqid 2736 |
. . . . . . . . . . . . . . 15
â¢
(Vtxâðº) =
(Vtxâðº) |
31 | 30 | clwwlknbp 28979 |
. . . . . . . . . . . . . 14
⢠(ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð)) |
32 | 29, 31 | syl11 33 |
. . . . . . . . . . . . 13
⢠(ð â â â (ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
33 | 9, 32 | biimtrid 241 |
. . . . . . . . . . . 12
⢠(ð â â â (ð¥ â ð â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
34 | 15, 33 | syl 17 |
. . . . . . . . . . 11
⢠((ðº â UMGraph ⧠ð â â) â (ð¥ â ð â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)))) |
35 | 34 | imp 407 |
. . . . . . . . . 10
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â (ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥))) |
36 | | scshwfzeqfzo 14715 |
. . . . . . . . . 10
⢠((ð¥ â Word (Vtxâðº) ⧠ð¥ â â
⧠ð = (â¯âð¥)) â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)}) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)}) |
38 | 37 | eqeq2d 2747 |
. . . . . . . 8
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)})) |
39 | | fveq2 6842 |
. . . . . . . . . . . . . . 15
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)})) |
40 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) â ðº â
UMGraph) |
41 | | prmuz2 16572 |
. . . . . . . . . . . . . . . . . . 19
â¢
((â¯âð¥)
â â â (â¯âð¥) â
(â€â¥â2)) |
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⢠((ðº â UMGraph â§
(â¯âð¥) â
â) â (â¯âð¥) â
(â€â¥â2)) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) â
(â¯âð¥) â
(â€â¥â2)) |
44 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) â ð¥ â ((â¯âð¥) ClWWalksN ðº)) |
45 | | umgr2cwwkdifex 29009 |
. . . . . . . . . . . . . . . . 17
⢠((ðº â UMGraph â§
(â¯âð¥) â
(â€â¥â2) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) â âð â (0..^(â¯âð¥))(ð¥âð) â (ð¥â0)) |
46 | 40, 43, 44, 45 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) â
âð â
(0..^(â¯âð¥))(ð¥âð) â (ð¥â0)) |
47 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = ð â (ð¥ cyclShift ð) = (ð¥ cyclShift ð)) |
48 | 47 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ð = ð â (ðŠ = (ð¥ cyclShift ð) â ðŠ = (ð¥ cyclShift ð))) |
49 | 48 | cbvrexvw 3226 |
. . . . . . . . . . . . . . . . . . . 20
â¢
(âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)) |
50 | | eqeq1 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â ð¢ = (ð¥ cyclShift ð))) |
51 | | eqcom 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð¢ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢) |
52 | 50, 51 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢)) |
53 | 52 | rexbidv 3175 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
54 | 49, 53 | bitrid 282 |
. . . . . . . . . . . . . . . . . . 19
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
55 | 54 | cbvrabv 3417 |
. . . . . . . . . . . . . . . . . 18
⢠{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} = {ð¢ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢} |
56 | 55 | cshwshashnsame 16976 |
. . . . . . . . . . . . . . . . 17
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) â â) â
(âð â
(0..^(â¯âð¥))(ð¥âð) â (ð¥â0) â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
57 | 56 | ad2ant2rl 747 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) â
(âð â
(0..^(â¯âð¥))(ð¥âð) â (ð¥â0) â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
58 | 46, 57 | mpd 15 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) â
(â¯â{ðŠ â
Word (Vtxâðº) â£
âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥)) |
59 | 39, 58 | sylan9eqr 2798 |
. . . . . . . . . . . . . 14
⢠((((ð¥ â Word (Vtxâðº) ⧠ð¥ â ((â¯âð¥) ClWWalksN ðº)) ⧠(ðº â UMGraph ⧠(â¯âð¥) â â)) ⧠ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â (â¯âð) = (â¯âð¥)) |
60 | 59 | exp41 435 |
. . . . . . . . . . . . 13
⢠(ð¥ â Word (Vtxâðº) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥))))) |
61 | 60 | adantr 481 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥))))) |
62 | | oveq1 7364 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (ð ClWWalksN ðº) = ((â¯âð¥) ClWWalksN ðº)) |
63 | 62 | eleq2d 2823 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â (ð¥ â (ð ClWWalksN ðº) â ð¥ â ((â¯âð¥) ClWWalksN ðº))) |
64 | | eleq1 2825 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â (ð â â â (â¯âð¥) â
â)) |
65 | 64 | anbi2d 629 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â ((ðº â UMGraph ⧠ð â â) â (ðº â UMGraph ⧠(â¯âð¥) â
â))) |
66 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ð = (â¯âð¥) â (0..^ð) = (0..^(â¯âð¥))) |
67 | 66 | rexeqdv 3314 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð = (â¯âð¥) â (âð â (0..^ð)ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð))) |
68 | 67 | rabbidv 3415 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = (â¯âð¥) â {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) |
69 | 68 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)})) |
70 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â ((â¯âð) = ð â (â¯âð) = (â¯âð¥))) |
71 | 69, 70 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â ((ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥)))) |
72 | 65, 71 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â (((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)) â ((ðº â UMGraph ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥))))) |
73 | 63, 72 | imbi12d 344 |
. . . . . . . . . . . . . 14
⢠(ð = (â¯âð¥) â ((ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥)))))) |
74 | 73 | eqcoms 2744 |
. . . . . . . . . . . . 13
â¢
((â¯âð¥) =
ð â ((ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥)))))) |
75 | 74 | adantl 482 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â ((ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph ⧠(â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥)))))) |
76 | 61, 75 | mpbird 256 |
. . . . . . . . . . 11
⢠((ð¥ â Word (Vtxâðº) ⧠(â¯âð¥) = ð) â (ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)))) |
77 | 31, 76 | mpcom 38 |
. . . . . . . . . 10
⢠(ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) |
78 | 77, 1 | eleq2s 2855 |
. . . . . . . . 9
⢠(ð¥ â ð â ((ðº â UMGraph ⧠ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) |
79 | 78 | impcom 408 |
. . . . . . . 8
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)) |
80 | 38, 79 | sylbid 239 |
. . . . . . 7
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)) |
81 | 14, 80 | sylbid 239 |
. . . . . 6
⢠(((ðº â UMGraph ⧠ð â â) ⧠ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)) |
82 | 81 | rexlimdva 3152 |
. . . . 5
⢠((ðº â UMGraph ⧠ð â â) â
(âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)) |
83 | 82 | com12 32 |
. . . 4
â¢
(âð¥ â
ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((ðº â UMGraph ⧠ð â â) â (â¯âð) = ð)) |
84 | 3, 83 | syl6bi 252 |
. . 3
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â ((ðº â UMGraph ⧠ð â â) â
(â¯âð) = ð))) |
85 | 84 | pm2.43i 52 |
. 2
⢠(ð â (ð / ⌠) â ((ðº â UMGraph ⧠ð â â) â
(â¯âð) = ð)) |
86 | 85 | com12 32 |
1
⢠((ðº â UMGraph ⧠ð â â) â (ð â (ð / ⌠) â
(â¯âð) = ð)) |