Theorem 3pthd

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

	Ref	Expression
Hypotheses	3wlkd.p	$$⊢P=⟨“ABCD”⟩$$
	3wlkd.f	$$⊢F=⟨“JKL”⟩$$
	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	3pthd	$$⊢\phi \to F\mathrm{Paths}\left(G\right)P$$

Proof

Step	Hyp	Ref	Expression
1		3wlkd.p	$$⊢P=⟨“ABCD”⟩$$
2		3wlkd.f	$$⊢F=⟨“JKL”⟩$$
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		s4cli	$$⊢⟨“ABCD”⟩\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|⟨“JKL”⟩\right|$$
13		s3len	$$⊢\left|⟨“JKL”⟩\right|=3$$
14	12 13	eqtri	$$⊢\left|F\right|=3$$
15		4m1e3	$$⊢4-1=3$$
16	1	fveq2i	$$⊢\left|P\right|=\left|⟨“ABCD”⟩\right|$$
17		s4len	$$⊢\left|⟨“ABCD”⟩\right|=4$$
18	16 17	eqtr2i	$$⊢4=\left|P\right|$$
19	18	oveq1i	$$⊢4-1=\left|P\right|-1$$
20	14 15 19	3eqtr2i	$$⊢\left|F\right|=\left|P\right|-1$$
21	1 2 3 4	3pthdlem1	$$⊢\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	3trld	$$⊢\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$$