uspgr2wlkeq2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > uspgr2wlkeq2		Structured version Visualization version GIF version

Theorem uspgr2wlkeq2 29733

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.)

**Assertion**
Ref	Expression
uspgr2wlkeq2	⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → ((2^nd ‘𝐴) = (2^nd ‘𝐵) → 𝐴 = 𝐵))

Proof of Theorem uspgr2wlkeq2 Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 484	. . . . . 6 ⊢ ((𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁) → (♯‘(1^st ‘𝐵)) = 𝑁)
2	1	eqcomd 2743	. . . . 5 ⊢ ((𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁) → 𝑁 = (♯‘(1^st ‘𝐵)))
3	2	3ad2ant3 1136	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → 𝑁 = (♯‘(1^st ‘𝐵)))
4	3	adantr 480	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝑁 = (♯‘(1^st ‘𝐵)))
5		fveq1 6834	. . . . 5 ⊢ ((2^nd ‘𝐴) = (2^nd ‘𝐵) → ((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))
6	5	adantl 481	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → ((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))
7	6	ralrimivw 3134	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → ∀𝑖 ∈ (0...𝑁)((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))
8		simpl1l 1226	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝐺 ∈ USPGraph)
9		simpl 482	. . . . . . 7 ⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) → 𝐴 ∈ (Walks‘𝐺))
10		simpl 482	. . . . . . 7 ⊢ ((𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁) → 𝐵 ∈ (Walks‘𝐺))
11	9, 10	anim12i 614	. . . . . 6 ⊢ (((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)))
12	11	3adant1 1131	. . . . 5 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)))
13	12	adantr 480	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)))
14		simpr 484	. . . . . . 7 ⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) → (♯‘(1^st ‘𝐴)) = 𝑁)
15	14	eqcomd 2743	. . . . . 6 ⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) → 𝑁 = (♯‘(1^st ‘𝐴)))
16	15	3ad2ant2 1135	. . . . 5 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → 𝑁 = (♯‘(1^st ‘𝐴)))
17	16	adantr 480	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝑁 = (♯‘(1^st ‘𝐴)))
18		uspgr2wlkeq 29732	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1^st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1^st ‘𝐵)) ∧ ∀𝑖 ∈ (0...𝑁)((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))))
19	8, 13, 17, 18	syl3anc 1374	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1^st ‘𝐵)) ∧ ∀𝑖 ∈ (0...𝑁)((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))))
20	4, 7, 19	mpbir2and 714	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝐴 = 𝐵)
21	20	ex 412	1 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → ((2^nd ‘𝐴) = (2^nd ‘𝐵) → 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ‘cfv 6493 (class class class)co 7361 1^st c1st 7934 2^nd c2nd 7935 0cc0 11032 ℕ₀cn0 12431 ...cfz 13455 ♯chash 14286 USPGraphcuspgr 29234 Walkscwlks 29683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ifp 1064 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1st 7936 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-er 8637 df-map 8769 df-pm 8770 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-dju 9819 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-n0 12432 df-xnn0 12505 df-z 12519 df-uz 12783 df-fz 13456 df-fzo 13603 df-hash 14287 df-word 14470 df-edg 29134 df-uhgr 29144 df-upgr 29168 df-uspgr 29236 df-wlks 29686

This theorem is referenced by: uspgr2wlkeqi 29734

W3C validator