Step | Hyp | Ref
| Expression |
1 | | uhgr3cyclex.e |
. . . . . . 7
β’ πΈ = (EdgβπΊ) |
2 | 1 | eleq2i 2819 |
. . . . . 6
β’ ({π΄, π΅} β πΈ β {π΄, π΅} β (EdgβπΊ)) |
3 | | eqid 2726 |
. . . . . . 7
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
4 | 3 | uhgredgiedgb 28894 |
. . . . . 6
β’ (πΊ β UHGraph β ({π΄, π΅} β (EdgβπΊ) β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ))) |
5 | 2, 4 | bitrid 283 |
. . . . 5
β’ (πΊ β UHGraph β ({π΄, π΅} β πΈ β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ))) |
6 | 1 | eleq2i 2819 |
. . . . . 6
β’ ({π΅, πΆ} β πΈ β {π΅, πΆ} β (EdgβπΊ)) |
7 | 3 | uhgredgiedgb 28894 |
. . . . . 6
β’ (πΊ β UHGraph β ({π΅, πΆ} β (EdgβπΊ) β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ))) |
8 | 6, 7 | bitrid 283 |
. . . . 5
β’ (πΊ β UHGraph β ({π΅, πΆ} β πΈ β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ))) |
9 | 1 | eleq2i 2819 |
. . . . . 6
β’ ({πΆ, π΄} β πΈ β {πΆ, π΄} β (EdgβπΊ)) |
10 | 3 | uhgredgiedgb 28894 |
. . . . . 6
β’ (πΊ β UHGraph β ({πΆ, π΄} β (EdgβπΊ) β βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ))) |
11 | 9, 10 | bitrid 283 |
. . . . 5
β’ (πΊ β UHGraph β ({πΆ, π΄} β πΈ β βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ))) |
12 | 5, 8, 11 | 3anbi123d 1432 |
. . . 4
β’ (πΊ β UHGraph β (({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ) β (βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ)))) |
13 | 12 | adantr 480 |
. . 3
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β (({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ) β (βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ)))) |
14 | | eqid 2726 |
. . . . . . . . . . . . . 14
β’
β¨βπ΄π΅πΆπ΄ββ© = β¨βπ΄π΅πΆπ΄ββ© |
15 | | eqid 2726 |
. . . . . . . . . . . . . 14
β’
β¨βπππββ© = β¨βπππββ© |
16 | | 3simpa 1145 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΄ β π β§ π΅ β π)) |
17 | | pm3.22 459 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β π β§ πΆ β π) β (πΆ β π β§ π΄ β π)) |
18 | 17 | 3adant2 1128 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (πΆ β π β§ π΄ β π)) |
19 | 16, 18 | jca 511 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π΄ β π))) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π΄ β π))) |
21 | 20 | ad2antlr 724 |
. . . . . . . . . . . . . 14
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π΄ β π))) |
22 | | 3simpa 1145 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β (π΄ β π΅ β§ π΄ β πΆ)) |
23 | | necom 2988 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β π΅ β π΅ β π΄) |
24 | 23 | biimpi 215 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β π΅ β π΅ β π΄) |
25 | 24 | anim1ci 615 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β π΅ β§ π΅ β πΆ) β (π΅ β πΆ β§ π΅ β π΄)) |
26 | 25 | 3adant2 1128 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β (π΅ β πΆ β§ π΅ β π΄)) |
27 | | necom 2988 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β πΆ β πΆ β π΄) |
28 | 27 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β πΆ β πΆ β π΄) |
29 | 28 | 3ad2ant2 1131 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β πΆ β π΄) |
30 | 22, 26, 29 | 3jca 1125 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π΄) β§ πΆ β π΄)) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π΄) β§ πΆ β π΄)) |
32 | 31 | ad2antlr 724 |
. . . . . . . . . . . . . 14
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π΄) β§ πΆ β π΄)) |
33 | | eqimss 4035 |
. . . . . . . . . . . . . . . . . 18
β’ ({π΄, π΅} = ((iEdgβπΊ)βπ) β {π΄, π΅} β ((iEdgβπΊ)βπ)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β {π΄, π΅} β ((iEdgβπΊ)βπ)) |
35 | 34 | 3ad2ant3 1132 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β {π΄, π΅} β ((iEdgβπΊ)βπ)) |
36 | | eqimss 4035 |
. . . . . . . . . . . . . . . . . 18
β’ ({π΅, πΆ} = ((iEdgβπΊ)βπ) β {π΅, πΆ} β ((iEdgβπΊ)βπ)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β {π΅, πΆ} β ((iEdgβπΊ)βπ)) |
38 | 37 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β {π΅, πΆ} β ((iEdgβπΊ)βπ)) |
39 | | eqimss 4035 |
. . . . . . . . . . . . . . . . . 18
β’ ({πΆ, π΄} = ((iEdgβπΊ)βπ) β {πΆ, π΄} β ((iEdgβπΊ)βπ)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β {πΆ, π΄} β ((iEdgβπΊ)βπ)) |
41 | 40 | 3ad2ant2 1131 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β {πΆ, π΄} β ((iEdgβπΊ)βπ)) |
42 | 35, 38, 41 | 3jca 1125 |
. . . . . . . . . . . . . . 15
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β ({π΄, π΅} β ((iEdgβπΊ)βπ) β§ {π΅, πΆ} β ((iEdgβπΊ)βπ) β§ {πΆ, π΄} β ((iEdgβπΊ)βπ))) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . 14
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β ({π΄, π΅} β ((iEdgβπΊ)βπ) β§ {π΅, πΆ} β ((iEdgβπΊ)βπ) β§ {πΆ, π΄} β ((iEdgβπΊ)βπ))) |
44 | | uhgr3cyclex.v |
. . . . . . . . . . . . . 14
β’ π = (VtxβπΊ) |
45 | | simp3 1135 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β πΆ β π) |
46 | | simp1 1133 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β π΄ β π) |
47 | 45, 46 | jca 511 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (πΆ β π β§ π΄ β π)) |
48 | 47, 29 | anim12i 612 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β ((πΆ β π β§ π΄ β π) β§ πΆ β π΄)) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β ((πΆ β π β§ π΄ β π) β§ πΆ β π΄)) |
50 | | pm3.22 459 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)))) |
51 | 50 | 3adant2 1128 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)))) |
52 | 44, 1, 3 | uhgr3cyclexlem 29943 |
. . . . . . . . . . . . . . . 16
β’ ((((πΆ β π β§ π΄ β π) β§ πΆ β π΄) β§ ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)))) β π β π) |
53 | 49, 51, 52 | syl2an 595 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β π β π) |
54 | | 3simpc 1147 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΅ β π β§ πΆ β π)) |
55 | | simp3 1135 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β π΅ β πΆ) |
56 | 54, 55 | anim12i 612 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β ((π΅ β π β§ πΆ β π) β§ π΅ β πΆ)) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β ((π΅ β π β§ πΆ β π) β§ π΅ β πΆ)) |
58 | | 3simpc 1147 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) |
59 | 44, 1, 3 | uhgr3cyclexlem 29943 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΅ β π β§ πΆ β π) β§ π΅ β πΆ) β§ ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β π β π) |
60 | 59 | necomd 2990 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β π β§ πΆ β π) β§ π΅ β πΆ) β§ ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β π β π) |
61 | 57, 58, 60 | syl2an 595 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β π β π) |
62 | 44, 1, 3 | uhgr3cyclexlem 29943 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β π β§ π΅ β π) β§ π΄ β π΅) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)))) β π β π) |
63 | 62 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ β π β§ π΅ β π) β (π΄ β π΅ β (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β π β π))) |
64 | 63 | 3adant3 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΄ β π΅ β (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β π β π))) |
65 | 64 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ β π΅ β ((π΄ β π β§ π΅ β π β§ πΆ β π) β (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β π β π))) |
66 | 65 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β ((π΄ β π β§ π΅ β π β§ πΆ β π) β (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β π β π))) |
67 | 66 | impcom 407 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β π β π)) |
68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β π β π)) |
69 | 68 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ))) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β π β π)) |
70 | 69 | 3adant3 1129 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β π β π)) |
71 | 70 | impcom 407 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β π β π) |
72 | 53, 61, 71 | 3jca 1125 |
. . . . . . . . . . . . . 14
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β (π β π β§ π β π β§ π β π)) |
73 | | eqidd 2727 |
. . . . . . . . . . . . . 14
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β π΄ = π΄) |
74 | 14, 15, 21, 32, 43, 44, 3, 72, 73 | 3cyclpd 29941 |
. . . . . . . . . . . . 13
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β (β¨βπππββ©(CyclesβπΊ)β¨βπ΄π΅πΆπ΄ββ© β§
(β―ββ¨βπππββ©) = 3 β§ (β¨βπ΄π΅πΆπ΄ββ©β0) = π΄)) |
75 | | s3cli 14838 |
. . . . . . . . . . . . . . 15
β’
β¨βπππββ© β Word V |
76 | 75 | elexi 3488 |
. . . . . . . . . . . . . 14
β’
β¨βπππββ© β V |
77 | | s4cli 14839 |
. . . . . . . . . . . . . . 15
β’
β¨βπ΄π΅πΆπ΄ββ© β Word V |
78 | 77 | elexi 3488 |
. . . . . . . . . . . . . 14
β’
β¨βπ΄π΅πΆπ΄ββ© β V |
79 | | breq12 5146 |
. . . . . . . . . . . . . . 15
β’ ((π = β¨βπππββ© β§ π = β¨βπ΄π΅πΆπ΄ββ©) β (π(CyclesβπΊ)π β β¨βπππββ©(CyclesβπΊ)β¨βπ΄π΅πΆπ΄ββ©)) |
80 | | fveqeq2 6894 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨βπππββ© β ((β―βπ) = 3 β
(β―ββ¨βπππββ©) = 3)) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π = β¨βπππββ© β§ π = β¨βπ΄π΅πΆπ΄ββ©) β ((β―βπ) = 3 β
(β―ββ¨βπππββ©) = 3)) |
82 | | fveq1 6884 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¨βπ΄π΅πΆπ΄ββ© β (πβ0) = (β¨βπ΄π΅πΆπ΄ββ©β0)) |
83 | 82 | eqeq1d 2728 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨βπ΄π΅πΆπ΄ββ© β ((πβ0) = π΄ β (β¨βπ΄π΅πΆπ΄ββ©β0) = π΄)) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((π = β¨βπππββ© β§ π = β¨βπ΄π΅πΆπ΄ββ©) β ((πβ0) = π΄ β (β¨βπ΄π΅πΆπ΄ββ©β0) = π΄)) |
85 | 79, 81, 84 | 3anbi123d 1432 |
. . . . . . . . . . . . . 14
β’ ((π = β¨βπππββ© β§ π = β¨βπ΄π΅πΆπ΄ββ©) β ((π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄) β (β¨βπππββ©(CyclesβπΊ)β¨βπ΄π΅πΆπ΄ββ© β§
(β―ββ¨βπππββ©) = 3 β§ (β¨βπ΄π΅πΆπ΄ββ©β0) = π΄))) |
86 | 76, 78, 85 | spc2ev 3591 |
. . . . . . . . . . . . 13
β’
((β¨βπππββ©(CyclesβπΊ)β¨βπ΄π΅πΆπ΄ββ© β§
(β―ββ¨βπππββ©) = 3 β§ (β¨βπ΄π΅πΆπ΄ββ©β0) = π΄) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) |
87 | 74, 86 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β§ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) |
88 | 87 | expcom 413 |
. . . . . . . . . . 11
β’ (((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β§ (π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ))) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))) |
89 | 88 | 3exp 1116 |
. . . . . . . . . 10
β’ ((π β dom (iEdgβπΊ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))))) |
90 | 89 | rexlimiva 3141 |
. . . . . . . . 9
β’
(βπ β dom
(iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))))) |
91 | 90 | com12 32 |
. . . . . . . 8
β’ ((π β dom (iEdgβπΊ) β§ {πΆ, π΄} = ((iEdgβπΊ)βπ)) β (βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))))) |
92 | 91 | rexlimiva 3141 |
. . . . . . 7
β’
(βπ β dom
(iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ) β (βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))))) |
93 | 92 | com13 88 |
. . . . . 6
β’ ((π β dom (iEdgβπΊ) β§ {π΄, π΅} = ((iEdgβπΊ)βπ)) β (βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β (βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))))) |
94 | 93 | rexlimiva 3141 |
. . . . 5
β’
(βπ β dom
(iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β (βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β (βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))))) |
95 | 94 | 3imp 1108 |
. . . 4
β’
((βπ β
dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ)) β ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))) |
96 | 95 | com12 32 |
. . 3
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β ((βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β§ βπ β dom (iEdgβπΊ){πΆ, π΄} = ((iEdgβπΊ)βπ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))) |
97 | 13, 96 | sylbid 239 |
. 2
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ))) β (({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄))) |
98 | 97 | 3impia 1114 |
1
β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) |