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	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3		eqid	⊢ ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐴 )
4		eqid	⊢ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐴 )
5	1 2 3 4	wlkelwrd	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
6		eqid	⊢ ( 1^st ‘ 𝐵 ) = ( 1^st ‘ 𝐵 )
7		eqid	⊢ ( 2^nd ‘ 𝐵 ) = ( 2^nd ‘ 𝐵 )
8	1 2 6 7	wlkelwrd	⊢ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
9	5 8	anim12i	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) )
10		wlkop	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
11		eleq1	⊢ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∈ ( Walks ‘ 𝐺 ) ) )
12		df-br	⊢ ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∈ ( Walks ‘ 𝐺 ) )
13		wlklenvm1	⊢ ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) )
14	12 13	sylbir	⊢ ( ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) )
15	11 14	syl6bi	⊢ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ) )
16	10 15	mpcom	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) )
17		wlkop	⊢ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
18		eleq1	⊢ ( 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ↔ ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ∈ ( Walks ‘ 𝐺 ) ) )
19		df-br	⊢ ( ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) ↔ ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ∈ ( Walks ‘ 𝐺 ) )
20		wlklenvm1	⊢ ( ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) )
21	19 20	sylbir	⊢ ( ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) )
22	18 21	syl6bi	⊢ ( 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) ) )
23	17 22	mpcom	⊢ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) )
24	16 23	anim12i	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) ) )
25		eqwrd	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
26	25	ad2ant2r	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
27	26	adantr	⊢ ( ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) ) ) → ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
28		lencl	⊢ ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ )
29	28	adantr	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ )
30		simpr	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) )
31		simpr	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) )
32		2ffzeq	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
33	29 30 31 32	syl2an3an	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
34	33	adantr	⊢ ( ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
35	27 34	anbi12d	⊢ ( ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) )
36	9 24 35	syl2anc	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) )
37	36	3adant3	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) )
38		eqeq1	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) )
39		oveq2	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
40	39	raleqdv	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) )
41	38 40	anbi12d	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
42		oveq2	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
43	42	raleqdv	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) )
44	38 43	anbi12d	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
45	41 44	anbi12d	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) )
46	45	bibi2d	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) ) )
47	46	3ad2ant3	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) ) )
48	37 47	mpbird	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ) )
49		1st2ndb	⊢ ( 𝐴 ∈ ( V × V ) ↔ 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
50	10 49	sylibr	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → 𝐴 ∈ ( V × V ) )
51		1st2ndb	⊢ ( 𝐵 ∈ ( V × V ) ↔ 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
52	17 51	sylibr	⊢ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → 𝐵 ∈ ( V × V ) )
53		xpopth	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ 𝐵 ∈ ( V × V ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
54	50 52 53	syl2an	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
55	54	3adant3	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
56		3anass	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ( ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
57		anandi	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ( ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
58	56 57	bitr2i	⊢ ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) )
59	58	a1i	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ) ∧ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
60	48 55 59	3bitr3d	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑥 ) ∧ ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem wlkeq

Proof