Step | Hyp | Ref
| Expression |
1 | | wlkson.v |
. . . . . 6
β’ π = (VtxβπΊ) |
2 | 1 | fvexi 6860 |
. . . . 5
β’ π β V |
3 | | df-wlkson 28597 |
. . . . . 6
β’ WalksOn =
(π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π)})) |
4 | 1 | wlkson 28653 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β (π΄(WalksOnβπΊ)π΅) = {β¨π, πβ© β£ (π(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπ)) = π΅)}) |
5 | 4 | 3adant1 1131 |
. . . . . 6
β’ ((πΊ β V β§ π΄ β π β§ π΅ β π) β (π΄(WalksOnβπΊ)π΅) = {β¨π, πβ© β£ (π(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπ)) = π΅)}) |
6 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
7 | 6, 1 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = π) |
8 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΊ β (Walksβπ) = (WalksβπΊ)) |
9 | 8 | breqd 5120 |
. . . . . . 7
β’ (π = πΊ β (π(Walksβπ)π β π(WalksβπΊ)π)) |
10 | 9 | 3anbi1d 1441 |
. . . . . 6
β’ (π = πΊ β ((π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π) β (π(WalksβπΊ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π))) |
11 | 3, 5, 7, 7, 10 | bropfvvvv 8028 |
. . . . 5
β’ ((π β V β§ π β V) β (πΉ(π΄(WalksOnβπΊ)π΅)π β (πΊ β V β§ (π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)))) |
12 | 2, 2, 11 | mp2an 691 |
. . . 4
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β (πΊ β V β§ (π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V))) |
13 | | 3anass 1096 |
. . . . . 6
β’ ((πΊ β V β§ π΄ β π β§ π΅ β π) β (πΊ β V β§ (π΄ β π β§ π΅ β π))) |
14 | 13 | anbi1i 625 |
. . . . 5
β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β ((πΊ β V β§ (π΄ β π β§ π΅ β π)) β§ (πΉ β V β§ π β V))) |
15 | | df-3an 1090 |
. . . . 5
β’ ((πΊ β V β§ (π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β ((πΊ β V β§ (π΄ β π β§ π΅ β π)) β§ (πΉ β V β§ π β V))) |
16 | 14, 15 | bitr4i 278 |
. . . 4
β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β (πΊ β V β§ (π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V))) |
17 | 12, 16 | sylibr 233 |
. . 3
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V))) |
18 | 1 | iswlkon 28654 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β (πΉ(π΄(WalksOnβπΊ)π΅)π β (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
19 | 18 | 3adantl1 1167 |
. . . . 5
β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β (πΉ(π΄(WalksOnβπΊ)π΅)π β (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
20 | 19 | biimpd 228 |
. . . 4
β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β (πΉ(π΄(WalksOnβπΊ)π΅)π β (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
21 | 20 | imdistani 570 |
. . 3
β’ ((((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β§ πΉ(π΄(WalksOnβπΊ)π΅)π) β (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
22 | 17, 21 | mpancom 687 |
. 2
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
23 | | df-3an 1090 |
. 2
β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
24 | 22, 23 | sylibr 233 |
1
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |