uspgr2wlkeqi

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 AV, 6-May-2021)

		Ref	Expression
	Assertion	uspgr2wlkeqi	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land 2^{nd} (A) = 2^{nd} (B)) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	$⊢ A \in Walks (G) \leftrightarrow 1^{st} (A) Walks (G) 2^{nd} (A)$
2		wlkcpr	$⊢ B \in Walks (G) \leftrightarrow 1^{st} (B) Walks (G) 2^{nd} (B)$
3		wlkcl	$⊢ 1^{st} (A) Walks (G) 2^{nd} (A) \to \|1^{st} (A)\| \in ℕ_{0}$
4		fveq2	$⊢ 2^{nd} (A) = 2^{nd} (B) \to \|2^{nd} (A)\| = \|2^{nd} (B)\|$
5	4	oveq1d	$⊢ 2^{nd} (A) = 2^{nd} (B) \to \|2^{nd} (A)\| - 1 = \|2^{nd} (B)\| - 1$
6	5	eqcomd	$⊢ 2^{nd} (A) = 2^{nd} (B) \to \|2^{nd} (B)\| - 1 = \|2^{nd} (A)\| - 1$
7	6	adantl	$⊢ ((1^{st} (A) Walks (G) 2^{nd} (A) \land 1^{st} (B) Walks (G) 2^{nd} (B)) \land 2^{nd} (A) = 2^{nd} (B)) \to \|2^{nd} (B)\| - 1 = \|2^{nd} (A)\| - 1$
8		wlklenvm1	$⊢ 1^{st} (B) Walks (G) 2^{nd} (B) \to \|1^{st} (B)\| = \|2^{nd} (B)\| - 1$
9		wlklenvm1	$⊢ 1^{st} (A) Walks (G) 2^{nd} (A) \to \|1^{st} (A)\| = \|2^{nd} (A)\| - 1$
10	8 9	eqeqan12rd	$⊢ (1^{st} (A) Walks (G) 2^{nd} (A) \land 1^{st} (B) Walks (G) 2^{nd} (B)) \to (\|1^{st} (B)\| = \|1^{st} (A)\| \leftrightarrow \|2^{nd} (B)\| - 1 = \|2^{nd} (A)\| - 1)$
11	10	adantr	$⊢ ((1^{st} (A) Walks (G) 2^{nd} (A) \land 1^{st} (B) Walks (G) 2^{nd} (B)) \land 2^{nd} (A) = 2^{nd} (B)) \to (\|1^{st} (B)\| = \|1^{st} (A)\| \leftrightarrow \|2^{nd} (B)\| - 1 = \|2^{nd} (A)\| - 1)$
12	7 11	mpbird	$⊢ ((1^{st} (A) Walks (G) 2^{nd} (A) \land 1^{st} (B) Walks (G) 2^{nd} (B)) \land 2^{nd} (A) = 2^{nd} (B)) \to \|1^{st} (B)\| = \|1^{st} (A)\|$
13	12	anim2i	$⊢ (\|1^{st} (A)\| \in ℕ_{0} \land ((1^{st} (A) Walks (G) 2^{nd} (A) \land 1^{st} (B) Walks (G) 2^{nd} (B)) \land 2^{nd} (A) = 2^{nd} (B))) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)$
14	13	exp44	$⊢ \|1^{st} (A)\| \in ℕ_{0} \to (1^{st} (A) Walks (G) 2^{nd} (A) \to (1^{st} (B) Walks (G) 2^{nd} (B) \to (2^{nd} (A) = 2^{nd} (B) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|))))$
15	3 14	mpcom	$⊢ 1^{st} (A) Walks (G) 2^{nd} (A) \to (1^{st} (B) Walks (G) 2^{nd} (B) \to (2^{nd} (A) = 2^{nd} (B) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)))$
16	2 15	biimtrid	$⊢ 1^{st} (A) Walks (G) 2^{nd} (A) \to (B \in Walks (G) \to (2^{nd} (A) = 2^{nd} (B) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)))$
17	1 16	sylbi	$⊢ A \in Walks (G) \to (B \in Walks (G) \to (2^{nd} (A) = 2^{nd} (B) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)))$
18	17	imp31	$⊢ ((A \in Walks (G) \land B \in Walks (G)) \land 2^{nd} (A) = 2^{nd} (B)) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)$
19	18	3adant1	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land 2^{nd} (A) = 2^{nd} (B)) \to (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)$
20		simpl	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \to G \in USHGraph$
21		simpl	$⊢ (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|) \to \|1^{st} (A)\| \in ℕ_{0}$
22	20 21	anim12i	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \land (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)) \to (G \in USHGraph \land \|1^{st} (A)\| \in ℕ_{0})$
23		simpl	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to A \in Walks (G)$
24	23	adantl	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \to A \in Walks (G)$
25		eqidd	$⊢ (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|) \to \|1^{st} (A)\| = \|1^{st} (A)\|$
26	24 25	anim12i	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \land (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)) \to (A \in Walks (G) \land \|1^{st} (A)\| = \|1^{st} (A)\|)$
27		simpr	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to B \in Walks (G)$
28	27	adantl	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \to B \in Walks (G)$
29		simpr	$⊢ (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|) \to \|1^{st} (B)\| = \|1^{st} (A)\|$
30	28 29	anim12i	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \land (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)) \to (B \in Walks (G) \land \|1^{st} (B)\| = \|1^{st} (A)\|)$
31		uspgr2wlkeq2	$⊢ ((G \in USHGraph \land \|1^{st} (A)\| \in ℕ_{0}) \land (A \in Walks (G) \land \|1^{st} (A)\| = \|1^{st} (A)\|) \land (B \in Walks (G) \land \|1^{st} (B)\| = \|1^{st} (A)\|)) \to (2^{nd} (A) = 2^{nd} (B) \to A = B)$
32	22 26 30 31	syl3anc	$⊢ ((G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \land (\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|)) \to (2^{nd} (A) = 2^{nd} (B) \to A = B)$
33	32	ex	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \to ((\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|) \to (2^{nd} (A) = 2^{nd} (B) \to A = B))$
34	33	com23	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G))) \to (2^{nd} (A) = 2^{nd} (B) \to ((\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|) \to A = B))$
35	34	3impia	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land 2^{nd} (A) = 2^{nd} (B)) \to ((\|1^{st} (A)\| \in ℕ_{0} \land \|1^{st} (B)\| = \|1^{st} (A)\|) \to A = B)$
36	19 35	mpd	$⊢ (G \in USHGraph \land (A \in Walks (G) \land B \in Walks (G)) \land 2^{nd} (A) = 2^{nd} (B)) \to A = B$

Metamath Proof Explorer

Theorem uspgr2wlkeqi

Proof