Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = 0 â (ðð¿ð¥) = (ðð¿0)) |
2 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = 0 â (ðŸâð¥) = (ðŸâ0)) |
3 | 1, 2 | eqeq12d 2749 |
. . . . . . 7
⢠(ð¥ = 0 â ((ðð¿ð¥) = (ðŸâð¥) â (ðð¿0) = (ðŸâ0))) |
4 | 3 | imbi2d 341 |
. . . . . 6
⢠(ð¥ = 0 â ((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ð¥) = (ðŸâð¥)) â (((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿0) = (ðŸâ0)))) |
5 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = ðŠ â (ðð¿ð¥) = (ðð¿ðŠ)) |
6 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = ðŠ â (ðŸâð¥) = (ðŸâðŠ)) |
7 | 5, 6 | eqeq12d 2749 |
. . . . . . 7
⢠(ð¥ = ðŠ â ((ðð¿ð¥) = (ðŸâð¥) â (ðð¿ðŠ) = (ðŸâðŠ))) |
8 | 7 | imbi2d 341 |
. . . . . 6
⢠(ð¥ = ðŠ â ((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ð¥) = (ðŸâð¥)) â (((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ðŠ) = (ðŸâðŠ)))) |
9 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = (ðŠ + 1) â (ðð¿ð¥) = (ðð¿(ðŠ + 1))) |
10 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = (ðŠ + 1) â (ðŸâð¥) = (ðŸâ(ðŠ + 1))) |
11 | 9, 10 | eqeq12d 2749 |
. . . . . . 7
⢠(ð¥ = (ðŠ + 1) â ((ðð¿ð¥) = (ðŸâð¥) â (ðð¿(ðŠ + 1)) = (ðŸâ(ðŠ + 1)))) |
12 | 11 | imbi2d 341 |
. . . . . 6
⢠(ð¥ = (ðŠ + 1) â ((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ð¥) = (ðŸâð¥)) â (((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿(ðŠ + 1)) = (ðŸâ(ðŠ + 1))))) |
13 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = ð â (ðð¿ð¥) = (ðð¿ð)) |
14 | | oveq2 7369 |
. . . . . . . 8
⢠(ð¥ = ð â (ðŸâð¥) = (ðŸâð)) |
15 | 13, 14 | eqeq12d 2749 |
. . . . . . 7
⢠(ð¥ = ð â ((ðð¿ð¥) = (ðŸâð¥) â (ðð¿ð) = (ðŸâð))) |
16 | 15 | imbi2d 341 |
. . . . . 6
⢠(ð¥ = ð â ((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ð¥) = (ðŸâð¥)) â (((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ð) = (ðŸâð)))) |
17 | | rusgrusgr 28561 |
. . . . . . . . 9
⢠(ðº RegUSGraph ðŸ â ðº â USGraph) |
18 | | usgruspgr 28178 |
. . . . . . . . 9
⢠(ðº â USGraph â ðº â
USPGraph) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⢠(ðº RegUSGraph ðŸ â ðº â USPGraph) |
20 | | simpr 486 |
. . . . . . . 8
⢠((ð â Fin ⧠ð â ð) â ð â ð) |
21 | | rusgrnumwwlk.v |
. . . . . . . . 9
⢠ð = (Vtxâðº) |
22 | | rusgrnumwwlk.l |
. . . . . . . . 9
⢠ð¿ = (ð£ â ð, ð â â0 âŠ
(â¯â{ð€ â
(ð WWalksN ðº) ⣠(ð€â0) = ð£})) |
23 | 21, 22 | rusgrnumwwlkb0 28965 |
. . . . . . . 8
⢠((ðº â USPGraph ⧠ð â ð) â (ðð¿0) = 1) |
24 | 19, 20, 23 | syl2anr 598 |
. . . . . . 7
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿0) = 1) |
25 | | simpl 484 |
. . . . . . . . . . 11
⢠((ð â Fin ⧠ð â ð) â ð â Fin) |
26 | 25, 17 | anim12ci 615 |
. . . . . . . . . 10
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðº â USGraph ⧠ð â Fin)) |
27 | 21 | isfusgr 28315 |
. . . . . . . . . 10
⢠(ðº â FinUSGraph â (ðº â USGraph ⧠ð â Fin)) |
28 | 26, 27 | sylibr 233 |
. . . . . . . . 9
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â ðº â FinUSGraph) |
29 | | simpr 486 |
. . . . . . . . 9
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â ðº RegUSGraph ðŸ) |
30 | | ne0i 4298 |
. . . . . . . . . 10
⢠(ð â ð â ð â â
) |
31 | 30 | ad2antlr 726 |
. . . . . . . . 9
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â ð â â
) |
32 | 21 | frusgrnn0 28568 |
. . . . . . . . . 10
⢠((ðº â FinUSGraph ⧠ðº RegUSGraph ðŸ ⧠ð â â
) â ðŸ â
â0) |
33 | 32 | nn0cnd 12483 |
. . . . . . . . 9
⢠((ðº â FinUSGraph ⧠ðº RegUSGraph ðŸ ⧠ð â â
) â ðŸ â â) |
34 | 28, 29, 31, 33 | syl3anc 1372 |
. . . . . . . 8
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â ðŸ â â) |
35 | 34 | exp0d 14054 |
. . . . . . 7
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðŸâ0) = 1) |
36 | 24, 35 | eqtr4d 2776 |
. . . . . 6
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿0) = (ðŸâ0)) |
37 | | simpl 484 |
. . . . . . . . . . 11
⢠(((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ð â Fin ⧠ð â ð)) |
38 | 37 | anim1i 616 |
. . . . . . . . . 10
⢠((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) ⧠ðŠ â â0) â ((ð â Fin ⧠ð â ð) ⧠ðŠ â
â0)) |
39 | | df-3an 1090 |
. . . . . . . . . 10
⢠((ð â Fin ⧠ð â ð ⧠ðŠ â â0) â ((ð â Fin ⧠ð â ð) ⧠ðŠ â
â0)) |
40 | 38, 39 | sylibr 233 |
. . . . . . . . 9
⢠((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) ⧠ðŠ â â0) â (ð â Fin ⧠ð â ð ⧠ðŠ â
â0)) |
41 | 21, 22 | rusgrnumwwlks 28968 |
. . . . . . . . 9
⢠((ðº RegUSGraph ðŸ ⧠(ð â Fin ⧠ð â ð ⧠ðŠ â â0)) â ((ðð¿ðŠ) = (ðŸâðŠ) â (ðð¿(ðŠ + 1)) = (ðŸâ(ðŠ + 1)))) |
42 | 29, 40, 41 | syl2an2r 684 |
. . . . . . . 8
⢠((((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) ⧠ðŠ â â0) â ((ðð¿ðŠ) = (ðŸâðŠ) â (ðð¿(ðŠ + 1)) = (ðŸâ(ðŠ + 1)))) |
43 | 42 | expcom 415 |
. . . . . . 7
⢠(ðŠ â â0
â (((ð â Fin
⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â ((ðð¿ðŠ) = (ðŸâðŠ) â (ðð¿(ðŠ + 1)) = (ðŸâ(ðŠ + 1))))) |
44 | 43 | a2d 29 |
. . . . . 6
⢠(ðŠ â â0
â ((((ð â Fin
⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ðŠ) = (ðŸâðŠ)) â (((ð â Fin ⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿(ðŠ + 1)) = (ðŸâ(ðŠ + 1))))) |
45 | 4, 8, 12, 16, 36, 44 | nn0ind 12606 |
. . . . 5
⢠(ð â â0
â (((ð â Fin
⧠ð â ð) ⧠ðº RegUSGraph ðŸ) â (ðð¿ð) = (ðŸâð))) |
46 | 45 | expd 417 |
. . . 4
⢠(ð â â0
â ((ð â Fin â§
ð â ð) â (ðº RegUSGraph ðŸ â (ðð¿ð) = (ðŸâð)))) |
47 | 46 | com12 32 |
. . 3
⢠((ð â Fin ⧠ð â ð) â (ð â â0 â (ðº RegUSGraph ðŸ â (ðð¿ð) = (ðŸâð)))) |
48 | 47 | 3impia 1118 |
. 2
⢠((ð â Fin ⧠ð â ð ⧠ð â â0) â (ðº RegUSGraph ðŸ â (ðð¿ð) = (ðŸâð))) |
49 | 48 | impcom 409 |
1
⢠((ðº RegUSGraph ðŸ ⧠(ð â Fin ⧠ð â ð ⧠ð â â0)) â (ðð¿ð) = (ðŸâð)) |