Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . . . 5
⢠ð = (ð ClWWalksN ðº) |
2 | | erclwwlkn.r |
. . . . 5
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð â§ ð¢ â ð â§ âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
3 | 1, 2 | eclclwwlkn1 29872 |
. . . 4
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â
âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
4 | | rabeq 3441 |
. . . . . . . . . 10
⢠(ð = (ð ClWWalksN ðº) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⢠(((ðº â UMGraph â§ ð â â) â§ ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
6 | | prmnn 16636 |
. . . . . . . . . . . 12
⢠(ð â â â ð â
â) |
7 | 6 | nnnn0d 12554 |
. . . . . . . . . . 11
⢠(ð â â â ð â
â0) |
8 | 7 | adantl 481 |
. . . . . . . . . 10
⢠((ðº â UMGraph â§ ð â â) â ð â
â0) |
9 | 1 | eleq2i 2820 |
. . . . . . . . . . 11
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
10 | 9 | biimpi 215 |
. . . . . . . . . 10
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
11 | | clwwlknscsh 29859 |
. . . . . . . . . 10
⢠((ð â â0
â§ ð¥ â (ð ClWWalksN ðº)) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
12 | 8, 10, 11 | syl2an 595 |
. . . . . . . . 9
⢠(((ðº â UMGraph â§ ð â â) â§ ð¥ â ð) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
13 | 5, 12 | eqtrd 2767 |
. . . . . . . 8
⢠(((ðº â UMGraph â§ ð â â) â§ ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
14 | 13 | eqeq2d 2738 |
. . . . . . 7
⢠(((ðº â UMGraph â§ ð â â) â§ ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
15 | 6 | adantl 481 |
. . . . . . . . . . . 12
⢠((ðº â UMGraph â§ ð â â) â ð â
â) |
16 | | simpll 766 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â ð¥ â Word (Vtxâðº)) |
17 | | elnnne0 12508 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â â â (ð â â0
â§ ð â
0)) |
18 | | eqeq1 2731 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = (â¯âð¥) â (ð = 0 â (â¯âð¥) = 0)) |
19 | 18 | eqcoms 2735 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
((â¯âð¥) =
ð â (ð = 0 â (â¯âð¥) = 0)) |
20 | | hasheq0 14346 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ð¥ â Word (Vtxâðº) â ((â¯âð¥) = 0 â ð¥ = â
)) |
21 | 19, 20 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . . . . 20
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð = 0 â ð¥ = â
)) |
22 | 21 | necon3bid 2980 |
. . . . . . . . . . . . . . . . . . 19
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð â 0 â ð¥ â â
)) |
23 | 22 | biimpcd 248 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â 0 â ((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ð¥ â â
)) |
24 | 17, 23 | simplbiim 504 |
. . . . . . . . . . . . . . . . 17
⢠(ð â â â ((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ð¥ â â
)) |
25 | 24 | impcom 407 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â ð¥ â â
) |
26 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â (â¯âð¥) = ð) |
27 | 26 | eqcomd 2733 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â ð = (â¯âð¥)) |
28 | 16, 25, 27 | 3jca 1126 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥))) |
29 | 28 | ex 412 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð â â â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥)))) |
30 | | eqid 2727 |
. . . . . . . . . . . . . . 15
â¢
(Vtxâðº) =
(Vtxâðº) |
31 | 30 | clwwlknbp 29832 |
. . . . . . . . . . . . . 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 406 |
. . . . . . . . . 10
⢠(((ðº â UMGraph â§ ð â â) â§ ð¥ â ð) â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥))) |
36 | | scshwfzeqfzo 14801 |
. . . . . . . . . 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 2738 |
. . . . . . . 8
⢠(((ðº â UMGraph â§ ð â â) â§ ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)})) |
39 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)})) |
40 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) â§ ð¥ â ((â¯âð¥) ClWWalksN ðº)) â§ (ðº â UMGraph â§ (â¯âð¥) â â)) â ðº â
UMGraph) |
41 | | prmuz2 16658 |
. . . . . . . . . . . . . . . . . . 19
â¢
((â¯âð¥)
â â â (â¯âð¥) â
(â€â¥â2)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⢠((ðº â UMGraph â§
(â¯âð¥) â
â) â (â¯âð¥) â
(â€â¥â2)) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) â§ ð¥ â ((â¯âð¥) ClWWalksN ðº)) â§ (ðº â UMGraph â§ (â¯âð¥) â â)) â
(â¯âð¥) â
(â€â¥â2)) |
44 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) â§ ð¥ â ((â¯âð¥) ClWWalksN ðº)) â§ (ðº â UMGraph â§ (â¯âð¥) â â)) â ð¥ â ((â¯âð¥) ClWWalksN ðº)) |
45 | | umgr2cwwkdifex 29862 |
. . . . . . . . . . . . . . . . 17
⢠((ðº â UMGraph â§
(â¯âð¥) â
(â€â¥â2) â§ ð¥ â ((â¯âð¥) ClWWalksN ðº)) â âð â (0..^(â¯âð¥))(ð¥âð) â (ð¥â0)) |
46 | 40, 43, 44, 45 | syl3anc 1369 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ ð¥ â ((â¯âð¥) ClWWalksN ðº)) â§ (ðº â UMGraph â§ (â¯âð¥) â â)) â
âð â
(0..^(â¯âð¥))(ð¥âð) â (ð¥â0)) |
47 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = ð â (ð¥ cyclShift ð) = (ð¥ cyclShift ð)) |
48 | 47 | eqeq2d 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ð = ð â (ðŠ = (ð¥ cyclShift ð) â ðŠ = (ð¥ cyclShift ð))) |
49 | 48 | cbvrexvw 3230 |
. . . . . . . . . . . . . . . . . . . 20
â¢
(âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)) |
50 | | eqeq1 2731 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â ð¢ = (ð¥ cyclShift ð))) |
51 | | eqcom 2734 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð¢ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢) |
52 | 50, 51 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢)) |
53 | 52 | rexbidv 3173 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
54 | 49, 53 | bitrid 283 |
. . . . . . . . . . . . . . . . . . 19
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
55 | 54 | cbvrabv 3437 |
. . . . . . . . . . . . . . . . . 18
⢠{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} = {ð¢ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢} |
56 | 55 | cshwshashnsame 17064 |
. . . . . . . . . . . . . . . . 17
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â
(âð â
(0..^(â¯âð¥))(ð¥âð) â (ð¥â0) â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
57 | 56 | ad2ant2rl 748 |
. . . . . . . . . . . . . . . 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 2789 |
. . . . . . . . . . . . . 14
⢠((((ð¥ â Word (Vtxâðº) â§ ð¥ â ((â¯âð¥) ClWWalksN ðº)) â§ (ðº â UMGraph â§ (â¯âð¥) â â)) â§ ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â (â¯âð) = (â¯âð¥)) |
60 | 59 | exp41 434 |
. . . . . . . . . . . . 13
⢠(ð¥ â Word (Vtxâðº) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph â§ (â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥))))) |
61 | 60 | adantr 480 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph â§ (â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥))))) |
62 | | oveq1 7421 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (ð ClWWalksN ðº) = ((â¯âð¥) ClWWalksN ðº)) |
63 | 62 | eleq2d 2814 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â (ð¥ â (ð ClWWalksN ðº) â ð¥ â ((â¯âð¥) ClWWalksN ðº))) |
64 | | eleq1 2816 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â (ð â â â (â¯âð¥) â
â)) |
65 | 64 | anbi2d 628 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â ((ðº â UMGraph â§ ð â â) â (ðº â UMGraph â§ (â¯âð¥) â
â))) |
66 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ð = (â¯âð¥) â (0..^ð) = (0..^(â¯âð¥))) |
67 | 66 | rexeqdv 3321 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð = (â¯âð¥) â (âð â (0..^ð)ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð))) |
68 | 67 | rabbidv 3435 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = (â¯âð¥) â {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) |
69 | 68 | eqeq2d 2738 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)})) |
70 | | eqeq2 2739 |
. . . . . . . . . . . . . . . . 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 2735 |
. . . . . . . . . . . . 13
â¢
((â¯âð¥) =
ð â ((ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph â§ ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph â§ (â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥)))))) |
75 | 74 | adantl 481 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ((ð¥ â (ð ClWWalksN ðº) â ((ðº â UMGraph â§ ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) â (ð¥ â ((â¯âð¥) ClWWalksN ðº) â ((ðº â UMGraph â§ (â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = (â¯âð¥)))))) |
76 | 61, 75 | mpbird 257 |
. . . . . . . . . . 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 2846 |
. . . . . . . . 9
⢠(ð¥ â ð â ((ðº â UMGraph â§ ð â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð))) |
79 | 78 | impcom 407 |
. . . . . . . 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 3150 |
. . . . 5
⢠((ðº â UMGraph â§ ð â â) â
(âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â (â¯âð) = ð)) |
83 | 82 | com12 32 |
. . . 4
â¢
(âð¥ â
ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((ðº â UMGraph â§ ð â â) â (â¯âð) = ð)) |
84 | 3, 83 | biimtrdi 252 |
. . 3
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â ((ðº â UMGraph â§ ð â â) â
(â¯âð) = ð))) |
85 | 84 | pm2.43i 52 |
. 2
⢠(ð â (ð / ⌠) â ((ðº â UMGraph â§ ð â â) â
(â¯âð) = ð)) |
86 | 85 | com12 32 |
1
⢠((ðº â UMGraph â§ ð â â) â (ð â (ð / ⌠) â
(â¯âð) = ð)) |