Step | Hyp | Ref
| Expression |
1 | | umgruhgr 28119 |
. . . . . 6
β’ (πΊ β UMGraph β πΊ β
UHGraph) |
2 | | umgr2wlk.e |
. . . . . . . 8
β’ πΈ = (EdgβπΊ) |
3 | 2 | eleq2i 2825 |
. . . . . . 7
β’ ({π΅, πΆ} β πΈ β {π΅, πΆ} β (EdgβπΊ)) |
4 | | eqid 2732 |
. . . . . . . 8
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
5 | 4 | uhgredgiedgb 28141 |
. . . . . . 7
β’ (πΊ β UHGraph β ({π΅, πΆ} β (EdgβπΊ) β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ))) |
6 | 3, 5 | bitrid 283 |
. . . . . 6
β’ (πΊ β UHGraph β ({π΅, πΆ} β πΈ β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ))) |
7 | 1, 6 | syl 17 |
. . . . 5
β’ (πΊ β UMGraph β ({π΅, πΆ} β πΈ β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ))) |
8 | 7 | biimpd 228 |
. . . 4
β’ (πΊ β UMGraph β ({π΅, πΆ} β πΈ β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ))) |
9 | 8 | a1d 25 |
. . 3
β’ (πΊ β UMGraph β ({π΄, π΅} β πΈ β ({π΅, πΆ} β πΈ β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ)))) |
10 | 9 | 3imp 1112 |
. 2
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ)) |
11 | 2 | eleq2i 2825 |
. . . . . . 7
β’ ({π΄, π΅} β πΈ β {π΄, π΅} β (EdgβπΊ)) |
12 | 4 | uhgredgiedgb 28141 |
. . . . . . 7
β’ (πΊ β UHGraph β ({π΄, π΅} β (EdgβπΊ) β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ))) |
13 | 11, 12 | bitrid 283 |
. . . . . 6
β’ (πΊ β UHGraph β ({π΄, π΅} β πΈ β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ))) |
14 | 1, 13 | syl 17 |
. . . . 5
β’ (πΊ β UMGraph β ({π΄, π΅} β πΈ β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ))) |
15 | 14 | biimpd 228 |
. . . 4
β’ (πΊ β UMGraph β ({π΄, π΅} β πΈ β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ))) |
16 | 15 | a1dd 50 |
. . 3
β’ (πΊ β UMGraph β ({π΄, π΅} β πΈ β ({π΅, πΆ} β πΈ β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ)))) |
17 | 16 | 3imp 1112 |
. 2
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ)) |
18 | | s2cli 14782 |
. . . . . . . . . 10
β’
β¨βππββ© β Word
V |
19 | | s3cli 14783 |
. . . . . . . . . 10
β’
β¨βπ΄π΅πΆββ© β Word V |
20 | 18, 19 | pm3.2i 472 |
. . . . . . . . 9
β’
(β¨βππββ© β Word V
β§ β¨βπ΄π΅πΆββ© β Word
V) |
21 | | eqid 2732 |
. . . . . . . . . 10
β’
β¨βππββ© =
β¨βππββ© |
22 | | eqid 2732 |
. . . . . . . . . 10
β’
β¨βπ΄π΅πΆββ© = β¨βπ΄π΅πΆββ© |
23 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ))) β πΊ β UMGraph) |
24 | | 3simpc 1151 |
. . . . . . . . . . 11
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
β’ (((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ))) β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) |
26 | | simpl 484 |
. . . . . . . . . . . 12
β’ (({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β {π΄, π΅} = ((iEdgβπΊ)βπ)) |
27 | 26 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β ((iEdgβπΊ)βπ) = {π΄, π΅}) |
28 | 27 | adantl 483 |
. . . . . . . . . 10
β’ (((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ))) β ((iEdgβπΊ)βπ) = {π΄, π΅}) |
29 | | simpr 486 |
. . . . . . . . . . . 12
β’ (({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β {π΅, πΆ} = ((iEdgβπΊ)βπ)) |
30 | 29 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ)) β ((iEdgβπΊ)βπ) = {π΅, πΆ}) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
β’ (((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ))) β ((iEdgβπΊ)βπ) = {π΅, πΆ}) |
32 | 2, 4, 21, 22, 23, 25, 28, 31 | umgr2adedgwlk 28954 |
. . . . . . . . 9
β’ (((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ))) β (β¨βππββ©(WalksβπΊ)β¨βπ΄π΅πΆββ© β§
(β―ββ¨βππββ©) = 2 β§ (π΄ = (β¨βπ΄π΅πΆββ©β0) β§ π΅ = (β¨βπ΄π΅πΆββ©β1) β§ πΆ = (β¨βπ΄π΅πΆββ©β2)))) |
33 | | breq12 5116 |
. . . . . . . . . . 11
β’ ((π = β¨βππββ© β§ π = β¨βπ΄π΅πΆββ©) β (π(WalksβπΊ)π β β¨βππββ©(WalksβπΊ)β¨βπ΄π΅πΆββ©)) |
34 | | fveqeq2 6857 |
. . . . . . . . . . . 12
β’ (π = β¨βππββ© β ((β―βπ) = 2 β
(β―ββ¨βππββ©) = 2)) |
35 | 34 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = β¨βππββ© β§ π = β¨βπ΄π΅πΆββ©) β ((β―βπ) = 2 β
(β―ββ¨βππββ©) = 2)) |
36 | | fveq1 6847 |
. . . . . . . . . . . . . 14
β’ (π = β¨βπ΄π΅πΆββ© β (πβ0) = (β¨βπ΄π΅πΆββ©β0)) |
37 | 36 | eqeq2d 2743 |
. . . . . . . . . . . . 13
β’ (π = β¨βπ΄π΅πΆββ© β (π΄ = (πβ0) β π΄ = (β¨βπ΄π΅πΆββ©β0))) |
38 | | fveq1 6847 |
. . . . . . . . . . . . . 14
β’ (π = β¨βπ΄π΅πΆββ© β (πβ1) = (β¨βπ΄π΅πΆββ©β1)) |
39 | 38 | eqeq2d 2743 |
. . . . . . . . . . . . 13
β’ (π = β¨βπ΄π΅πΆββ© β (π΅ = (πβ1) β π΅ = (β¨βπ΄π΅πΆββ©β1))) |
40 | | fveq1 6847 |
. . . . . . . . . . . . . 14
β’ (π = β¨βπ΄π΅πΆββ© β (πβ2) = (β¨βπ΄π΅πΆββ©β2)) |
41 | 40 | eqeq2d 2743 |
. . . . . . . . . . . . 13
β’ (π = β¨βπ΄π΅πΆββ© β (πΆ = (πβ2) β πΆ = (β¨βπ΄π΅πΆββ©β2))) |
42 | 37, 39, 41 | 3anbi123d 1437 |
. . . . . . . . . . . 12
β’ (π = β¨βπ΄π΅πΆββ© β ((π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)) β (π΄ = (β¨βπ΄π΅πΆββ©β0) β§ π΅ = (β¨βπ΄π΅πΆββ©β1) β§ πΆ = (β¨βπ΄π΅πΆββ©β2)))) |
43 | 42 | adantl 483 |
. . . . . . . . . . 11
β’ ((π = β¨βππββ© β§ π = β¨βπ΄π΅πΆββ©) β ((π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)) β (π΄ = (β¨βπ΄π΅πΆββ©β0) β§ π΅ = (β¨βπ΄π΅πΆββ©β1) β§ πΆ = (β¨βπ΄π΅πΆββ©β2)))) |
44 | 33, 35, 43 | 3anbi123d 1437 |
. . . . . . . . . 10
β’ ((π = β¨βππββ© β§ π = β¨βπ΄π΅πΆββ©) β ((π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2))) β (β¨βππββ©(WalksβπΊ)β¨βπ΄π΅πΆββ© β§
(β―ββ¨βππββ©) = 2 β§ (π΄ = (β¨βπ΄π΅πΆββ©β0) β§ π΅ = (β¨βπ΄π΅πΆββ©β1) β§ πΆ = (β¨βπ΄π΅πΆββ©β2))))) |
45 | 44 | spc2egv 3560 |
. . . . . . . . 9
β’
((β¨βππββ© β Word V β§
β¨βπ΄π΅πΆββ© β Word V) β
((β¨βππββ©(WalksβπΊ)β¨βπ΄π΅πΆββ© β§
(β―ββ¨βππββ©) = 2 β§ (π΄ = (β¨βπ΄π΅πΆββ©β0) β§ π΅ = (β¨βπ΄π΅πΆββ©β1) β§ πΆ = (β¨βπ΄π΅πΆββ©β2))) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2))))) |
46 | 20, 32, 45 | mpsyl 68 |
. . . . . . . 8
β’ (((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({π΄, π΅} = ((iEdgβπΊ)βπ) β§ {π΅, πΆ} = ((iEdgβπΊ)βπ))) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))) |
47 | 46 | exp32 422 |
. . . . . . 7
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ({π΄, π΅} = ((iEdgβπΊ)βπ) β ({π΅, πΆ} = ((iEdgβπΊ)βπ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))))) |
48 | 47 | com12 32 |
. . . . . 6
β’ ({π΄, π΅} = ((iEdgβπΊ)βπ) β ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ({π΅, πΆ} = ((iEdgβπΊ)βπ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))))) |
49 | 48 | rexlimivw 3145 |
. . . . 5
β’
(βπ β dom
(iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ({π΅, πΆ} = ((iEdgβπΊ)βπ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))))) |
50 | 49 | com13 88 |
. . . 4
β’ ({π΅, πΆ} = ((iEdgβπΊ)βπ) β ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β (βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))))) |
51 | 50 | rexlimivw 3145 |
. . 3
β’
(βπ β dom
(iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β (βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))))) |
52 | 51 | com12 32 |
. 2
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β (βπ β dom (iEdgβπΊ){π΅, πΆ} = ((iEdgβπΊ)βπ) β (βπ β dom (iEdgβπΊ){π΄, π΅} = ((iEdgβπΊ)βπ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))))) |
53 | 10, 17, 52 | mp2d 49 |
1
β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))) |