Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | 1 | wlkonprop 28915 |
. 2
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
3 | 1 | wlkonprop 28915 |
. 2
β’ (π»(πΆ(WalksOnβπΊ)π·)π β ((πΊ β V β§ πΆ β (VtxβπΊ) β§ π· β (VtxβπΊ)) β§ (π» β V β§ π β V) β§ (π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·))) |
4 | | simp2 1138 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ0) = π΄) |
5 | 4 | eqcomd 2739 |
. . . . . . . . 9
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β π΄ = (πβ0)) |
6 | | simp2 1138 |
. . . . . . . . 9
β’ ((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β (πβ0) = πΆ) |
7 | 5, 6 | sylan9eqr 2795 |
. . . . . . . 8
β’ (((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β π΄ = πΆ) |
8 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ(β―βπΉ)) = π΅) |
9 | 8 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β π΅ = (πβ(β―βπΉ))) |
10 | 9 | adantl 483 |
. . . . . . . . 9
β’ (((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β π΅ = (πβ(β―βπΉ))) |
11 | | wlklenvm1 28879 |
. . . . . . . . . . . 12
β’ (π»(WalksβπΊ)π β (β―βπ») = ((β―βπ) β 1)) |
12 | | wlklenvm1 28879 |
. . . . . . . . . . . . . . 15
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) = ((β―βπ) β 1)) |
13 | | eqtr3 2759 |
. . . . . . . . . . . . . . . . 17
β’
(((β―βπΉ)
= ((β―βπ)
β 1) β§ (β―βπ») = ((β―βπ) β 1)) β (β―βπΉ) = (β―βπ»)) |
14 | 13 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπΉ)
= ((β―βπ)
β 1) β§ (β―βπ») = ((β―βπ) β 1)) β (πβ(β―βπΉ)) = (πβ(β―βπ»))) |
15 | 14 | ex 414 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ) =
((β―βπ) β
1) β ((β―βπ») = ((β―βπ) β 1) β (πβ(β―βπΉ)) = (πβ(β―βπ»)))) |
16 | 12, 15 | syl 17 |
. . . . . . . . . . . . . 14
β’ (πΉ(WalksβπΊ)π β ((β―βπ») = ((β―βπ) β 1) β (πβ(β―βπΉ)) = (πβ(β―βπ»)))) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((β―βπ») = ((β―βπ) β 1) β (πβ(β―βπΉ)) = (πβ(β―βπ»)))) |
18 | 17 | com12 32 |
. . . . . . . . . . . 12
β’
((β―βπ») =
((β―βπ) β
1) β ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ(β―βπΉ)) = (πβ(β―βπ»)))) |
19 | 11, 18 | syl 17 |
. . . . . . . . . . 11
β’ (π»(WalksβπΊ)π β ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ(β―βπΉ)) = (πβ(β―βπ»)))) |
20 | 19 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πβ(β―βπΉ)) = (πβ(β―βπ»)))) |
21 | 20 | imp 408 |
. . . . . . . . 9
β’ (((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β (πβ(β―βπΉ)) = (πβ(β―βπ»))) |
22 | | simpl3 1194 |
. . . . . . . . 9
β’ (((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β (πβ(β―βπ»)) = π·) |
23 | 10, 21, 22 | 3eqtrd 2777 |
. . . . . . . 8
β’ (((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β π΅ = π·) |
24 | 7, 23 | jca 513 |
. . . . . . 7
β’ (((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β (π΄ = πΆ β§ π΅ = π·)) |
25 | 24 | ex 414 |
. . . . . 6
β’ ((π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·) β ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (π΄ = πΆ β§ π΅ = π·))) |
26 | 25 | 3ad2ant3 1136 |
. . . . 5
β’ (((πΊ β V β§ πΆ β (VtxβπΊ) β§ π· β (VtxβπΊ)) β§ (π» β V β§ π β V) β§ (π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·)) β ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (π΄ = πΆ β§ π΅ = π·))) |
27 | 26 | com12 32 |
. . . 4
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (((πΊ β V β§ πΆ β (VtxβπΊ) β§ π· β (VtxβπΊ)) β§ (π» β V β§ π β V) β§ (π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·)) β (π΄ = πΆ β§ π΅ = π·))) |
28 | 27 | 3ad2ant3 1136 |
. . 3
β’ (((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β (((πΊ β V β§ πΆ β (VtxβπΊ) β§ π· β (VtxβπΊ)) β§ (π» β V β§ π β V) β§ (π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·)) β (π΄ = πΆ β§ π΅ = π·))) |
29 | 28 | imp 408 |
. 2
β’ ((((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ ((πΊ β V β§ πΆ β (VtxβπΊ) β§ π· β (VtxβπΊ)) β§ (π» β V β§ π β V) β§ (π»(WalksβπΊ)π β§ (πβ0) = πΆ β§ (πβ(β―βπ»)) = π·))) β (π΄ = πΆ β§ π΅ = π·)) |
30 | 2, 3, 29 | syl2an 597 |
1
β’ ((πΉ(π΄(WalksOnβπΊ)π΅)π β§ π»(πΆ(WalksOnβπΊ)π·)π) β (π΄ = πΆ β§ π΅ = π·)) |