Step | Hyp | Ref
| Expression |
1 | | eqeq1 2737 |
. . . 4
⢠(ðŠ = ð¥ â (ðŠ = (ð cyclShift ð) â ð¥ = (ð cyclShift ð))) |
2 | 1 | rexbidv 3172 |
. . 3
⢠(ðŠ = ð¥ â (âð â (0...ð)ðŠ = (ð cyclShift ð) â âð â (0...ð)ð¥ = (ð cyclShift ð))) |
3 | 2 | cbvrabv 3416 |
. 2
⢠{ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð cyclShift ð)} = {ð¥ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ð¥ = (ð cyclShift ð)} |
4 | | eqid 2733 |
. . . . . . . 8
â¢
(Vtxâðº) =
(Vtxâðº) |
5 | 4 | clwwlknwrd 29027 |
. . . . . . 7
⢠(ð€ â (ð ClWWalksN ðº) â ð€ â Word (Vtxâðº)) |
6 | 5 | ad2antrl 727 |
. . . . . 6
⢠(((ð â â0
⧠ð â (ð ClWWalksN ðº)) ⧠(ð€ â (ð ClWWalksN ðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) â ð€ â Word (Vtxâðº)) |
7 | | simprr 772 |
. . . . . 6
⢠(((ð â â0
⧠ð â (ð ClWWalksN ðº)) ⧠(ð€ â (ð ClWWalksN ðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) â âð â (0...ð)ð€ = (ð cyclShift ð)) |
8 | 6, 7 | jca 513 |
. . . . 5
⢠(((ð â â0
⧠ð â (ð ClWWalksN ðº)) ⧠(ð€ â (ð ClWWalksN ðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) â (ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) |
9 | | simprr 772 |
. . . . . . . . . . . . 13
⢠(((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) ⧠(ð â â0 ⧠ð â (ð ClWWalksN ðº))) â ð â (ð ClWWalksN ðº)) |
10 | | simpllr 775 |
. . . . . . . . . . . . 13
⢠((((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) ⧠(ð â â0 ⧠ð â (ð ClWWalksN ðº))) ⧠ð€ = (ð cyclShift ð)) â ð â (0...ð)) |
11 | | clwwnisshclwwsn 29052 |
. . . . . . . . . . . . 13
⢠((ð â (ð ClWWalksN ðº) ⧠ð â (0...ð)) â (ð cyclShift ð) â (ð ClWWalksN ðº)) |
12 | 9, 10, 11 | syl2an2r 684 |
. . . . . . . . . . . 12
⢠((((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) ⧠(ð â â0 ⧠ð â (ð ClWWalksN ðº))) ⧠ð€ = (ð cyclShift ð)) â (ð cyclShift ð) â (ð ClWWalksN ðº)) |
13 | | eleq1 2822 |
. . . . . . . . . . . . 13
⢠(ð€ = (ð cyclShift ð) â (ð€ â (ð ClWWalksN ðº) â (ð cyclShift ð) â (ð ClWWalksN ðº))) |
14 | 13 | adantl 483 |
. . . . . . . . . . . 12
⢠((((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) ⧠(ð â â0 ⧠ð â (ð ClWWalksN ðº))) ⧠ð€ = (ð cyclShift ð)) â (ð€ â (ð ClWWalksN ðº) â (ð cyclShift ð) â (ð ClWWalksN ðº))) |
15 | 12, 14 | mpbird 257 |
. . . . . . . . . . 11
⢠((((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) ⧠(ð â â0 ⧠ð â (ð ClWWalksN ðº))) ⧠ð€ = (ð cyclShift ð)) â ð€ â (ð ClWWalksN ðº)) |
16 | 15 | exp31 421 |
. . . . . . . . . 10
⢠((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) â ((ð â â0 ⧠ð â (ð ClWWalksN ðº)) â (ð€ = (ð cyclShift ð) â ð€ â (ð ClWWalksN ðº)))) |
17 | 16 | com23 86 |
. . . . . . . . 9
⢠((ð€ â Word (Vtxâðº) ⧠ð â (0...ð)) â (ð€ = (ð cyclShift ð) â ((ð â â0 ⧠ð â (ð ClWWalksN ðº)) â ð€ â (ð ClWWalksN ðº)))) |
18 | 17 | rexlimdva 3149 |
. . . . . . . 8
⢠(ð€ â Word (Vtxâðº) â (âð â (0...ð)ð€ = (ð cyclShift ð) â ((ð â â0 ⧠ð â (ð ClWWalksN ðº)) â ð€ â (ð ClWWalksN ðº)))) |
19 | 18 | imp 408 |
. . . . . . 7
⢠((ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð)) â ((ð â â0 ⧠ð â (ð ClWWalksN ðº)) â ð€ â (ð ClWWalksN ðº))) |
20 | 19 | impcom 409 |
. . . . . 6
⢠(((ð â â0
⧠ð â (ð ClWWalksN ðº)) ⧠(ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) â ð€ â (ð ClWWalksN ðº)) |
21 | | simprr 772 |
. . . . . 6
⢠(((ð â â0
⧠ð â (ð ClWWalksN ðº)) ⧠(ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) â âð â (0...ð)ð€ = (ð cyclShift ð)) |
22 | 20, 21 | jca 513 |
. . . . 5
⢠(((ð â â0
⧠ð â (ð ClWWalksN ðº)) ⧠(ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) â (ð€ â (ð ClWWalksN ðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) |
23 | 8, 22 | impbida 800 |
. . . 4
⢠((ð â â0
⧠ð â (ð ClWWalksN ðº)) â ((ð€ â (ð ClWWalksN ðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð)) â (ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð)))) |
24 | | eqeq1 2737 |
. . . . . 6
⢠(ð¥ = ð€ â (ð¥ = (ð cyclShift ð) â ð€ = (ð cyclShift ð))) |
25 | 24 | rexbidv 3172 |
. . . . 5
⢠(ð¥ = ð€ â (âð â (0...ð)ð¥ = (ð cyclShift ð) â âð â (0...ð)ð€ = (ð cyclShift ð))) |
26 | 25 | elrab 3649 |
. . . 4
⢠(ð€ â {ð¥ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ð¥ = (ð cyclShift ð)} â (ð€ â (ð ClWWalksN ðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) |
27 | | eqeq1 2737 |
. . . . . 6
⢠(ðŠ = ð€ â (ðŠ = (ð cyclShift ð) â ð€ = (ð cyclShift ð))) |
28 | 27 | rexbidv 3172 |
. . . . 5
⢠(ðŠ = ð€ â (âð â (0...ð)ðŠ = (ð cyclShift ð) â âð â (0...ð)ð€ = (ð cyclShift ð))) |
29 | 28 | elrab 3649 |
. . . 4
⢠(ð€ â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð cyclShift ð)} â (ð€ â Word (Vtxâðº) ⧠âð â (0...ð)ð€ = (ð cyclShift ð))) |
30 | 23, 26, 29 | 3bitr4g 314 |
. . 3
⢠((ð â â0
⧠ð â (ð ClWWalksN ðº)) â (ð€ â {ð¥ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ð¥ = (ð cyclShift ð)} â ð€ â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð cyclShift ð)})) |
31 | 30 | eqrdv 2731 |
. 2
⢠((ð â â0
⧠ð â (ð ClWWalksN ðº)) â {ð¥ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ð¥ = (ð cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð cyclShift ð)}) |
32 | 3, 31 | eqtrid 2785 |
1
⢠((ð â â0
⧠ð â (ð ClWWalksN ðº)) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð cyclShift ð)}) |