Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . . 6
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2 β§
(πβ0) β (πβ(β―βπΉ))) β πΊ β USGraph) |
2 | 1 | anim2i 618 |
. . . . 5
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (πΉ(WalksβπΊ)π β§ πΊ β USGraph)) |
3 | 2 | ancomd 463 |
. . . 4
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (πΊ β USGraph β§ πΉ(WalksβπΊ)π)) |
4 | | 3simpc 1151 |
. . . . 5
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2 β§
(πβ0) β (πβ(β―βπΉ))) β ((β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) |
5 | 4 | adantl 483 |
. . . 4
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β ((β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) |
6 | | usgr2wlkneq 28746 |
. . . 4
β’ (((πΊ β USGraph β§ πΉ(WalksβπΊ)π) β§ ((β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2)) β§ (πΉβ0) β (πΉβ1))) |
7 | 3, 5, 6 | syl2anc 585 |
. . 3
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2)) β§ (πΉβ0) β (πΉβ1))) |
8 | | simpl 484 |
. . . 4
β’ ((((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2)) β§ (πΉβ0) β (πΉβ1)) β ((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2))) |
9 | | fvex 6856 |
. . . . 5
β’ (πβ0) β
V |
10 | | fvex 6856 |
. . . . 5
β’ (πβ1) β
V |
11 | | fvex 6856 |
. . . . 5
β’ (πβ2) β
V |
12 | 9, 10, 11 | 3pm3.2i 1340 |
. . . 4
β’ ((πβ0) β V β§ (πβ1) β V β§ (πβ2) β
V) |
13 | 8, 12 | jctil 521 |
. . 3
β’ ((((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2)) β§ (πΉβ0) β (πΉβ1)) β (((πβ0) β V β§ (πβ1) β V β§ (πβ2) β V) β§
((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2)))) |
14 | | funcnvs3 14809 |
. . 3
β’ ((((πβ0) β V β§ (πβ1) β V β§ (πβ2) β V) β§
((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2))) β Fun β‘β¨β(πβ0)(πβ1)(πβ2)ββ©) |
15 | 7, 13, 14 | 3syl 18 |
. 2
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β Fun β‘β¨β(πβ0)(πβ1)(πβ2)ββ©) |
16 | | eqid 2733 |
. . . . . 6
β’
(VtxβπΊ) =
(VtxβπΊ) |
17 | 16 | wlkpwrd 28607 |
. . . . 5
β’ (πΉ(WalksβπΊ)π β π β Word (VtxβπΊ)) |
18 | | wlklenvp1 28608 |
. . . . . 6
β’ (πΉ(WalksβπΊ)π β (β―βπ) = ((β―βπΉ) + 1)) |
19 | | oveq1 7365 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β ((β―βπΉ)
+ 1) = (2 + 1)) |
20 | | 2p1e3 12300 |
. . . . . . . 8
β’ (2 + 1) =
3 |
21 | 19, 20 | eqtrdi 2789 |
. . . . . . 7
β’
((β―βπΉ) =
2 β ((β―βπΉ)
+ 1) = 3) |
22 | 21 | 3ad2ant2 1135 |
. . . . . 6
β’ ((πΊ β USGraph β§
(β―βπΉ) = 2 β§
(πβ0) β (πβ(β―βπΉ))) β ((β―βπΉ) + 1) = 3) |
23 | 18, 22 | sylan9eq 2793 |
. . . . 5
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (β―βπ) = 3) |
24 | | wrdlen3s3 14844 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = 3) β π = β¨β(πβ0)(πβ1)(πβ2)ββ©) |
25 | 17, 23, 24 | syl2an2r 684 |
. . . 4
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β π = β¨β(πβ0)(πβ1)(πβ2)ββ©) |
26 | 25 | cnveqd 5832 |
. . 3
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β β‘π = β‘β¨β(πβ0)(πβ1)(πβ2)ββ©) |
27 | 26 | funeqd 6524 |
. 2
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (Fun β‘π β Fun β‘β¨β(πβ0)(πβ1)(πβ2)ββ©)) |
28 | 15, 27 | mpbird 257 |
1
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β Fun β‘π) |