Step | Hyp | Ref
| Expression |
1 | | umgr2adedgwlk.p |
. . 3
β’ π = β¨βπ΄π΅πΆββ© |
2 | | umgr2adedgwlk.f |
. . 3
β’ πΉ = β¨βπ½πΎββ© |
3 | | umgr2adedgwlk.g |
. . . . . 6
β’ (π β πΊ β UMGraph) |
4 | | umgr2adedgwlk.a |
. . . . . 6
β’ (π β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) |
5 | | 3anass 1095 |
. . . . . 6
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β (πΊ β UMGraph β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ))) |
6 | 3, 4, 5 | sylanbrc 584 |
. . . . 5
β’ (π β (πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) |
7 | | umgr2adedgwlk.e |
. . . . . 6
β’ πΈ = (EdgβπΊ) |
8 | 7 | umgr2adedgwlklem 28354 |
. . . . 5
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ((π΄ β π΅ β§ π΅ β πΆ) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ) β§ πΆ β (VtxβπΊ)))) |
9 | 6, 8 | syl 17 |
. . . 4
β’ (π β ((π΄ β π΅ β§ π΅ β πΆ) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ) β§ πΆ β (VtxβπΊ)))) |
10 | 9 | simprd 497 |
. . 3
β’ (π β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ) β§ πΆ β (VtxβπΊ))) |
11 | 9 | simpld 496 |
. . 3
β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) |
12 | | ssid 3948 |
. . . . 5
β’ {π΄, π΅} β {π΄, π΅} |
13 | | umgr2adedgwlk.j |
. . . . 5
β’ (π β (πΌβπ½) = {π΄, π΅}) |
14 | 12, 13 | sseqtrrid 3979 |
. . . 4
β’ (π β {π΄, π΅} β (πΌβπ½)) |
15 | | ssid 3948 |
. . . . 5
β’ {π΅, πΆ} β {π΅, πΆ} |
16 | | umgr2adedgwlk.k |
. . . . 5
β’ (π β (πΌβπΎ) = {π΅, πΆ}) |
17 | 15, 16 | sseqtrrid 3979 |
. . . 4
β’ (π β {π΅, πΆ} β (πΌβπΎ)) |
18 | 14, 17 | jca 513 |
. . 3
β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) |
19 | | eqid 2736 |
. . 3
β’
(VtxβπΊ) =
(VtxβπΊ) |
20 | | umgr2adedgwlk.i |
. . 3
β’ πΌ = (iEdgβπΊ) |
21 | 1, 2, 10, 11, 18, 19, 20 | 2wlkd 28346 |
. 2
β’ (π β πΉ(WalksβπΊ)π) |
22 | 2 | fveq2i 6807 |
. . . 4
β’
(β―βπΉ) =
(β―ββ¨βπ½πΎββ©) |
23 | | s2len 14647 |
. . . 4
β’
(β―ββ¨βπ½πΎββ©) = 2 |
24 | 22, 23 | eqtri 2764 |
. . 3
β’
(β―βπΉ) =
2 |
25 | 24 | a1i 11 |
. 2
β’ (π β (β―βπΉ) = 2) |
26 | | s3fv0 14649 |
. . . . 5
β’ (π΄ β (VtxβπΊ) β (β¨βπ΄π΅πΆββ©β0) = π΄) |
27 | | s3fv1 14650 |
. . . . 5
β’ (π΅ β (VtxβπΊ) β (β¨βπ΄π΅πΆββ©β1) = π΅) |
28 | | s3fv2 14651 |
. . . . 5
β’ (πΆ β (VtxβπΊ) β (β¨βπ΄π΅πΆββ©β2) = πΆ) |
29 | 26, 27, 28 | 3anim123i 1151 |
. . . 4
β’ ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ) β§ πΆ β (VtxβπΊ)) β ((β¨βπ΄π΅πΆββ©β0) = π΄ β§ (β¨βπ΄π΅πΆββ©β1) = π΅ β§ (β¨βπ΄π΅πΆββ©β2) = πΆ)) |
30 | 10, 29 | syl 17 |
. . 3
β’ (π β ((β¨βπ΄π΅πΆββ©β0) = π΄ β§ (β¨βπ΄π΅πΆββ©β1) = π΅ β§ (β¨βπ΄π΅πΆββ©β2) = πΆ)) |
31 | 1 | fveq1i 6805 |
. . . . . 6
β’ (πβ0) = (β¨βπ΄π΅πΆββ©β0) |
32 | 31 | eqeq2i 2749 |
. . . . 5
β’ (π΄ = (πβ0) β π΄ = (β¨βπ΄π΅πΆββ©β0)) |
33 | | eqcom 2743 |
. . . . 5
β’ (π΄ = (β¨βπ΄π΅πΆββ©β0) β
(β¨βπ΄π΅πΆββ©β0) = π΄) |
34 | 32, 33 | bitri 275 |
. . . 4
β’ (π΄ = (πβ0) β (β¨βπ΄π΅πΆββ©β0) = π΄) |
35 | 1 | fveq1i 6805 |
. . . . . 6
β’ (πβ1) = (β¨βπ΄π΅πΆββ©β1) |
36 | 35 | eqeq2i 2749 |
. . . . 5
β’ (π΅ = (πβ1) β π΅ = (β¨βπ΄π΅πΆββ©β1)) |
37 | | eqcom 2743 |
. . . . 5
β’ (π΅ = (β¨βπ΄π΅πΆββ©β1) β
(β¨βπ΄π΅πΆββ©β1) = π΅) |
38 | 36, 37 | bitri 275 |
. . . 4
β’ (π΅ = (πβ1) β (β¨βπ΄π΅πΆββ©β1) = π΅) |
39 | 1 | fveq1i 6805 |
. . . . . 6
β’ (πβ2) = (β¨βπ΄π΅πΆββ©β2) |
40 | 39 | eqeq2i 2749 |
. . . . 5
β’ (πΆ = (πβ2) β πΆ = (β¨βπ΄π΅πΆββ©β2)) |
41 | | eqcom 2743 |
. . . . 5
β’ (πΆ = (β¨βπ΄π΅πΆββ©β2) β
(β¨βπ΄π΅πΆββ©β2) = πΆ) |
42 | 40, 41 | bitri 275 |
. . . 4
β’ (πΆ = (πβ2) β (β¨βπ΄π΅πΆββ©β2) = πΆ) |
43 | 34, 38, 42 | 3anbi123i 1155 |
. . 3
β’ ((π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)) β ((β¨βπ΄π΅πΆββ©β0) = π΄ β§ (β¨βπ΄π΅πΆββ©β1) = π΅ β§ (β¨βπ΄π΅πΆββ©β2) = πΆ)) |
44 | 30, 43 | sylibr 233 |
. 2
β’ (π β (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2))) |
45 | 21, 25, 44 | 3jca 1128 |
1
β’ (π β (πΉ(WalksβπΊ)π β§ (β―βπΉ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))) |