Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
⢠((ðº â USPGraph ⧠ð â ð) â ð â ð) |
2 | | 0nn0 12436 |
. . 3
⢠0 â
â0 |
3 | | rusgrnumwwlk.v |
. . . 4
⢠ð = (Vtxâðº) |
4 | | rusgrnumwwlk.l |
. . . 4
⢠ð¿ = (ð£ â ð, ð â â0 âŠ
(â¯â{ð€ â
(ð WWalksN ðº) ⣠(ð€â0) = ð£})) |
5 | 3, 4 | rusgrnumwwlklem 28964 |
. . 3
⢠((ð â ð ⧠0 â â0) â
(ðð¿0) = (â¯â{ð€ â (0 WWalksN ðº) ⣠(ð€â0) = ð})) |
6 | 1, 2, 5 | sylancl 587 |
. 2
⢠((ðº â USPGraph ⧠ð â ð) â (ðð¿0) = (â¯â{ð€ â (0 WWalksN ðº) ⣠(ð€â0) = ð})) |
7 | | df-rab 3407 |
. . . . 5
⢠{ð€ â (0 WWalksN ðº) ⣠(ð€â0) = ð} = {ð€ ⣠(ð€ â (0 WWalksN ðº) ⧠(ð€â0) = ð)} |
8 | 7 | a1i 11 |
. . . 4
⢠((ðº â USPGraph ⧠ð â ð) â {ð€ â (0 WWalksN ðº) ⣠(ð€â0) = ð} = {ð€ ⣠(ð€ â (0 WWalksN ðº) ⧠(ð€â0) = ð)}) |
9 | | wwlksn0s 28855 |
. . . . . . . . 9
⢠(0
WWalksN ðº) = {ð€ â Word (Vtxâðº) ⣠(â¯âð€) = 1} |
10 | 9 | a1i 11 |
. . . . . . . 8
⢠((ðº â USPGraph ⧠ð â ð) â (0 WWalksN ðº) = {ð€ â Word (Vtxâðº) ⣠(â¯âð€) = 1}) |
11 | 10 | eleq2d 2820 |
. . . . . . 7
⢠((ðº â USPGraph ⧠ð â ð) â (ð€ â (0 WWalksN ðº) â ð€ â {ð€ â Word (Vtxâðº) ⣠(â¯âð€) = 1})) |
12 | | rabid 3426 |
. . . . . . 7
⢠(ð€ â {ð€ â Word (Vtxâðº) ⣠(â¯âð€) = 1} â (ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1)) |
13 | 11, 12 | bitrdi 287 |
. . . . . 6
⢠((ðº â USPGraph ⧠ð â ð) â (ð€ â (0 WWalksN ðº) â (ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1))) |
14 | 13 | anbi1d 631 |
. . . . 5
⢠((ðº â USPGraph ⧠ð â ð) â ((ð€ â (0 WWalksN ðº) ⧠(ð€â0) = ð) â ((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð))) |
15 | 14 | abbidv 2802 |
. . . 4
⢠((ðº â USPGraph ⧠ð â ð) â {ð€ ⣠(ð€ â (0 WWalksN ðº) ⧠(ð€â0) = ð)} = {ð€ ⣠((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð)}) |
16 | | wrdl1s1 14511 |
. . . . . . . . 9
⢠(ð â (Vtxâðº) â (ð£ = âšâðââ© â (ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1 ⧠(ð£â0) = ð))) |
17 | | df-3an 1090 |
. . . . . . . . 9
⢠((ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1 ⧠(ð£â0) = ð) â ((ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1) ⧠(ð£â0) = ð)) |
18 | 16, 17 | bitr2di 288 |
. . . . . . . 8
⢠(ð â (Vtxâðº) â (((ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1) ⧠(ð£â0) = ð) â ð£ = âšâðââ©)) |
19 | | vex 3451 |
. . . . . . . . 9
⢠ð£ â V |
20 | | eleq1w 2817 |
. . . . . . . . . . 11
⢠(ð€ = ð£ â (ð€ â Word (Vtxâðº) â ð£ â Word (Vtxâðº))) |
21 | | fveqeq2 6855 |
. . . . . . . . . . 11
⢠(ð€ = ð£ â ((â¯âð€) = 1 â (â¯âð£) = 1)) |
22 | 20, 21 | anbi12d 632 |
. . . . . . . . . 10
⢠(ð€ = ð£ â ((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) â (ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1))) |
23 | | fveq1 6845 |
. . . . . . . . . . 11
⢠(ð€ = ð£ â (ð€â0) = (ð£â0)) |
24 | 23 | eqeq1d 2735 |
. . . . . . . . . 10
⢠(ð€ = ð£ â ((ð€â0) = ð â (ð£â0) = ð)) |
25 | 22, 24 | anbi12d 632 |
. . . . . . . . 9
⢠(ð€ = ð£ â (((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð) â ((ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1) ⧠(ð£â0) = ð))) |
26 | 19, 25 | elab 3634 |
. . . . . . . 8
⢠(ð£ â {ð€ ⣠((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð)} â ((ð£ â Word (Vtxâðº) ⧠(â¯âð£) = 1) ⧠(ð£â0) = ð)) |
27 | | velsn 4606 |
. . . . . . . 8
⢠(ð£ â {âšâðââ©} â ð£ = âšâðââ©) |
28 | 18, 26, 27 | 3bitr4g 314 |
. . . . . . 7
⢠(ð â (Vtxâðº) â (ð£ â {ð€ ⣠((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð)} â ð£ â {âšâðââ©})) |
29 | 28, 3 | eleq2s 2852 |
. . . . . 6
⢠(ð â ð â (ð£ â {ð€ ⣠((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð)} â ð£ â {âšâðââ©})) |
30 | 29 | eqrdv 2731 |
. . . . 5
⢠(ð â ð â {ð€ ⣠((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð)} = {âšâðââ©}) |
31 | 30 | adantl 483 |
. . . 4
⢠((ðº â USPGraph ⧠ð â ð) â {ð€ ⣠((ð€ â Word (Vtxâðº) ⧠(â¯âð€) = 1) ⧠(ð€â0) = ð)} = {âšâðââ©}) |
32 | 8, 15, 31 | 3eqtrd 2777 |
. . 3
⢠((ðº â USPGraph ⧠ð â ð) â {ð€ â (0 WWalksN ðº) ⣠(ð€â0) = ð} = {âšâðââ©}) |
33 | 32 | fveq2d 6850 |
. 2
⢠((ðº â USPGraph ⧠ð â ð) â (â¯â{ð€ â (0 WWalksN ðº) ⣠(ð€â0) = ð}) = (â¯â{âšâðââ©})) |
34 | | s1cl 14499 |
. . . 4
⢠(ð â ð â âšâðââ© â Word ð) |
35 | | hashsng 14278 |
. . . 4
â¢
(âšâðââ© â Word ð â (â¯â{âšâðââ©}) =
1) |
36 | 34, 35 | syl 17 |
. . 3
⢠(ð â ð â (â¯â{âšâðââ©}) =
1) |
37 | 36 | adantl 483 |
. 2
⢠((ðº â USPGraph ⧠ð â ð) â (â¯â{âšâðââ©}) =
1) |
38 | 6, 33, 37 | 3eqtrd 2777 |
1
⢠((ðº â USPGraph ⧠ð â ð) â (ðð¿0) = 1) |