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

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) )
2		wlkcpr	⊢ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) )
3		wlkcl	⊢ ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ )
4		fveq2	⊢ ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) = ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) )
5	4	oveq1d	⊢ ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) )
6	5	eqcomd	⊢ ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) )
7	6	adantl	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) ∧ ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) )
8		wlklenvm1	⊢ ( ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) )
9		wlklenvm1	⊢ ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) )
10	8 9	eqeqan12rd	⊢ ( ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) ∧ ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ) )
11	10	adantr	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) ∧ ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ ( 2^nd ‘ 𝐵 ) ) − 1 ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐴 ) ) − 1 ) ) )
12	7 11	mpbird	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) ∧ ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) )
13	12	anim2i	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) ∧ ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
14	13	exp44	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ → ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) → ( ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) ) ) )
15	3 14	mpcom	⊢ ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) → ( ( 1^st ‘ 𝐵 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐵 ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) ) )
16	2 15	biimtrid	⊢ ( ( 1^st ‘ 𝐴 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐴 ) → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) ) )
17	1 16	sylbi	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) ) )
18	17	imp31	⊢ ( ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
19	18	3adant1	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
20		simpl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) → 𝐺 ∈ USPGraph )
21		simpl	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ )
22	20 21	anim12i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) → ( 𝐺 ∈ USPGraph ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ) )
23		simpl	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → 𝐴 ∈ ( Walks ‘ 𝐺 ) )
24	23	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) → 𝐴 ∈ ( Walks ‘ 𝐺 ) )
25		eqidd	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) )
26	24 25	anim12i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
27		simpr	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → 𝐵 ∈ ( Walks ‘ 𝐺 ) )
28	27	adantl	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) → 𝐵 ∈ ( Walks ‘ 𝐺 ) )
29		simpr	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) )
30	28 29	anim12i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
31		uspgr2wlkeq2	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ) ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
32	22 26 30 31	syl3anc	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → 𝐴 = 𝐵 ) )
33	32	ex	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → 𝐴 = 𝐵 ) ) )
34	33	com23	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ) → ( ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → 𝐴 = 𝐵 ) ) )
35	34	3impia	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∈ ℕ₀ ∧ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → 𝐴 = 𝐵 ) )
36	19 35	mpd	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) → 𝐴 = 𝐵 )

Metamath Proof Explorer

Theorem uspgr2wlkeqi

Proof