Metamath Proof Explorer

Theorem clwlkcompbp

Description: Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022)

		Ref	Expression
	Hypotheses	clwlkcompbp.1	$⊢ F = 1^{st} (W)$
		clwlkcompbp.2	$⊢ P = 2^{nd} (W)$
	Assertion	clwlkcompbp	$⊢ W \in ClWalks (G) \to (F Walks (G) P \land P (0) = P (\|F\|))$

Proof

Step	Hyp	Ref	Expression
1		clwlkcompbp.1	$⊢ F = 1^{st} (W)$
2		clwlkcompbp.2	$⊢ P = 2^{nd} (W)$
3		clwlkwlk	$⊢ W \in ClWalks (G) \to W \in Walks (G)$
4		wlkop	$⊢ W \in Walks (G) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$
5	3 4	syl	$⊢ W \in ClWalks (G) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$
6		eleq1	$⊢ W = ⟨1^{st} (W), 2^{nd} (W)⟩ \to (W \in ClWalks (G) \leftrightarrow ⟨1^{st} (W), 2^{nd} (W)⟩ \in ClWalks (G))$
7		df-br	$⊢ 1^{st} (W) ClWalks (G) 2^{nd} (W) \leftrightarrow ⟨1^{st} (W), 2^{nd} (W)⟩ \in ClWalks (G)$
8	6 7	bitr4di	$⊢ W = ⟨1^{st} (W), 2^{nd} (W)⟩ \to (W \in ClWalks (G) \leftrightarrow 1^{st} (W) ClWalks (G) 2^{nd} (W))$
9		isclwlk	$⊢ 1^{st} (W) ClWalks (G) 2^{nd} (W) \leftrightarrow (1^{st} (W) Walks (G) 2^{nd} (W) \land 2^{nd} (W) (0) = 2^{nd} (W) (\|1^{st} (W)\|))$
10	1 2	breq12i	$⊢ F Walks (G) P \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$
11	2	fveq1i	$⊢ P (0) = 2^{nd} (W) (0)$
12	1	fveq2i	$⊢ \|F\| = \|1^{st} (W)\|$
13	2 12	fveq12i	$⊢ P (\|F\|) = 2^{nd} (W) (\|1^{st} (W)\|)$
14	11 13	eqeq12i	$⊢ P (0) = P (\|F\|) \leftrightarrow 2^{nd} (W) (0) = 2^{nd} (W) (\|1^{st} (W)\|)$
15	10 14	anbi12i	$⊢ (F Walks (G) P \land P (0) = P (\|F\|)) \leftrightarrow (1^{st} (W) Walks (G) 2^{nd} (W) \land 2^{nd} (W) (0) = 2^{nd} (W) (\|1^{st} (W)\|))$
16	9 15	sylbb2	$⊢ 1^{st} (W) ClWalks (G) 2^{nd} (W) \to (F Walks (G) P \land P (0) = P (\|F\|))$
17	8 16	biimtrdi	$⊢ W = ⟨1^{st} (W), 2^{nd} (W)⟩ \to (W \in ClWalks (G) \to (F Walks (G) P \land P (0) = P (\|F\|)))$
18	5 17	mpcom	$⊢ W \in ClWalks (G) \to (F Walks (G) P \land P (0) = P (\|F\|))$