Step | Hyp | Ref
| Expression |
1 | | isclwlke.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | | isclwlke.i |
. . . 4
β’ πΌ = (iEdgβπΊ) |
3 | | clwlkcomp.1 |
. . . 4
β’ πΉ = (1st βπ) |
4 | | clwlkcomp.2 |
. . . 4
β’ π = (2nd βπ) |
5 | 1, 2, 3, 4 | clwlkcompim 28770 |
. . 3
β’ (π β (ClWalksβπΊ) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) |
6 | 5 | adantl 483 |
. 2
β’ ((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) |
7 | | simprl 770 |
. . 3
β’ (((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β§ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ)) |
8 | | clwlkwlk 28765 |
. . . . 5
β’ (π β (ClWalksβπΊ) β π β (WalksβπΊ)) |
9 | 1, 2, 3, 4 | upgrwlkcompim 28633 |
. . . . . 6
β’ ((πΊ β UPGraph β§ π β (WalksβπΊ)) β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
10 | 9 | simp3d 1145 |
. . . . 5
β’ ((πΊ β UPGraph β§ π β (WalksβπΊ)) β βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
11 | 8, 10 | sylan2 594 |
. . . 4
β’ ((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
12 | 11 | adantr 482 |
. . 3
β’ (((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β§ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) β βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
13 | | simprrr 781 |
. . 3
β’ (((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β§ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) β (πβ0) = (πβ(β―βπΉ))) |
14 | 7, 12, 13 | 3jca 1129 |
. 2
β’ (((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β§ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))) |
15 | 6, 14 | mpdan 686 |
1
β’ ((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))) |