Metamath Proof Explorer

Theorem upgrclwlkcompim

Description: Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 2-May-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	upgrclwlkcompim	$⊢ (G \in UPGraph \land W \in ClWalks (G)) \to ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \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	1 2 3 4	clwlkcompim	$⊢ W \in ClWalks (G) \to ((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\|)))$
6	5	adantl	$⊢ (G \in UPGraph \land W \in ClWalks (G)) \to ((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\|)))$
7		simprl	$⊢ ((G \in UPGraph \land W \in ClWalks (G)) \land ((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\|)))) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V)$
8		clwlkwlk	$⊢ W \in ClWalks (G) \to W \in Walks (G)$
9	1 2 3 4	upgrwlkcompim	$⊢ (G \in UPGraph \land W \in Walks (G)) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
10	9	simp3d	$⊢ (G \in UPGraph \land W \in Walks (G)) \to \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}$
11	8 10	sylan2	$⊢ (G \in UPGraph \land W \in ClWalks (G)) \to \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}$
12	11	adantr	$⊢ ((G \in UPGraph \land W \in ClWalks (G)) \land ((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\|)))) \to \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}$
13		simprrr	$⊢ ((G \in UPGraph \land W \in ClWalks (G)) \land ((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\|)))) \to P (0) = P (\|F\|)$
14	7 12 13	3jca	$⊢ ((G \in UPGraph \land W \in ClWalks (G)) \land ((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\|)))) \to ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \land P (0) = P (\|F\|))$
15	6 14	mpdan	$⊢ (G \in UPGraph \land W \in ClWalks (G)) \to ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \land P (0) = P (\|F\|))$