Step | Hyp | Ref
| Expression |
1 | | vex 3473 |
. 2
⢠ð¥ â V |
2 | | vex 3473 |
. 2
⢠ðŠ â V |
3 | | vex 3473 |
. 2
⢠ð§ â V |
4 | | erclwwlkn.w |
. . . . . 6
⢠ð = (ð ClWWalksN ðº) |
5 | | erclwwlkn.r |
. . . . . 6
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð â§ ð¢ â ð â§ âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
6 | 4, 5 | erclwwlkneqlen 29852 |
. . . . 5
⢠((ð¥ â V â§ ðŠ â V) â (ð¥ ⌠ðŠ â (â¯âð¥) = (â¯âðŠ))) |
7 | 6 | 3adant3 1130 |
. . . 4
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ð¥ ⌠ðŠ â (â¯âð¥) = (â¯âðŠ))) |
8 | 4, 5 | erclwwlkneqlen 29852 |
. . . . . . 7
⢠((ðŠ â V â§ ð§ â V) â (ðŠ âŒ ð§ â (â¯âðŠ) = (â¯âð§))) |
9 | 8 | 3adant1 1128 |
. . . . . 6
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ðŠ âŒ ð§ â (â¯âðŠ) = (â¯âð§))) |
10 | 4, 5 | erclwwlkneq 29851 |
. . . . . . . 8
⢠((ðŠ â V â§ ð§ â V) â (ðŠ âŒ ð§ â (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)))) |
11 | 10 | 3adant1 1128 |
. . . . . . 7
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ðŠ âŒ ð§ â (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)))) |
12 | 4, 5 | erclwwlkneq 29851 |
. . . . . . . . . 10
⢠((ð¥ â V â§ ðŠ â V) â (ð¥ ⌠ðŠ â (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)))) |
13 | 12 | 3adant3 1130 |
. . . . . . . . 9
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ð¥ ⌠ðŠ â (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)))) |
14 | | simpr1 1192 |
. . . . . . . . . . . . . . 15
â¢
(((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â§ (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â ð¥ â ð) |
15 | | simplr2 1214 |
. . . . . . . . . . . . . . 15
â¢
(((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â§ (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â ð§ â ð) |
16 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⢠(ð = ð â (ðŠ cyclShift ð) = (ðŠ cyclShift ð)) |
17 | 16 | eqeq2d 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⢠(ð = ð â (ð¥ = (ðŠ cyclShift ð) â ð¥ = (ðŠ cyclShift ð))) |
18 | 17 | cbvrexvw 3230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
â¢
(âð â
(0...ð)ð¥ = (ðŠ cyclShift ð) â âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) |
19 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⢠(ð = ð â (ð§ cyclShift ð) = (ð§ cyclShift ð)) |
20 | 19 | eqeq2d 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⢠(ð = ð â (ðŠ = (ð§ cyclShift ð) â ðŠ = (ð§ cyclShift ð))) |
21 | 20 | cbvrexvw 3230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
â¢
(âð â
(0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ðŠ = (ð§ cyclShift ð)) |
22 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
â¢
(Vtxâðº) =
(Vtxâðº) |
23 | 22 | clwwlknbp 29819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠(ð§ â (ð ClWWalksN ðº) â (ð§ â Word (Vtxâðº) â§ (â¯âð§) = ð)) |
24 | | eqcom 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
â¢
((â¯âð§) =
ð â ð = (â¯âð§)) |
25 | 24 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
â¢
((â¯âð§) =
ð â ð = (â¯âð§)) |
26 | 23, 25 | simpl2im 503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠(ð§ â (ð ClWWalksN ðº) â ð = (â¯âð§)) |
27 | 26, 4 | eleq2s 2846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠(ð§ â ð â ð = (â¯âð§)) |
28 | 27 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â ð = (â¯âð§)) |
29 | 23 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⢠(ð§ â (ð ClWWalksN ðº) â ð§ â Word (Vtxâðº)) |
30 | 29, 4 | eleq2s 2846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⢠(ð§ â ð â ð§ â Word (Vtxâðº)) |
31 | 30 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â ð§ â Word (Vtxâðº)) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â ð§ â Word (Vtxâðº)) |
33 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) |
34 | 32, 33 | cshwcsh2id 14797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â (((ð â (0...(â¯âðŠ)) â§ ð¥ = (ðŠ cyclShift ð)) â§ (ð â (0...(â¯âð§)) â§ ðŠ = (ð§ cyclShift ð))) â âð â (0...(â¯âð§))ð¥ = (ð§ cyclShift ð))) |
35 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⢠(ð = (â¯âð§) â (0...ð) = (0...(â¯âð§))) |
36 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
â¢
((â¯âð§) =
(â¯âðŠ) â
(0...(â¯âð§)) =
(0...(â¯âðŠ))) |
37 | 36 | eqcoms 2735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
â¢
((â¯âðŠ) =
(â¯âð§) â
(0...(â¯âð§)) =
(0...(â¯âðŠ))) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
â¢
(((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â
(0...(â¯âð§)) =
(0...(â¯âðŠ))) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â (0...(â¯âð§)) = (0...(â¯âðŠ))) |
40 | 35, 39 | sylan9eq 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â (0...ð) = (0...(â¯âðŠ))) |
41 | 40 | eleq2d 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â (ð â (0...ð) â ð â (0...(â¯âðŠ)))) |
42 | 41 | anbi1d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â ((ð â (0...ð) â§ ð¥ = (ðŠ cyclShift ð)) â (ð â (0...(â¯âðŠ)) â§ ð¥ = (ðŠ cyclShift ð)))) |
43 | 35 | eleq2d 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⢠(ð = (â¯âð§) â (ð â (0...ð) â ð â (0...(â¯âð§)))) |
44 | 43 | anbi1d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠(ð = (â¯âð§) â ((ð â (0...ð) â§ ðŠ = (ð§ cyclShift ð)) â (ð â (0...(â¯âð§)) â§ ðŠ = (ð§ cyclShift ð)))) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â ((ð â (0...ð) â§ ðŠ = (ð§ cyclShift ð)) â (ð â (0...(â¯âð§)) â§ ðŠ = (ð§ cyclShift ð)))) |
46 | 42, 45 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â (((ð â (0...ð) â§ ð¥ = (ðŠ cyclShift ð)) â§ (ð â (0...ð) â§ ðŠ = (ð§ cyclShift ð))) â ((ð â (0...(â¯âðŠ)) â§ ð¥ = (ðŠ cyclShift ð)) â§ (ð â (0...(â¯âð§)) â§ ðŠ = (ð§ cyclShift ð))))) |
47 | 35 | rexeqdv 3321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠(ð = (â¯âð§) â (âð â (0...ð)ð¥ = (ð§ cyclShift ð) â âð â (0...(â¯âð§))ð¥ = (ð§ cyclShift ð))) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â (âð â (0...ð)ð¥ = (ð§ cyclShift ð) â âð â (0...(â¯âð§))ð¥ = (ð§ cyclShift ð))) |
49 | 34, 46, 48 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⢠((ð = (â¯âð§) â§ (((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)))) â (((ð â (0...ð) â§ ð¥ = (ðŠ cyclShift ð)) â§ (ð â (0...ð) â§ ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
50 | 28, 49 | mpancom 687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â (((ð â (0...ð) â§ ð¥ = (ðŠ cyclShift ð)) â§ (ð â (0...ð) â§ ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
51 | 50 | exp5l 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â (ð â (0...ð) â (ð¥ = (ðŠ cyclShift ð) â (ð â (0...ð) â (ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))))) |
52 | 51 | imp41 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
â¢
(((((((ð¥ â
ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â§ ð â (0...ð)) â§ ð¥ = (ðŠ cyclShift ð)) â§ ð â (0...ð)) â (ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
53 | 52 | rexlimdva 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
â¢
((((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â§ ð â (0...ð)) â§ ð¥ = (ðŠ cyclShift ð)) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
54 | 53 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
â¢
(((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â§ ð â (0...ð)) â (ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
55 | 54 | rexlimdva 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
56 | 21, 55 | syl7bi 255 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
57 | 18, 56 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠((((ð¥ â ð â§ ðŠ â ð) â§ ð§ â ð) â§ ((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ))) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
58 | 57 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠((ð¥ â ð â§ ðŠ â ð) â (ð§ â ð â (((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))))) |
59 | 58 | com15 101 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
(âð â
(0...ð)ðŠ = (ð§ cyclShift ð) â (ð§ â ð â (((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð â§ ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))))) |
60 | 59 | impcom 407 |
. . . . . . . . . . . . . . . . . . . 20
⢠((ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â (((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð â§ ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))))) |
61 | 60 | 3adant1 1128 |
. . . . . . . . . . . . . . . . . . 19
⢠((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â (((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð â§ ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))))) |
62 | 61 | impcom 407 |
. . . . . . . . . . . . . . . . . 18
â¢
((((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â§
(ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð â§ ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
63 | 62 | com13 88 |
. . . . . . . . . . . . . . . . 17
⢠((ð¥ â ð â§ ðŠ â ð) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
64 | 63 | 3impia 1115 |
. . . . . . . . . . . . . . . 16
⢠((ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
65 | 64 | impcom 407 |
. . . . . . . . . . . . . . 15
â¢
(((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â§ (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)) |
66 | 14, 15, 65 | 3jca 1126 |
. . . . . . . . . . . . . 14
â¢
(((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â§ (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â (ð¥ â ð â§ ð§ â ð â§ âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
67 | 4, 5 | erclwwlkneq 29851 |
. . . . . . . . . . . . . . 15
⢠((ð¥ â V â§ ð§ â V) â (ð¥ ⌠ð§ â (ð¥ â ð â§ ð§ â ð â§ âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
68 | 67 | 3adant2 1129 |
. . . . . . . . . . . . . 14
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ð¥ ⌠ð§ â (ð¥ â ð â§ ð§ â ð â§ âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
69 | 66, 68 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
â¢
(((((â¯âðŠ) = (â¯âð§) â§ (â¯âð¥) = (â¯âðŠ)) â§ (ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â§ (ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â ((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ð¥ ⌠ð§)) |
70 | 69 | exp31 419 |
. . . . . . . . . . . 12
â¢
(((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â
((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ((ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ð¥ ⌠ð§)))) |
71 | 70 | com24 95 |
. . . . . . . . . . 11
â¢
(((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â
((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ((ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ð¥ ⌠ð§)))) |
72 | 71 | ex 412 |
. . . . . . . . . 10
â¢
((â¯âðŠ) =
(â¯âð§) â
((â¯âð¥) =
(â¯âðŠ) â
((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ((ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ð¥ ⌠ð§))))) |
73 | 72 | com4t 93 |
. . . . . . . . 9
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ((ð¥ â ð â§ ðŠ â ð â§ âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((â¯âðŠ) = (â¯âð§) â ((â¯âð¥) = (â¯âðŠ) â ((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ð¥ ⌠ð§))))) |
74 | 13, 73 | sylbid 239 |
. . . . . . . 8
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ð¥ ⌠ðŠ â ((â¯âðŠ) = (â¯âð§) â ((â¯âð¥) = (â¯âðŠ) â ((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ð¥ ⌠ð§))))) |
75 | 74 | com25 99 |
. . . . . . 7
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ((ðŠ â ð â§ ð§ â ð â§ âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ((â¯âðŠ) = (â¯âð§) â ((â¯âð¥) = (â¯âðŠ) â (ð¥ ⌠ðŠ â ð¥ ⌠ð§))))) |
76 | 11, 75 | sylbid 239 |
. . . . . 6
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ðŠ âŒ ð§ â ((â¯âðŠ) = (â¯âð§) â ((â¯âð¥) = (â¯âðŠ) â (ð¥ ⌠ðŠ â ð¥ ⌠ð§))))) |
77 | 9, 76 | mpdd 43 |
. . . . 5
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ðŠ âŒ ð§ â ((â¯âð¥) = (â¯âðŠ) â (ð¥ ⌠ðŠ â ð¥ ⌠ð§)))) |
78 | 77 | com24 95 |
. . . 4
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ð¥ ⌠ðŠ â ((â¯âð¥) = (â¯âðŠ) â (ðŠ âŒ ð§ â ð¥ ⌠ð§)))) |
79 | 7, 78 | mpdd 43 |
. . 3
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â (ð¥ ⌠ðŠ â (ðŠ âŒ ð§ â ð¥ ⌠ð§))) |
80 | 79 | impd 410 |
. 2
⢠((ð¥ â V â§ ðŠ â V â§ ð§ â V) â ((ð¥ ⌠ðŠ â§ ðŠ âŒ ð§) â ð¥ ⌠ð§)) |
81 | 1, 2, 3, 80 | mp3an 1458 |
1
⢠((ð¥ ⌠ðŠ â§ ðŠ âŒ ð§) â ð¥ ⌠ð§) |