wlkeq

Description: Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018) (Revised by AV, 16-May-2019) (Revised by AV, 14-Apr-2021)

		Ref	Expression
	Assertion	wlkeq	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3		eqid	$⊢ 1^{st} (A) = 1^{st} (A)$
4		eqid	$⊢ 2^{nd} (A) = 2^{nd} (A)$
5	1 2 3 4	wlkelwrd	$⊢ A \in Walks (G) \to (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G))$
6		eqid	$⊢ 1^{st} (B) = 1^{st} (B)$
7		eqid	$⊢ 2^{nd} (B) = 2^{nd} (B)$
8	1 2 6 7	wlkelwrd	$⊢ B \in Walks (G) \to (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))$
9	5 8	anim12i	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to ((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)))$
10		wlkop	$⊢ A \in Walks (G) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
11		eleq1	$⊢ A = ⟨1^{st} (A), 2^{nd} (A)⟩ \to (A \in Walks (G) \leftrightarrow ⟨1^{st} (A), 2^{nd} (A)⟩ \in Walks (G))$
12		df-br	$⊢ 1^{st} (A) Walks (G) 2^{nd} (A) \leftrightarrow ⟨1^{st} (A), 2^{nd} (A)⟩ \in Walks (G)$
13		wlklenvm1	$⊢ 1^{st} (A) Walks (G) 2^{nd} (A) \to \|1^{st} (A)\| = \|2^{nd} (A)\| - 1$
14	12 13	sylbir	$⊢ ⟨1^{st} (A), 2^{nd} (A)⟩ \in Walks (G) \to \|1^{st} (A)\| = \|2^{nd} (A)\| - 1$
15	11 14	syl6bi	$⊢ A = ⟨1^{st} (A), 2^{nd} (A)⟩ \to (A \in Walks (G) \to \|1^{st} (A)\| = \|2^{nd} (A)\| - 1)$
16	10 15	mpcom	$⊢ A \in Walks (G) \to \|1^{st} (A)\| = \|2^{nd} (A)\| - 1$
17		wlkop	$⊢ B \in Walks (G) \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
18		eleq1	$⊢ B = ⟨1^{st} (B), 2^{nd} (B)⟩ \to (B \in Walks (G) \leftrightarrow ⟨1^{st} (B), 2^{nd} (B)⟩ \in Walks (G))$
19		df-br	$⊢ 1^{st} (B) Walks (G) 2^{nd} (B) \leftrightarrow ⟨1^{st} (B), 2^{nd} (B)⟩ \in Walks (G)$
20		wlklenvm1	$⊢ 1^{st} (B) Walks (G) 2^{nd} (B) \to \|1^{st} (B)\| = \|2^{nd} (B)\| - 1$
21	19 20	sylbir	$⊢ ⟨1^{st} (B), 2^{nd} (B)⟩ \in Walks (G) \to \|1^{st} (B)\| = \|2^{nd} (B)\| - 1$
22	18 21	syl6bi	$⊢ B = ⟨1^{st} (B), 2^{nd} (B)⟩ \to (B \in Walks (G) \to \|1^{st} (B)\| = \|2^{nd} (B)\| - 1)$
23	17 22	mpcom	$⊢ B \in Walks (G) \to \|1^{st} (B)\| = \|2^{nd} (B)\| - 1$
24	16 23	anim12i	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to (\|1^{st} (A)\| = \|2^{nd} (A)\| - 1 \land \|1^{st} (B)\| = \|2^{nd} (B)\| - 1)$
25		eqwrd	$⊢ (1^{st} (A) \in Word dom iEdg (G) \land 1^{st} (B) \in Word dom iEdg (G)) \to (1^{st} (A) = 1^{st} (B) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)))$
26	25	ad2ant2r	$⊢ ((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))) \to (1^{st} (A) = 1^{st} (B) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)))$
27	26	adantr	$⊢ (((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))) \land (\|1^{st} (A)\| = \|2^{nd} (A)\| - 1 \land \|1^{st} (B)\| = \|2^{nd} (B)\| - 1)) \to (1^{st} (A) = 1^{st} (B) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)))$
28		lencl	$⊢ 1^{st} (A) \in Word dom iEdg (G) \to \|1^{st} (A)\| \in ℕ_{0}$
29	28	adantr	$⊢ (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \to \|1^{st} (A)\| \in ℕ_{0}$
30		simpr	$⊢ (1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \to 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)$
31		simpr	$⊢ (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)) \to 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)$
32		2ffzeq	$⊢ (\|1^{st} (A)\| \in ℕ_{0} \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G)) \to (2^{nd} (A) = 2^{nd} (B) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
33	29 30 31 32	syl2an3an	$⊢ ((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))) \to (2^{nd} (A) = 2^{nd} (B) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
34	33	adantr	$⊢ (((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))) \land (\|1^{st} (A)\| = \|2^{nd} (A)\| - 1 \land \|1^{st} (B)\| = \|2^{nd} (B)\| - 1)) \to (2^{nd} (A) = 2^{nd} (B) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
35	27 34	anbi12d	$⊢ (((1^{st} (A) \in Word dom iEdg (G) \land 2^{nd} (A) : (0 \dots \|1^{st} (A)\|) ⟶ Vtx (G)) \land (1^{st} (B) \in Word dom iEdg (G) \land 2^{nd} (B) : (0 \dots \|1^{st} (B)\|) ⟶ Vtx (G))) \land (\|1^{st} (A)\| = \|2^{nd} (A)\| - 1 \land \|1^{st} (B)\| = \|2^{nd} (B)\| - 1)) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x))))$
36	9 24 35	syl2anc	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x))))$
37	36	3adant3	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x))))$
38		eqeq1	$⊢ N = \|1^{st} (A)\| \to (N = \|1^{st} (B)\| \leftrightarrow \|1^{st} (A)\| = \|1^{st} (B)\|)$
39		oveq2	$⊢ N = \|1^{st} (A)\| \to (0 ..^N) = (0 ..^\|1^{st} (A)\|)$
40	39	raleqdv	$⊢ N = \|1^{st} (A)\| \to (\forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \leftrightarrow \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x))$
41	38 40	anbi12d	$⊢ N = \|1^{st} (A)\| \to ((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)))$
42		oveq2	$⊢ N = \|1^{st} (A)\| \to (0 \dots N) = (0 \dots \|1^{st} (A)\|)$
43	42	raleqdv	$⊢ N = \|1^{st} (A)\| \to (\forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x) \leftrightarrow \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x))$
44	38 43	anbi12d	$⊢ N = \|1^{st} (A)\| \to ((N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)) \leftrightarrow (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
45	41 44	anbi12d	$⊢ N = \|1^{st} (A)\| \to (((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x))) \leftrightarrow ((\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x))))$
46	45	bibi2d	$⊢ N = \|1^{st} (A)\| \to (((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))) \leftrightarrow ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x)))))$
47	46	3ad2ant3	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to (((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))) \leftrightarrow ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 ..^\|1^{st} (A)\|) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (\|1^{st} (A)\| = \|1^{st} (B)\| \land \forall x \in (0 \dots \|1^{st} (A)\|) 2^{nd} (A) (x) = 2^{nd} (B) (x)))))$
48	37 47	mpbird	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x))))$
49		1st2ndb	$⊢ A \in (V \times V) \leftrightarrow A = ⟨1^{st} (A), 2^{nd} (A)⟩$
50	10 49	sylibr	$⊢ A \in Walks (G) \to A \in (V \times V)$
51		1st2ndb	$⊢ B \in (V \times V) \leftrightarrow B = ⟨1^{st} (B), 2^{nd} (B)⟩$
52	17 51	sylibr	$⊢ B \in Walks (G) \to B \in (V \times V)$
53		xpopth	$⊢ (A \in (V \times V) \land B \in (V \times V)) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow A = B)$
54	50 52 53	syl2an	$⊢ (A \in Walks (G) \land B \in Walks (G)) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow A = B)$
55	54	3adant3	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to ((1^{st} (A) = 1^{st} (B) \land 2^{nd} (A) = 2^{nd} (B)) \leftrightarrow A = B)$
56		3anass	$⊢ (N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)) \leftrightarrow (N = \|1^{st} (B)\| \land (\forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
57		anandi	$⊢ (N = \|1^{st} (B)\| \land (\forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x))) \leftrightarrow ((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
58	56 57	bitr2i	$⊢ ((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x))) \leftrightarrow (N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x))$
59	58	a1i	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to (((N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x)) \land (N = \|1^{st} (B)\| \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x))) \leftrightarrow (N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$
60	48 55 59	3bitr3d	$⊢ (A \in Walks (G) \land B \in Walks (G) \land N = \|1^{st} (A)\|) \to (A = B \leftrightarrow (N = \|1^{st} (B)\| \land \forall x \in (0 ..^N) 1^{st} (A) (x) = 1^{st} (B) (x) \land \forall x \in (0 \dots N) 2^{nd} (A) (x) = 2^{nd} (B) (x)))$

Metamath Proof Explorer

Theorem wlkeq

Proof