# Metamath Proof Explorer

## Theorem 3trld

Description: Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017) (Revised by AV, 8-Feb-2021) (Revised by AV, 24-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypotheses 3wlkd.p ${⊢}{P}=⟨“{A}{B}{C}{D}”⟩$
3wlkd.f ${⊢}{F}=⟨“{J}{K}{L}”⟩$
3wlkd.s ${⊢}{\phi }\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)$
3wlkd.n ${⊢}{\phi }\to \left(\left({A}\ne {B}\wedge {A}\ne {C}\right)\wedge \left({B}\ne {C}\wedge {B}\ne {D}\right)\wedge {C}\ne {D}\right)$
3wlkd.e ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\subseteq {I}\left({J}\right)\wedge \left\{{B},{C}\right\}\subseteq {I}\left({K}\right)\wedge \left\{{C},{D}\right\}\subseteq {I}\left({L}\right)\right)$
3wlkd.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
3wlkd.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3trld.n ${⊢}{\phi }\to \left({J}\ne {K}\wedge {J}\ne {L}\wedge {K}\ne {L}\right)$
Assertion 3trld ${⊢}{\phi }\to {F}\mathrm{Trails}\left({G}\right){P}$

### Proof

Step Hyp Ref Expression
1 3wlkd.p ${⊢}{P}=⟨“{A}{B}{C}{D}”⟩$
2 3wlkd.f ${⊢}{F}=⟨“{J}{K}{L}”⟩$
3 3wlkd.s ${⊢}{\phi }\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)$
4 3wlkd.n ${⊢}{\phi }\to \left(\left({A}\ne {B}\wedge {A}\ne {C}\right)\wedge \left({B}\ne {C}\wedge {B}\ne {D}\right)\wedge {C}\ne {D}\right)$
5 3wlkd.e ${⊢}{\phi }\to \left(\left\{{A},{B}\right\}\subseteq {I}\left({J}\right)\wedge \left\{{B},{C}\right\}\subseteq {I}\left({K}\right)\wedge \left\{{C},{D}\right\}\subseteq {I}\left({L}\right)\right)$
6 3wlkd.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
7 3wlkd.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
8 3trld.n ${⊢}{\phi }\to \left({J}\ne {K}\wedge {J}\ne {L}\wedge {K}\ne {L}\right)$
9 1 2 3 4 5 6 7 3wlkd ${⊢}{\phi }\to {F}\mathrm{Walks}\left({G}\right){P}$
10 1 2 3 4 5 3wlkdlem7 ${⊢}{\phi }\to \left({J}\in \mathrm{V}\wedge {K}\in \mathrm{V}\wedge {L}\in \mathrm{V}\right)$
11 funcnvs3 ${⊢}\left(\left({J}\in \mathrm{V}\wedge {K}\in \mathrm{V}\wedge {L}\in \mathrm{V}\right)\wedge \left({J}\ne {K}\wedge {J}\ne {L}\wedge {K}\ne {L}\right)\right)\to \mathrm{Fun}{⟨“{J}{K}{L}”⟩}^{-1}$
12 10 8 11 syl2anc ${⊢}{\phi }\to \mathrm{Fun}{⟨“{J}{K}{L}”⟩}^{-1}$
13 2 cnveqi ${⊢}{{F}}^{-1}={⟨“{J}{K}{L}”⟩}^{-1}$
14 13 funeqi ${⊢}\mathrm{Fun}{{F}}^{-1}↔\mathrm{Fun}{⟨“{J}{K}{L}”⟩}^{-1}$
15 12 14 sylibr ${⊢}{\phi }\to \mathrm{Fun}{{F}}^{-1}$
16 istrl ${⊢}{F}\mathrm{Trails}\left({G}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
17 9 15 16 sylanbrc ${⊢}{\phi }\to {F}\mathrm{Trails}\left({G}\right){P}$