Step | Hyp | Ref
| Expression |
1 | | cyclprop 29039 |
. . . . . . . . . . . . 13
β’ (π(CyclesβπΊ)π β (π(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπ)))) |
2 | | fveq2 6888 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
1 β (πβ(β―βπ)) = (πβ1)) |
3 | 2 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
β’
((β―βπ) =
1 β ((πβ0) =
(πβ(β―βπ)) β (πβ0) = (πβ1))) |
4 | 3 | anbi2d 629 |
. . . . . . . . . . . . . 14
β’
((β―βπ) =
1 β ((π(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπ))) β (π(PathsβπΊ)π β§ (πβ0) = (πβ1)))) |
5 | 4 | biimpd 228 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
1 β ((π(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπ))) β (π(PathsβπΊ)π β§ (πβ0) = (πβ1)))) |
6 | 1, 5 | mpan9 507 |
. . . . . . . . . . . 12
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (π(PathsβπΊ)π β§ (πβ0) = (πβ1))) |
7 | | pthiswlk 28973 |
. . . . . . . . . . . . 13
β’ (π(PathsβπΊ)π β π(WalksβπΊ)π) |
8 | 7 | anim1i 615 |
. . . . . . . . . . . 12
β’ ((π(PathsβπΊ)π β§ (πβ0) = (πβ1)) β (π(WalksβπΊ)π β§ (πβ0) = (πβ1))) |
9 | 6, 8 | syl 17 |
. . . . . . . . . . 11
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (π(WalksβπΊ)π β§ (πβ0) = (πβ1))) |
10 | 9 | anim1i 615 |
. . . . . . . . . 10
β’ (((π(CyclesβπΊ)π β§ (β―βπ) = 1) β§ (β―βπ) = 1) β ((π(WalksβπΊ)π β§ (πβ0) = (πβ1)) β§ (β―βπ) = 1)) |
11 | 10 | anabss3 673 |
. . . . . . . . 9
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β ((π(WalksβπΊ)π β§ (πβ0) = (πβ1)) β§ (β―βπ) = 1)) |
12 | | df-3an 1089 |
. . . . . . . . 9
β’ ((π(WalksβπΊ)π β§ (πβ0) = (πβ1) β§ (β―βπ) = 1) β ((π(WalksβπΊ)π β§ (πβ0) = (πβ1)) β§ (β―βπ) = 1)) |
13 | 11, 12 | sylibr 233 |
. . . . . . . 8
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (π(WalksβπΊ)π β§ (πβ0) = (πβ1) β§ (β―βπ) = 1)) |
14 | | 3ancomb 1099 |
. . . . . . . 8
β’ ((π(WalksβπΊ)π β§ (πβ0) = (πβ1) β§ (β―βπ) = 1) β (π(WalksβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = (πβ1))) |
15 | 13, 14 | sylib 217 |
. . . . . . 7
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (π(WalksβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = (πβ1))) |
16 | | wlkl1loop 28884 |
. . . . . . . . . 10
β’ (((Fun
(iEdgβπΊ) β§ π(WalksβπΊ)π) β§ ((β―βπ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} β (EdgβπΊ)) |
17 | 16 | expl 458 |
. . . . . . . . 9
β’ (Fun
(iEdgβπΊ) β
((π(WalksβπΊ)π β§ ((β―βπ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} β (EdgβπΊ))) |
18 | | eqid 2732 |
. . . . . . . . . 10
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
19 | 18 | uhgrfun 28315 |
. . . . . . . . 9
β’ (πΊ β UHGraph β Fun
(iEdgβπΊ)) |
20 | 17, 19 | syl11 33 |
. . . . . . . 8
β’ ((π(WalksβπΊ)π β§ ((β―βπ) = 1 β§ (πβ0) = (πβ1))) β (πΊ β UHGraph β {(πβ0)} β (EdgβπΊ))) |
21 | 20 | 3impb 1115 |
. . . . . . 7
β’ ((π(WalksβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = (πβ1)) β (πΊ β UHGraph β {(πβ0)} β (EdgβπΊ))) |
22 | 15, 21 | syl 17 |
. . . . . 6
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1) β (πΊ β UHGraph β {(πβ0)} β (EdgβπΊ))) |
23 | 22 | 3adant3 1132 |
. . . . 5
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β (πΊ β UHGraph β {(πβ0)} β (EdgβπΊ))) |
24 | | sneq 4637 |
. . . . . . 7
β’ ((πβ0) = π΄ β {(πβ0)} = {π΄}) |
25 | 24 | eleq1d 2818 |
. . . . . 6
β’ ((πβ0) = π΄ β ({(πβ0)} β (EdgβπΊ) β {π΄} β (EdgβπΊ))) |
26 | 25 | 3ad2ant3 1135 |
. . . . 5
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β ({(πβ0)} β (EdgβπΊ) β {π΄} β (EdgβπΊ))) |
27 | 23, 26 | sylibd 238 |
. . . 4
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β (πΊ β UHGraph β {π΄} β (EdgβπΊ))) |
28 | 27 | exlimivv 1935 |
. . 3
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β (πΊ β UHGraph β {π΄} β (EdgβπΊ))) |
29 | 28 | com12 32 |
. 2
β’ (πΊ β UHGraph β
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β {π΄} β (EdgβπΊ))) |
30 | | edgval 28298 |
. . . . . . . . . . . . . 14
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
31 | 30 | eleq2i 2825 |
. . . . . . . . . . . . 13
β’ ({π΄} β (EdgβπΊ) β {π΄} β ran (iEdgβπΊ)) |
32 | | elrnrexdm 7087 |
. . . . . . . . . . . . . 14
β’ (Fun
(iEdgβπΊ) β
({π΄} β ran
(iEdgβπΊ) β
βπ β dom
(iEdgβπΊ){π΄} = ((iEdgβπΊ)βπ))) |
33 | | eqcom 2739 |
. . . . . . . . . . . . . . 15
β’ ({π΄} = ((iEdgβπΊ)βπ) β ((iEdgβπΊ)βπ) = {π΄}) |
34 | 33 | rexbii 3094 |
. . . . . . . . . . . . . 14
β’
(βπ β dom
(iEdgβπΊ){π΄} = ((iEdgβπΊ)βπ) β βπ β dom (iEdgβπΊ)((iEdgβπΊ)βπ) = {π΄}) |
35 | 32, 34 | imbitrdi 250 |
. . . . . . . . . . . . 13
β’ (Fun
(iEdgβπΊ) β
({π΄} β ran
(iEdgβπΊ) β
βπ β dom
(iEdgβπΊ)((iEdgβπΊ)βπ) = {π΄})) |
36 | 31, 35 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (Fun
(iEdgβπΊ) β
({π΄} β
(EdgβπΊ) β
βπ β dom
(iEdgβπΊ)((iEdgβπΊ)βπ) = {π΄})) |
37 | 19, 36 | syl 17 |
. . . . . . . . . . 11
β’ (πΊ β UHGraph β ({π΄} β (EdgβπΊ) β βπ β dom (iEdgβπΊ)((iEdgβπΊ)βπ) = {π΄})) |
38 | | df-rex 3071 |
. . . . . . . . . . 11
β’
(βπ β dom
(iEdgβπΊ)((iEdgβπΊ)βπ) = {π΄} β βπ(π β dom (iEdgβπΊ) β§ ((iEdgβπΊ)βπ) = {π΄})) |
39 | 37, 38 | imbitrdi 250 |
. . . . . . . . . 10
β’ (πΊ β UHGraph β ({π΄} β (EdgβπΊ) β βπ(π β dom (iEdgβπΊ) β§ ((iEdgβπΊ)βπ) = {π΄}))) |
40 | 18 | lp1cycl 29394 |
. . . . . . . . . . . 12
β’ ((πΊ β UHGraph β§ π β dom (iEdgβπΊ) β§ ((iEdgβπΊ)βπ) = {π΄}) β β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ©) |
41 | 40 | 3expib 1122 |
. . . . . . . . . . 11
β’ (πΊ β UHGraph β ((π β dom (iEdgβπΊ) β§ ((iEdgβπΊ)βπ) = {π΄}) β β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ©)) |
42 | 41 | eximdv 1920 |
. . . . . . . . . 10
β’ (πΊ β UHGraph β
(βπ(π β dom (iEdgβπΊ) β§ ((iEdgβπΊ)βπ) = {π΄}) β βπβ¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ©)) |
43 | 39, 42 | syld 47 |
. . . . . . . . 9
β’ (πΊ β UHGraph β ({π΄} β (EdgβπΊ) β βπβ¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ©)) |
44 | | s1len 14552 |
. . . . . . . . . . 11
β’
(β―ββ¨βπββ©) = 1 |
45 | 44 | ax-gen 1797 |
. . . . . . . . . 10
β’
βπ(β―ββ¨βπββ©) =
1 |
46 | | 19.29r 1877 |
. . . . . . . . . 10
β’
((βπβ¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§ βπ(β―ββ¨βπββ©) = 1) β
βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1)) |
47 | 45, 46 | mpan2 689 |
. . . . . . . . 9
β’
(βπβ¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1)) |
48 | 43, 47 | syl6 35 |
. . . . . . . 8
β’ (πΊ β UHGraph β ({π΄} β (EdgβπΊ) β βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1))) |
49 | 48 | imp 407 |
. . . . . . 7
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1)) |
50 | | uhgredgn0 28377 |
. . . . . . . . . . 11
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β {π΄} β (π« (VtxβπΊ) β
{β
})) |
51 | | eldifsni 4792 |
. . . . . . . . . . 11
β’ ({π΄} β (π«
(VtxβπΊ) β
{β
}) β {π΄} β
β
) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β {π΄} β β
) |
53 | | snnzb 4721 |
. . . . . . . . . 10
β’ (π΄ β V β {π΄} β β
) |
54 | 52, 53 | sylibr 233 |
. . . . . . . . 9
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β π΄ β V) |
55 | | s2fv0 14834 |
. . . . . . . . 9
β’ (π΄ β V β
(β¨βπ΄π΄ββ©β0) = π΄) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β (β¨βπ΄π΄ββ©β0) = π΄) |
57 | 56 | alrimiv 1930 |
. . . . . . 7
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β βπ(β¨βπ΄π΄ββ©β0) = π΄) |
58 | | 19.29r 1877 |
. . . . . . 7
β’
((βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1) β§ βπ(β¨βπ΄π΄ββ©β0) = π΄) β βπ((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1) β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
59 | 49, 57, 58 | syl2anc 584 |
. . . . . 6
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β βπ((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1) β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
60 | | df-3an 1089 |
. . . . . . 7
β’
((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β ((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1) β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
61 | 60 | exbii 1850 |
. . . . . 6
β’
(βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1) β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
62 | 59, 61 | sylibr 233 |
. . . . 5
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
63 | | s1cli 14551 |
. . . . . . . 8
β’
β¨βπββ© β Word V |
64 | | breq1 5150 |
. . . . . . . . . 10
β’ (π = β¨βπββ© β (π(CyclesβπΊ)β¨βπ΄π΄ββ© β β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ©)) |
65 | | fveqeq2 6897 |
. . . . . . . . . 10
β’ (π = β¨βπββ© β
((β―βπ) = 1
β (β―ββ¨βπββ©) = 1)) |
66 | 64, 65 | 3anbi12d 1437 |
. . . . . . . . 9
β’ (π = β¨βπββ© β ((π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β (β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄))) |
67 | 66 | rspcev 3612 |
. . . . . . . 8
β’
((β¨βπββ© β Word V β§
(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) β βπ β Word V(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
68 | 63, 67 | mpan 688 |
. . . . . . 7
β’
((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ β Word V(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
69 | | rexex 3076 |
. . . . . . 7
β’
(βπ β
Word V(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
70 | 68, 69 | syl 17 |
. . . . . 6
β’
((β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
71 | 70 | exlimiv 1933 |
. . . . 5
β’
(βπ(β¨βπββ©(CyclesβπΊ)β¨βπ΄π΄ββ© β§
(β―ββ¨βπββ©) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
72 | 62, 71 | syl 17 |
. . . 4
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β βπ(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) |
73 | | s2cli 14827 |
. . . . . . 7
β’
β¨βπ΄π΄ββ© β Word
V |
74 | | breq2 5151 |
. . . . . . . . 9
β’ (π = β¨βπ΄π΄ββ© β (π(CyclesβπΊ)π β π(CyclesβπΊ)β¨βπ΄π΄ββ©)) |
75 | | fveq1 6887 |
. . . . . . . . . 10
β’ (π = β¨βπ΄π΄ββ© β (πβ0) = (β¨βπ΄π΄ββ©β0)) |
76 | 75 | eqeq1d 2734 |
. . . . . . . . 9
β’ (π = β¨βπ΄π΄ββ© β ((πβ0) = π΄ β (β¨βπ΄π΄ββ©β0) = π΄)) |
77 | 74, 76 | 3anbi13d 1438 |
. . . . . . . 8
β’ (π = β¨βπ΄π΄ββ© β ((π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β (π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄))) |
78 | 77 | rspcev 3612 |
. . . . . . 7
β’
((β¨βπ΄π΄ββ© β Word V β§ (π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄)) β βπ β Word V(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄)) |
79 | 73, 78 | mpan 688 |
. . . . . 6
β’ ((π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ β Word V(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄)) |
80 | | rexex 3076 |
. . . . . 6
β’
(βπ β
Word V(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β βπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄)) |
81 | 79, 80 | syl 17 |
. . . . 5
β’ ((π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄)) |
82 | 81 | eximi 1837 |
. . . 4
β’
(βπ(π(CyclesβπΊ)β¨βπ΄π΄ββ© β§ (β―βπ) = 1 β§ (β¨βπ΄π΄ββ©β0) = π΄) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄)) |
83 | 72, 82 | syl 17 |
. . 3
β’ ((πΊ β UHGraph β§ {π΄} β (EdgβπΊ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄)) |
84 | 83 | ex 413 |
. 2
β’ (πΊ β UHGraph β ({π΄} β (EdgβπΊ) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄))) |
85 | 29, 84 | impbid 211 |
1
β’ (πΊ β UHGraph β
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 1 β§ (πβ0) = π΄) β {π΄} β (EdgβπΊ))) |