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 26777

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 473	. . . . . 6 ⊢ ((𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁) → (♯‘(1^st ‘𝐵)) = 𝑁)
2	1	eqcomd 2819	. . . . 5 ⊢ ((𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁) → 𝑁 = (♯‘(1^st ‘𝐵)))
3	2	3ad2ant3 1158	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → 𝑁 = (♯‘(1^st ‘𝐵)))
4	3	adantr 468	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝑁 = (♯‘(1^st ‘𝐵)))
5		fveq1 6410	. . . . 5 ⊢ ((2^nd ‘𝐴) = (2^nd ‘𝐵) → ((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))
6	5	adantl 469	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → ((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))
7	6	ralrimivw 3162	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → ∀𝑖 ∈ (0...𝑁)((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))
8		simpl1l 1286	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝐺 ∈ USPGraph)
9		simpl 470	. . . . . . 7 ⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) → 𝐴 ∈ (Walks‘𝐺))
10		simpl 470	. . . . . . 7 ⊢ ((𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁) → 𝐵 ∈ (Walks‘𝐺))
11	9, 10	anim12i 602	. . . . . 6 ⊢ (((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)))
12	11	3adant1 1153	. . . . 5 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)))
13	12	adantr 468	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)))
14		simpr 473	. . . . . . 7 ⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) → (♯‘(1^st ‘𝐴)) = 𝑁)
15	14	eqcomd 2819	. . . . . 6 ⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) → 𝑁 = (♯‘(1^st ‘𝐴)))
16	15	3ad2ant2 1157	. . . . 5 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → 𝑁 = (♯‘(1^st ‘𝐴)))
17	16	adantr 468	. . . 4 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝑁 = (♯‘(1^st ‘𝐴)))
18		uspgr2wlkeq 26776	. . . 4 ⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1^st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1^st ‘𝐵)) ∧ ∀𝑖 ∈ (0...𝑁)((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))))
19	8, 13, 17, 18	syl3anc 1483	. . 3 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1^st ‘𝐵)) ∧ ∀𝑖 ∈ (0...𝑁)((2^nd ‘𝐴)‘𝑖) = ((2^nd ‘𝐵)‘𝑖))))
20	4, 7, 19	mpbir2and 695	. 2 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) → 𝐴 = 𝐵)
21	20	ex 399	1 ⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ₀) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1^st ‘𝐵)) = 𝑁)) → ((2^nd ‘𝐴) = (2^nd ‘𝐵) → 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1100 = wceq 1637 ∈ wcel 2157 ∀wral 3103 ‘cfv 6104 (class class class)co 6877 1^st c1st 7399 2^nd c2nd 7400 0cc0 10224 ℕ₀cn0 11562 ...cfz 12552 ♯chash 13340 USPGraphcuspgr 26264 Walkscwlks 26726

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2069 ax-7 2105 ax-8 2159 ax-9 2166 ax-10 2186 ax-11 2202 ax-12 2215 ax-13 2422 ax-ext 2791 ax-rep 4971 ax-sep 4982 ax-nul 4990 ax-pow 5042 ax-pr 5103 ax-un 7182 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-ifp 1079 df-3or 1101 df-3an 1102 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2062 df-mo 2635 df-eu 2638 df-clab 2800 df-cleq 2806 df-clel 2809 df-nfc 2944 df-ne 2986 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3400 df-sbc 3641 df-csb 3736 df-dif 3779 df-un 3781 df-in 3783 df-ss 3790 df-pss 3792 df-nul 4124 df-if 4287 df-pw 4360 df-sn 4378 df-pr 4380 df-tp 4382 df-op 4384 df-uni 4638 df-int 4677 df-iun 4721 df-br 4852 df-opab 4914 df-mpt 4931 df-tr 4954 df-id 5226 df-eprel 5231 df-po 5239 df-so 5240 df-fr 5277 df-we 5279 df-xp 5324 df-rel 5325 df-cnv 5326 df-co 5327 df-dm 5328 df-rn 5329 df-res 5330 df-ima 5331 df-pred 5900 df-ord 5946 df-on 5947 df-lim 5948 df-suc 5949 df-iota 6067 df-fun 6106 df-fn 6107 df-f 6108 df-f1 6109 df-fo 6110 df-f1o 6111 df-fv 6112 df-riota 6838 df-ov 6880 df-oprab 6881 df-mpt2 6882 df-om 7299 df-1st 7401 df-2nd 7402 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-1o 7799 df-2o 7800 df-oadd 7803 df-er 7982 df-map 8097 df-pm 8098 df-en 8196 df-dom 8197 df-sdom 8198 df-fin 8199 df-card 9051 df-cda 9278 df-pnf 10364 df-mnf 10365 df-xr 10366 df-ltxr 10367 df-le 10368 df-sub 10556 df-neg 10557 df-nn 11309 df-2 11367 df-n0 11563 df-xnn0 11633 df-z 11647 df-uz 11908 df-fz 12553 df-fzo 12693 df-hash 13341 df-word 13513 df-edg 26160 df-uhgr 26173 df-upgr 26197 df-uspgr 26266 df-wlks 26729

This theorem is referenced by: uspgr2wlkeqi 26778 wlknwwlksninjOLD 27022 wlkwwlkinjOLD 27030

W3C validator