Step | Hyp | Ref
| Expression |
1 | | vex 3441 |
. 2
⢠ð¥ â V |
2 | | vex 3441 |
. 2
⢠ðŠ â V |
3 | | vex 3441 |
. 2
⢠ð§ â V |
4 | | erclwwlkn.w |
. . . . . 6
⢠ð = (ð ClWWalksN ðº) |
5 | | erclwwlkn.r |
. . . . . 6
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð ⧠ð¢ â ð ⧠âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
6 | 4, 5 | erclwwlkneqlen 28477 |
. . . . 5
⢠((ð¥ â V ⧠ðŠ â V) â (ð¥ ⌠ðŠ â (â¯âð¥) = (â¯âðŠ))) |
7 | 6 | 3adant3 1132 |
. . . 4
⢠((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â (ð¥ ⌠ðŠ â (â¯âð¥) = (â¯âðŠ))) |
8 | 4, 5 | erclwwlkneqlen 28477 |
. . . . . . 7
⢠((ðŠ â V ⧠ð§ â V) â (ðŠ ⌠ð§ â (â¯âðŠ) = (â¯âð§))) |
9 | 8 | 3adant1 1130 |
. . . . . 6
⢠((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â (ðŠ ⌠ð§ â (â¯âðŠ) = (â¯âð§))) |
10 | 4, 5 | erclwwlkneq 28476 |
. . . . . . . 8
⢠((ðŠ â V ⧠ð§ â V) â (ðŠ ⌠ð§ â (ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð)))) |
11 | 10 | 3adant1 1130 |
. . . . . . 7
⢠((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â (ðŠ ⌠ð§ â (ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð)))) |
12 | 4, 5 | erclwwlkneq 28476 |
. . . . . . . . . 10
⢠((ð¥ â V ⧠ðŠ â V) â (ð¥ ⌠ðŠ â (ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)))) |
13 | 12 | 3adant3 1132 |
. . . . . . . . 9
⢠((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â (ð¥ ⌠ðŠ â (ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)))) |
14 | | simpr1 1194 |
. . . . . . . . . . . . . . 15
â¢
(((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) ⧠(ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â ð¥ â ð) |
15 | | simplr2 1216 |
. . . . . . . . . . . . . . 15
â¢
(((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) ⧠(ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â ð§ â ð) |
16 | | oveq2 7315 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⢠(ð = ð â (ðŠ cyclShift ð) = (ðŠ cyclShift ð)) |
17 | 16 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⢠(ð = ð â (ð¥ = (ðŠ cyclShift ð) â ð¥ = (ðŠ cyclShift ð))) |
18 | 17 | cbvrexvw 3223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
â¢
(âð â
(0...ð)ð¥ = (ðŠ cyclShift ð) â âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) |
19 | | oveq2 7315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⢠(ð = ð â (ð§ cyclShift ð) = (ð§ cyclShift ð)) |
20 | 19 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⢠(ð = ð â (ðŠ = (ð§ cyclShift ð) â ðŠ = (ð§ cyclShift ð))) |
21 | 20 | cbvrexvw 3223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
â¢
(âð â
(0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ðŠ = (ð§ cyclShift ð)) |
22 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
â¢
(Vtxâðº) =
(Vtxâðº) |
23 | 22 | clwwlknbp 28444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠(ð§ â (ð ClWWalksN ðº) â (ð§ â Word (Vtxâðº) ⧠(â¯âð§) = ð)) |
24 | | eqcom 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
â¢
((â¯âð§) =
ð â ð = (â¯âð§)) |
25 | 24 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
â¢
((â¯âð§) =
ð â ð = (â¯âð§)) |
26 | 23, 25 | simpl2im 505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠(ð§ â (ð ClWWalksN ðº) â ð = (â¯âð§)) |
27 | 26, 4 | eleq2s 2855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠(ð§ â ð â ð = (â¯âð§)) |
28 | 27 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⢠((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) â ð = (â¯âð§)) |
29 | 23 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⢠(ð§ â (ð ClWWalksN ðº) â ð§ â Word (Vtxâðº)) |
30 | 29, 4 | eleq2s 2855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⢠(ð§ â ð â ð§ â Word (Vtxâðº)) |
31 | 30 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) â ð§ â Word (Vtxâðº)) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â ð§ â Word (Vtxâðº)) |
33 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â ((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) |
34 | 32, 33 | cshwcsh2id 14586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â (((ð â (0...(â¯âðŠ)) ⧠ð¥ = (ðŠ cyclShift ð)) ⧠(ð â (0...(â¯âð§)) ⧠ðŠ = (ð§ cyclShift ð))) â âð â (0...(â¯âð§))ð¥ = (ð§ cyclShift ð))) |
35 | | oveq2 7315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⢠(ð = (â¯âð§) â (0...ð) = (0...(â¯âð§))) |
36 | | oveq2 7315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
â¢
((â¯âð§) =
(â¯âðŠ) â
(0...(â¯âð§)) =
(0...(â¯âðŠ))) |
37 | 36 | eqcoms 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
â¢
((â¯âðŠ) =
(â¯âð§) â
(0...(â¯âð§)) =
(0...(â¯âðŠ))) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
â¢
(((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â
(0...(â¯âð§)) =
(0...(â¯âðŠ))) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⢠((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) â (0...(â¯âð§)) = (0...(â¯âðŠ))) |
40 | 35, 39 | sylan9eq 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â (0...ð) = (0...(â¯âðŠ))) |
41 | 40 | eleq2d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â (ð â (0...ð) â ð â (0...(â¯âðŠ)))) |
42 | 41 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â ((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) â (ð â (0...(â¯âðŠ)) ⧠ð¥ = (ðŠ cyclShift ð)))) |
43 | 35 | eleq2d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⢠(ð = (â¯âð§) â (ð â (0...ð) â ð â (0...(â¯âð§)))) |
44 | 43 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⢠(ð = (â¯âð§) â ((ð â (0...ð) ⧠ðŠ = (ð§ cyclShift ð)) â (ð â (0...(â¯âð§)) ⧠ðŠ = (ð§ cyclShift ð)))) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â ((ð â (0...ð) ⧠ðŠ = (ð§ cyclShift ð)) â (ð â (0...(â¯âð§)) ⧠ðŠ = (ð§ cyclShift ð)))) |
46 | 42, 45 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â (((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) ⧠(ð â (0...ð) ⧠ðŠ = (ð§ cyclShift ð))) â ((ð â (0...(â¯âðŠ)) ⧠ð¥ = (ðŠ cyclShift ð)) ⧠(ð â (0...(â¯âð§)) ⧠ðŠ = (ð§ cyclShift ð))))) |
47 | 35 | rexeqdv 3361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⢠(ð = (â¯âð§) â (âð â (0...ð)ð¥ = (ð§ cyclShift ð) â âð â (0...(â¯âð§))ð¥ = (ð§ cyclShift ð))) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â (âð â (0...ð)ð¥ = (ð§ cyclShift ð) â âð â (0...(â¯âð§))ð¥ = (ð§ cyclShift ð))) |
49 | 34, 46, 48 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⢠((ð = (â¯âð§) ⧠(((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)))) â (((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) ⧠(ð â (0...ð) ⧠ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
50 | 28, 49 | mpancom 686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⢠((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) â (((ð â (0...ð) ⧠ð¥ = (ðŠ cyclShift ð)) ⧠(ð â (0...ð) ⧠ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
51 | 50 | exp5l 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⢠((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) â (ð â (0...ð) â (ð¥ = (ðŠ cyclShift ð) â (ð â (0...ð) â (ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))))) |
52 | 51 | imp41 427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
â¢
(((((((ð¥ â
ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) ⧠ð â (0...ð)) ⧠ð¥ = (ðŠ cyclShift ð)) ⧠ð â (0...ð)) â (ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
53 | 52 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
â¢
((((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) ⧠ð â (0...ð)) ⧠ð¥ = (ðŠ cyclShift ð)) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
54 | 53 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
â¢
(((((ð¥ â ð ⧠ðŠ â ð) ⧠ð§ â ð) ⧠((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ))) ⧠ð â (0...ð)) â (ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
55 | 54 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 421 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠((ð¥ â ð ⧠ðŠ â ð) â (ð§ â ð â (((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â (âð â (0...ð)ðŠ = (ð§ cyclShift ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))))) |
59 | 58 | com15 101 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
(âð â
(0...ð)ðŠ = (ð§ cyclShift ð) â (ð§ â ð â (((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð ⧠ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))))) |
60 | 59 | impcom 409 |
. . . . . . . . . . . . . . . . . . . 20
⢠((ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â (((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð ⧠ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))))) |
61 | 60 | 3adant1 1130 |
. . . . . . . . . . . . . . . . . . 19
⢠((ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â (((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð ⧠ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))))) |
62 | 61 | impcom 409 |
. . . . . . . . . . . . . . . . . 18
â¢
((((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â§
(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((ð¥ â ð ⧠ðŠ â ð) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
63 | 62 | com13 88 |
. . . . . . . . . . . . . . . . 17
⢠((ð¥ â ð ⧠ðŠ â ð) â (âð â (0...ð)ð¥ = (ðŠ cyclShift ð) â ((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
64 | 63 | 3impia 1117 |
. . . . . . . . . . . . . . . 16
⢠((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
65 | 64 | impcom 409 |
. . . . . . . . . . . . . . 15
â¢
(((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) ⧠(ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â âð â (0...ð)ð¥ = (ð§ cyclShift ð)) |
66 | 14, 15, 65 | 3jca 1128 |
. . . . . . . . . . . . . 14
â¢
(((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) ⧠(ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â (ð¥ â ð ⧠ð§ â ð ⧠âð â (0...ð)ð¥ = (ð§ cyclShift ð))) |
67 | 4, 5 | erclwwlkneq 28476 |
. . . . . . . . . . . . . . 15
⢠((ð¥ â V ⧠ð§ â V) â (ð¥ ⌠ð§ â (ð¥ â ð ⧠ð§ â ð ⧠âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
68 | 67 | 3adant2 1131 |
. . . . . . . . . . . . . 14
⢠((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â (ð¥ ⌠ð§ â (ð¥ â ð ⧠ð§ â ð ⧠âð â (0...ð)ð¥ = (ð§ cyclShift ð)))) |
69 | 66, 68 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
â¢
(((((â¯âðŠ) = (â¯âð§) ⧠(â¯âð¥) = (â¯âðŠ)) ⧠(ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð))) ⧠(ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð))) â ((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â ð¥ ⌠ð§)) |
70 | 69 | exp31 421 |
. . . . . . . . . . . 12
â¢
(((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â
((ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â ð¥ ⌠ð§)))) |
71 | 70 | com24 95 |
. . . . . . . . . . 11
â¢
(((â¯âðŠ)
= (â¯âð§) â§
(â¯âð¥) =
(â¯âðŠ)) â
((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â ((ð¥ â ð ⧠ðŠ â ð ⧠âð â (0...ð)ð¥ = (ðŠ cyclShift ð)) â ((ðŠ â ð ⧠ð§ â ð ⧠âð â (0...ð)ðŠ = (ð§ cyclShift ð)) â ð¥ ⌠ð§)))) |
72 | 71 | ex 414 |
. . . . . . . . . 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 412 |
. 2
⢠((ð¥ â V ⧠ðŠ â V ⧠ð§ â V) â ((ð¥ ⌠ðŠ ⧠ðŠ ⌠ð§) â ð¥ ⌠ð§)) |
81 | 1, 2, 3, 80 | mp3an 1461 |
1
⢠((ð¥ ⌠ðŠ ⧠ðŠ ⌠ð§) â ð¥ ⌠ð§) |