Step | Hyp | Ref
| Expression |
1 | | subgrv 28795 |
. . . . . 6
β’ (π SubGraph πΊ β (π β V β§ πΊ β V)) |
2 | 1 | simpld 494 |
. . . . 5
β’ (π SubGraph πΊ β π β V) |
3 | | eqid 2731 |
. . . . . 6
β’
(Vtxβπ) =
(Vtxβπ) |
4 | | eqid 2731 |
. . . . . 6
β’
(iEdgβπ) =
(iEdgβπ) |
5 | 3, 4 | iswlkg 29138 |
. . . . 5
β’ (π β V β (πΉ(Walksβπ)π β (πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))))) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (π SubGraph πΊ β (πΉ(Walksβπ)π β (πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))))) |
7 | | 3simpa 1147 |
. . . . . 6
β’ ((πΉ β Word dom
(iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))) β (πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ))) |
8 | | eqid 2731 |
. . . . . . . . . . 11
β’
(VtxβπΊ) =
(VtxβπΊ) |
9 | | eqid 2731 |
. . . . . . . . . . 11
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
10 | | eqid 2731 |
. . . . . . . . . . 11
β’
(Edgβπ) =
(Edgβπ) |
11 | 3, 8, 4, 9, 10 | subgrprop2 28799 |
. . . . . . . . . 10
β’ (π SubGraph πΊ β ((Vtxβπ) β (VtxβπΊ) β§ (iEdgβπ) β (iEdgβπΊ) β§ (Edgβπ) β π« (Vtxβπ))) |
12 | 11 | simp2d 1142 |
. . . . . . . . 9
β’ (π SubGraph πΊ β (iEdgβπ) β (iEdgβπΊ)) |
13 | | dmss 5902 |
. . . . . . . . 9
β’
((iEdgβπ)
β (iEdgβπΊ)
β dom (iEdgβπ)
β dom (iEdgβπΊ)) |
14 | | sswrd 14477 |
. . . . . . . . 9
β’ (dom
(iEdgβπ) β dom
(iEdgβπΊ) β Word
dom (iEdgβπ) β
Word dom (iEdgβπΊ)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . 8
β’ (π SubGraph πΊ β Word dom (iEdgβπ) β Word dom
(iEdgβπΊ)) |
16 | 15 | sseld 3981 |
. . . . . . 7
β’ (π SubGraph πΊ β (πΉ β Word dom (iEdgβπ) β πΉ β Word dom (iEdgβπΊ))) |
17 | 11 | simp1d 1141 |
. . . . . . . 8
β’ (π SubGraph πΊ β (Vtxβπ) β (VtxβπΊ)) |
18 | | fss 6734 |
. . . . . . . . 9
β’ ((π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ (Vtxβπ) β (VtxβπΊ)) β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) |
19 | 18 | expcom 413 |
. . . . . . . 8
β’
((Vtxβπ)
β (VtxβπΊ)
β (π:(0...(β―βπΉ))βΆ(Vtxβπ) β π:(0...(β―βπΉ))βΆ(VtxβπΊ))) |
20 | 17, 19 | syl 17 |
. . . . . . 7
β’ (π SubGraph πΊ β (π:(0...(β―βπΉ))βΆ(Vtxβπ) β π:(0...(β―βπΉ))βΆ(VtxβπΊ))) |
21 | 16, 20 | anim12d 608 |
. . . . . 6
β’ (π SubGraph πΊ β ((πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ)) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)))) |
22 | 7, 21 | syl5 34 |
. . . . 5
β’ (π SubGraph πΊ β ((πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)))) |
23 | | 3simpb 1148 |
. . . . . 6
β’ ((πΉ β Word dom
(iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))) β (πΉ β Word dom (iEdgβπ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))))) |
24 | 3, 8, 4, 9, 10 | subgrprop 28798 |
. . . . . . . . . . . . . . . . 17
β’ (π SubGraph πΊ β ((Vtxβπ) β (VtxβπΊ) β§ (iEdgβπ) = ((iEdgβπΊ) βΎ dom (iEdgβπ)) β§ (Edgβπ) β π« (Vtxβπ))) |
25 | 24 | simp2d 1142 |
. . . . . . . . . . . . . . . 16
β’ (π SubGraph πΊ β (iEdgβπ) = ((iEdgβπΊ) βΎ dom (iEdgβπ))) |
26 | 25 | fveq1d 6893 |
. . . . . . . . . . . . . . 15
β’ (π SubGraph πΊ β ((iEdgβπ)β(πΉβπ)) = (((iEdgβπΊ) βΎ dom (iEdgβπ))β(πΉβπ))) |
27 | 26 | 3ad2ant1 1132 |
. . . . . . . . . . . . . 14
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β ((iEdgβπ)β(πΉβπ)) = (((iEdgβπΊ) βΎ dom (iEdgβπ))β(πΉβπ))) |
28 | | wrdsymbcl 14482 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β Word dom
(iEdgβπ) β§ π β
(0..^(β―βπΉ)))
β (πΉβπ) β dom (iEdgβπ)) |
29 | 28 | fvresd 6911 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β Word dom
(iEdgβπ) β§ π β
(0..^(β―βπΉ)))
β (((iEdgβπΊ)
βΎ dom (iEdgβπ))β(πΉβπ)) = ((iEdgβπΊ)β(πΉβπ))) |
30 | 29 | 3adant1 1129 |
. . . . . . . . . . . . . 14
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β (((iEdgβπΊ) βΎ dom (iEdgβπ))β(πΉβπ)) = ((iEdgβπΊ)β(πΉβπ))) |
31 | 27, 30 | eqtrd 2771 |
. . . . . . . . . . . . 13
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β ((iEdgβπ)β(πΉβπ)) = ((iEdgβπΊ)β(πΉβπ))) |
32 | 31 | eqeq1d 2733 |
. . . . . . . . . . . 12
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β (((iEdgβπ)β(πΉβπ)) = {(πβπ)} β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)})) |
33 | 31 | sseq2d 4014 |
. . . . . . . . . . . 12
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β ({(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)) β {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) |
34 | 32, 33 | ifpbi23d 1079 |
. . . . . . . . . . 11
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
35 | 34 | biimpd 228 |
. . . . . . . . . 10
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ) β§ π β (0..^(β―βπΉ))) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
36 | 35 | 3expia 1120 |
. . . . . . . . 9
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ)) β (π β (0..^(β―βπΉ)) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
37 | 36 | ralrimiv 3144 |
. . . . . . . 8
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ)) β βπ β
(0..^(β―βπΉ))(if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
38 | | ralim 3085 |
. . . . . . . 8
β’
(βπ β
(0..^(β―βπΉ))(if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
39 | 37, 38 | syl 17 |
. . . . . . 7
β’ ((π SubGraph πΊ β§ πΉ β Word dom (iEdgβπ)) β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ))) β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
40 | 39 | expimpd 453 |
. . . . . 6
β’ (π SubGraph πΊ β ((πΉ β Word dom (iEdgβπ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))) β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
41 | 23, 40 | syl5 34 |
. . . . 5
β’ (π SubGraph πΊ β ((πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))) β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
42 | 22, 41 | jcad 512 |
. . . 4
β’ (π SubGraph πΊ β ((πΉ β Word dom (iEdgβπ) β§ π:(0...(β―βπΉ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πΉβπ)))) β ((πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
43 | 6, 42 | sylbid 239 |
. . 3
β’ (π SubGraph πΊ β (πΉ(Walksβπ)π β ((πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
44 | | df-3an 1088 |
. . 3
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
45 | 43, 44 | imbitrrdi 251 |
. 2
β’ (π SubGraph πΊ β (πΉ(Walksβπ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
46 | 8, 9 | iswlkg 29138 |
. . 3
β’ (πΊ β V β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
47 | 1, 46 | simpl2im 503 |
. 2
β’ (π SubGraph πΊ β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
48 | 45, 47 | sylibrd 259 |
1
β’ (π SubGraph πΊ β (πΉ(Walksβπ)π β πΉ(WalksβπΊ)π)) |