Step | Hyp | Ref
| Expression |
1 | | wwlks2onv.v |
. . 3
⢠ð = (Vtxâðº) |
2 | 1 | wwlksonvtx 28842 |
. 2
⢠(ð â (ðŽ(2 WWalksNOn ðº)ð¶) â (ðŽ â ð ⧠ð¶ â ð)) |
3 | | wwlknon 28844 |
. . 3
⢠(ð â (ðŽ(2 WWalksNOn ðº)ð¶) â (ð â (2 WWalksN ðº) ⧠(ðâ0) = ðŽ ⧠(ðâ2) = ð¶)) |
4 | | wwlknbp1 28831 |
. . . . 5
⢠(ð â (2 WWalksN ðº) â (2 â
â0 ⧠ð
â Word (Vtxâðº)
⧠(â¯âð) =
(2 + 1))) |
5 | | 2p1e3 12300 |
. . . . . . . 8
⢠(2 + 1) =
3 |
6 | 5 | eqeq2i 2746 |
. . . . . . 7
â¢
((â¯âð) =
(2 + 1) â (â¯âð) = 3) |
7 | | 1ex 11156 |
. . . . . . . . . . . . . 14
⢠1 â
V |
8 | 7 | tpid2 4732 |
. . . . . . . . . . . . 13
⢠1 â
{0, 1, 2} |
9 | | fzo0to3tp 13664 |
. . . . . . . . . . . . 13
⢠(0..^3) =
{0, 1, 2} |
10 | 8, 9 | eleqtrri 2833 |
. . . . . . . . . . . 12
⢠1 â
(0..^3) |
11 | | oveq2 7366 |
. . . . . . . . . . . 12
â¢
((â¯âð) =
3 â (0..^(â¯âð)) = (0..^3)) |
12 | 10, 11 | eleqtrrid 2841 |
. . . . . . . . . . 11
â¢
((â¯âð) =
3 â 1 â (0..^(â¯âð))) |
13 | | wrdsymbcl 14421 |
. . . . . . . . . . 11
⢠((ð â Word (Vtxâðº) ⧠1 â
(0..^(â¯âð)))
â (ðâ1) â
(Vtxâðº)) |
14 | 12, 13 | sylan2 594 |
. . . . . . . . . 10
⢠((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) â (ðâ1) â (Vtxâðº)) |
15 | 14 | 3ad2ant1 1134 |
. . . . . . . . 9
⢠(((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) â (ðâ1) â (Vtxâðº)) |
16 | | simpl1r 1226 |
. . . . . . . . . . 11
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â (â¯âð) = 3) |
17 | | simpl 484 |
. . . . . . . . . . . . . 14
⢠(((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â (ðâ0) = ðŽ) |
18 | | eqidd 2734 |
. . . . . . . . . . . . . 14
⢠(((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â (ðâ1) = (ðâ1)) |
19 | | simpr 486 |
. . . . . . . . . . . . . 14
⢠(((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â (ðâ2) = ð¶) |
20 | 17, 18, 19 | 3jca 1129 |
. . . . . . . . . . . . 13
⢠(((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â ((ðâ0) = ðŽ ⧠(ðâ1) = (ðâ1) ⧠(ðâ2) = ð¶)) |
21 | 20 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⢠(((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) â ((ðâ0) = ðŽ ⧠(ðâ1) = (ðâ1) ⧠(ðâ2) = ð¶)) |
22 | 21 | adantr 482 |
. . . . . . . . . . 11
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â ((ðâ0) = ðŽ ⧠(ðâ1) = (ðâ1) ⧠(ðâ2) = ð¶)) |
23 | 1 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . 18
â¢
(Vtxâðº) =
ð |
24 | 23 | wrdeqi 14431 |
. . . . . . . . . . . . . . . . 17
⢠Word
(Vtxâðº) = Word ð |
25 | 24 | eleq2i 2826 |
. . . . . . . . . . . . . . . 16
⢠(ð â Word (Vtxâðº) â ð â Word ð) |
26 | 25 | biimpi 215 |
. . . . . . . . . . . . . . 15
⢠(ð â Word (Vtxâðº) â ð â Word ð) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . 14
⢠((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) â ð â Word ð) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⢠(((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) â ð â Word ð) |
29 | 28 | adantr 482 |
. . . . . . . . . . . 12
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â ð â Word ð) |
30 | | simpl3l 1229 |
. . . . . . . . . . . 12
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â ðŽ â ð) |
31 | 23 | eleq2i 2826 |
. . . . . . . . . . . . . 14
⢠((ðâ1) â
(Vtxâðº) â (ðâ1) â ð) |
32 | 31 | biimpi 215 |
. . . . . . . . . . . . 13
⢠((ðâ1) â
(Vtxâðº) â (ðâ1) â ð) |
33 | 32 | adantl 483 |
. . . . . . . . . . . 12
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â (ðâ1) â ð) |
34 | | simpl3r 1230 |
. . . . . . . . . . . 12
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â ð¶ â ð) |
35 | | eqwrds3 14856 |
. . . . . . . . . . . 12
⢠((ð â Word ð ⧠(ðŽ â ð ⧠(ðâ1) â ð ⧠ð¶ â ð)) â (ð = âšâðŽ(ðâ1)ð¶ââ© â ((â¯âð) = 3 ⧠((ðâ0) = ðŽ ⧠(ðâ1) = (ðâ1) ⧠(ðâ2) = ð¶)))) |
36 | 29, 30, 33, 34, 35 | syl13anc 1373 |
. . . . . . . . . . 11
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â (ð = âšâðŽ(ðâ1)ð¶ââ© â ((â¯âð) = 3 ⧠((ðâ0) = ðŽ ⧠(ðâ1) = (ðâ1) ⧠(ðâ2) = ð¶)))) |
37 | 16, 22, 36 | mpbir2and 712 |
. . . . . . . . . 10
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â ð = âšâðŽ(ðâ1)ð¶ââ©) |
38 | 37, 33 | jca 513 |
. . . . . . . . 9
⢠((((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) ⧠(ðâ1) â (Vtxâðº)) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)) |
39 | 15, 38 | mpdan 686 |
. . . . . . . 8
⢠(((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) ⧠((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) ⧠(ðŽ â ð ⧠ð¶ â ð)) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)) |
40 | 39 | 3exp 1120 |
. . . . . . 7
⢠((ð â Word (Vtxâðº) ⧠(â¯âð) = 3) â (((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â ((ðŽ â ð ⧠ð¶ â ð) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)))) |
41 | 6, 40 | sylan2b 595 |
. . . . . 6
⢠((ð â Word (Vtxâðº) ⧠(â¯âð) = (2 + 1)) â (((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â ((ðŽ â ð ⧠ð¶ â ð) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)))) |
42 | 41 | 3adant1 1131 |
. . . . 5
⢠((2
â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (2 + 1)) â (((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â ((ðŽ â ð ⧠ð¶ â ð) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)))) |
43 | 4, 42 | syl 17 |
. . . 4
⢠(ð â (2 WWalksN ðº) â (((ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â ((ðŽ â ð ⧠ð¶ â ð) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)))) |
44 | 43 | 3impib 1117 |
. . 3
⢠((ð â (2 WWalksN ðº) ⧠(ðâ0) = ðŽ ⧠(ðâ2) = ð¶) â ((ðŽ â ð ⧠ð¶ â ð) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð))) |
45 | 3, 44 | sylbi 216 |
. 2
⢠(ð â (ðŽ(2 WWalksNOn ðº)ð¶) â ((ðŽ â ð ⧠ð¶ â ð) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð))) |
46 | 2, 45 | mpd 15 |
1
⢠(ð â (ðŽ(2 WWalksNOn ðº)ð¶) â (ð = âšâðŽ(ðâ1)ð¶â⩠⧠(ðâ1) â ð)) |