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	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 )
2	1	eqcomd	⊢ ( ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) → 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) )
3	2	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) → 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) )
4	3	adantr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) )
5		fveq1	⊢ ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( 2^nd ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑖 ) )
6	5	adantl	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ( 2^nd ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑖 ) )
7	6	ralrimivw	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑖 ) )
8		simpl1l	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → 𝐺 ∈ USPGraph )
9		simpl	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) → 𝐴 ∈ ( Walks ‘ 𝐺 ) )
10		simpl	⊢ ( ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) → 𝐵 ∈ ( Walks ‘ 𝐺 ) )
11	9 10	anim12i	⊢ ( ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) )
12	11	3adant1	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) )
13	12	adantr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) )
14		simpr	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 )
15	14	eqcomd	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) → 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) )
16	15	3ad2ant2	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) → 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) )
17	16	adantr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) )
18		uspgr2wlkeq	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑖 ) ) ) )
19	8 13 17 18	syl3anc	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑖 ) ) ) )
20	4 7 19	mpbir2and	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → 𝐴 = 𝐵 )
21	20	ex	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → 𝐴 = 𝐵 ) )

Metamath Proof Explorer

Theorem uspgr2wlkeq2

Proof