uspgr2wlkeq2

Description: Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 14-Apr-2021)

		Ref	Expression
	Assertion	uspgr2wlkeq2	$⊢ ((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \to (2^{nd} (A) = 2^{nd} (B) \to A = B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (B \in Walks (G) \land \|1^{st} (B)\| = N) \to \|1^{st} (B)\| = N$
2	1	eqcomd	$⊢ (B \in Walks (G) \land \|1^{st} (B)\| = N) \to N = \|1^{st} (B)\|$
3	2	3ad2ant3	$⊢ ((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \to N = \|1^{st} (B)\|$
4	3	adantr	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to N = \|1^{st} (B)\|$
5		fveq1	$⊢ 2^{nd} (A) = 2^{nd} (B) \to 2^{nd} (A) (i) = 2^{nd} (B) (i)$
6	5	adantl	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to 2^{nd} (A) (i) = 2^{nd} (B) (i)$
7	6	ralrimivw	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to \forall i \in (0 \dots N) 2^{nd} (A) (i) = 2^{nd} (B) (i)$
8		simpl1l	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to G \in USHGraph$
9		simpl	$⊢ (A \in Walks (G) \land \|1^{st} (A)\| = N) \to A \in Walks (G)$
10		simpl	$⊢ (B \in Walks (G) \land \|1^{st} (B)\| = N) \to B \in Walks (G)$
11	9 10	anim12i	$⊢ ((A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \to (A \in Walks (G) \land B \in Walks (G))$
12	11	3adant1	$⊢ ((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \to (A \in Walks (G) \land B \in Walks (G))$
13	12	adantr	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to (A \in Walks (G) \land B \in Walks (G))$
14		simpr	$⊢ (A \in Walks (G) \land \|1^{st} (A)\| = N) \to \|1^{st} (A)\| = N$
15	14	eqcomd	$⊢ (A \in Walks (G) \land \|1^{st} (A)\| = N) \to N = \|1^{st} (A)\|$
16	15	3ad2ant2	$⊢ ((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \to N = \|1^{st} (A)\|$
17	16	adantr	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to N = \|1^{st} (A)\|$
18		uspgr2wlkeq	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall i \in (0 \dots N) 2^{nd} (A) (i) = 2^{nd} (B) (i)))$
19	8 13 17 18	syl3anc	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall i \in (0 \dots N) 2^{nd} (A) (i) = 2^{nd} (B) (i)))$
20	4 7 19	mpbir2and	$⊢ (((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \land 2^{nd} (A) = 2^{nd} (B)) \to A = B$
21	20	ex	$⊢ ((G \in USHGraph \land N \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = N) \land (B \in Walks (G) \land \|1^{st} (B)\| = N)) \to (2^{nd} (A) = 2^{nd} (B) \to A = B)$

Metamath Proof Explorer

Theorem uspgr2wlkeq2

Proof