Metamath Proof Explorer

Theorem clwlkcomp

Description: A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 17-Feb-2021)

		Ref	Expression
	Hypotheses	isclwlke.v	$⊢ V = Vtx (G)$
		isclwlke.i	$⊢ I = iEdg (G)$
		clwlkcomp.1	$⊢ F = 1^{st} (W)$
		clwlkcomp.2	$⊢ P = 2^{nd} (W)$
	Assertion	clwlkcomp	$⊢ (G \in X \land W \in (S \times T)) \to (W \in ClWalks (G) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \land P (0) = P (\|F\|))))$

Proof

Step	Hyp	Ref	Expression
1		isclwlke.v	$⊢ V = Vtx (G)$
2		isclwlke.i	$⊢ I = iEdg (G)$
3		clwlkcomp.1	$⊢ F = 1^{st} (W)$
4		clwlkcomp.2	$⊢ P = 2^{nd} (W)$
5	3	eqcomi	$⊢ 1^{st} (W) = F$
6	4	eqcomi	$⊢ 2^{nd} (W) = P$
7	5 6	pm3.2i	$⊢ (1^{st} (W) = F \land 2^{nd} (W) = P)$
8		eqop	$⊢ W \in (S \times T) \to (W = ⟨F, P⟩ \leftrightarrow (1^{st} (W) = F \land 2^{nd} (W) = P))$
9	7 8	mpbiri	$⊢ W \in (S \times T) \to W = ⟨F, P⟩$
10	9	eleq1d	$⊢ W \in (S \times T) \to (W \in ClWalks (G) \leftrightarrow ⟨F, P⟩ \in ClWalks (G))$
11		df-br	$⊢ F ClWalks (G) P \leftrightarrow ⟨F, P⟩ \in ClWalks (G)$
12	10 11	bitr4di	$⊢ W \in (S \times T) \to (W \in ClWalks (G) \leftrightarrow F ClWalks (G) P)$
13	1 2	isclwlke	$⊢ G \in X \to (F ClWalks (G) P \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \land P (0) = P (\|F\|))))$
14	12 13	sylan9bbr	$⊢ (G \in X \land W \in (S \times T)) \to (W \in ClWalks (G) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \land P (0) = P (\|F\|))))$