Theorem 2pthd

Description: A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 24-Jan-2021) (Revised by AV, 24-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	$$⊢P=⟨“ABC”⟩$$
2		2wlkd.f	$$⊢F=⟨“JK”⟩$$
3		2wlkd.s	$$⊢\phi \to \left(A\in V\wedge B\in V\wedge C\in V\right)$$
4		2wlkd.n	$$⊢\phi \to \left(A\ne B\wedge B\ne C\right)$$
5		2wlkd.e	$$⊢\phi \to \left(\left\{A,B\right\}\subseteq I\left(J\right)\wedge \left\{B,C\right\}\subseteq I\left(K\right)\right)$$
6		2wlkd.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
7		2wlkd.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
8		2trld.n	$$⊢\phi \to J\ne K$$
9		s3cli	$$⊢⟨“ABC”⟩\in \mathrm{Word}\mathrm{V}$$
10	1 9	eqeltri	$$⊢P\in \mathrm{Word}\mathrm{V}$$
11	10	a1i	$$⊢\phi \to P\in \mathrm{Word}\mathrm{V}$$
12	2	fveq2i	$$⊢\left|F\right|=\left|⟨“JK”⟩\right|$$
13		s2len	$$⊢\left|⟨“JK”⟩\right|=2$$
14	12 13	eqtri	$$⊢\left|F\right|=2$$
15		3m1e2	$$⊢3-1=2$$
16	1	fveq2i	$$⊢\left|P\right|=\left|⟨“ABC”⟩\right|$$
17		s3len	$$⊢\left|⟨“ABC”⟩\right|=3$$
18	16 17	eqtr2i	$$⊢3=\left|P\right|$$
19	18	oveq1i	$$⊢3-1=\left|P\right|-1$$
20	14 15 19	3eqtr2i	$$⊢\left|F\right|=\left|P\right|-1$$
21	1 2 3 4	2pthdlem1	$$⊢\phi \to \forall k\in \left(0..^\left|P\right|\right)\forall j\in \left(1..^\left|F\right|\right)\left(k\ne j\to P\left(k\right)\ne P\left(j\right)\right)$$
22		eqid	$$⊢\left|F\right|=\left|F\right|$$
23	1 2 3 4 5 6 7 8	2trld	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
24	11 20 21 22 23	pthd	$$⊢\phi \to F\mathrm{Paths}\left(G\right)P$$