Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  usg2wlkeq Structured version   Unicode version

Theorem usg2wlkeq 25419
 Description: Conditions for two walks within the same undirected simple graph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.)
Assertion
Ref Expression
usg2wlkeq USGrph Walks Walks
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem usg2wlkeq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 3anan32 994 . . 3 ..^ ..^
21a1i 11 . 2 USGrph Walks Walks ..^ ..^
3 2wlkeq 25418 . . . 4 Walks Walks ..^
433expa 1205 . . 3 Walks Walks ..^
543adant1 1023 . 2 USGrph Walks Walks ..^
6 fzofzp1 12007 . . . . . . . . . . . 12 ..^
76adantl 467 . . . . . . . . . . 11 USGrph Walks Walks ..^
8 fveq2 5877 . . . . . . . . . . . . 13
9 fveq2 5877 . . . . . . . . . . . . 13
108, 9eqeq12d 2444 . . . . . . . . . . . 12
1110adantl 467 . . . . . . . . . . 11 USGrph Walks Walks ..^
127, 11rspcdv 3185 . . . . . . . . . 10 USGrph Walks Walks ..^
1312impancom 441 . . . . . . . . 9 USGrph Walks Walks ..^
1413ralrimiv 2837 . . . . . . . 8 USGrph Walks Walks ..^
15 oveq1 6308 . . . . . . . . . . 11
1615fveq2d 5881 . . . . . . . . . 10
1715fveq2d 5881 . . . . . . . . . 10
1816, 17eqeq12d 2444 . . . . . . . . 9
1918cbvralv 3055 . . . . . . . 8 ..^ ..^
2014, 19sylibr 215 . . . . . . 7 USGrph Walks Walks ..^
21 fzossfz 11938 . . . . . . . . . 10 ..^
22 ssralv 3525 . . . . . . . . . 10 ..^ ..^
2321, 22mp1i 13 . . . . . . . . 9 USGrph Walks Walks ..^
24 r19.26 2955 . . . . . . . . . . 11 ..^ ..^ ..^
25 preq12 4078 . . . . . . . . . . . . 13
2625a1i 11 . . . . . . . . . . . 12 USGrph Walks Walks
2726ralimdv 2835 . . . . . . . . . . 11 USGrph Walks Walks ..^ ..^
2824, 27syl5bir 221 . . . . . . . . . 10 USGrph Walks Walks ..^ ..^ ..^
2928expd 437 . . . . . . . . 9 USGrph Walks Walks ..^ ..^ ..^
3023, 29syld 45 . . . . . . . 8 USGrph Walks Walks ..^ ..^
3130imp 430 . . . . . . 7 USGrph Walks Walks ..^ ..^
3220, 31mpd 15 . . . . . 6 USGrph Walks Walks ..^
3332ex 435 . . . . 5 USGrph Walks Walks ..^
34 eqid 2422 . . . . . . . . . 10
35 eqid 2422 . . . . . . . . . 10
3634, 35wlkcompim 25237 . . . . . . . . 9 Walks Word ..^
37 eqid 2422 . . . . . . . . . 10
38 eqid 2422 . . . . . . . . . 10
3937, 38wlkcompim 25237 . . . . . . . . 9 Walks Word ..^
40 oveq2 6309 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
4140eqcoms 2434 . . . . . . . . . . . . . . . . . 18 ..^ ..^
4241raleqdv 3031 . . . . . . . . . . . . . . . . 17 ..^ ..^
43 oveq2 6309 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
4443eqcoms 2434 . . . . . . . . . . . . . . . . . 18 ..^ ..^
4544raleqdv 3031 . . . . . . . . . . . . . . . . 17 ..^ ..^
4642, 45bi2anan9r 882 . . . . . . . . . . . . . . . 16 ..^ ..^ ..^ ..^
47 r19.26 2955 . . . . . . . . . . . . . . . . 17 ..^ ..^ ..^
48 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . 21
49 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . . . 23
5049eqcoms 2434 . . . . . . . . . . . . . . . . . . . . . 22
5150biimpd 210 . . . . . . . . . . . . . . . . . . . . 21
5248, 51syl6bi 231 . . . . . . . . . . . . . . . . . . . 20
5352com13 83 . . . . . . . . . . . . . . . . . . 19
5453imp 430 . . . . . . . . . . . . . . . . . 18
5554ral2imi 2813 . . . . . . . . . . . . . . . . 17 ..^ ..^ ..^
5647, 55sylbir 216 . . . . . . . . . . . . . . . 16 ..^ ..^ ..^ ..^
5746, 56syl6bi 231 . . . . . . . . . . . . . . 15 ..^ ..^ ..^ ..^
5857com12 32 . . . . . . . . . . . . . 14 ..^ ..^ ..^ ..^
5958ex 435 . . . . . . . . . . . . 13 ..^ ..^ ..^ ..^
60593ad2ant3 1028 . . . . . . . . . . . 12 Word ..^ ..^ ..^ ..^
6160com12 32 . . . . . . . . . . 11 ..^ Word ..^ ..^ ..^
62613ad2ant3 1028 . . . . . . . . . 10 Word ..^ Word ..^ ..^ ..^
6362imp 430 . . . . . . . . 9 Word ..^ Word ..^ ..^ ..^
6436, 39, 63syl2an 479 . . . . . . . 8 Walks Walks ..^ ..^
6564expd 437 . . . . . . 7 Walks Walks ..^ ..^
6665a1i 11 . . . . . 6 USGrph Walks Walks ..^ ..^
67663imp1 1218 . . . . 5 USGrph Walks Walks ..^ ..^
68 eqcom 2431 . . . . . . 7
69 usgraf1 25071 . . . . . . . . . . 11 USGrph
70693ad2ant1 1026 . . . . . . . . . 10 USGrph Walks Walks
7170adantr 466 . . . . . . . . 9 USGrph Walks Walks
7271adantr 466 . . . . . . . 8 USGrph Walks Walks ..^
73 wlkelwrd 25241 . . . . . . . . . . . . . . 15 Walks Word
74 wlkelwrd 25241 . . . . . . . . . . . . . . 15 Walks Word
75 oveq2 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
7675eleq2d 2492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
77 wrdsymbcl 12674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word ..^
7877expcom 436 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Word
7976, 78syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ Word
8079adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Word
8180imp 430 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
8281com12 32 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^
8382adantl 467 . . . . . . . . . . . . . . . . . . . . 21 Word Word ..^
84 oveq2 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
8584eleq2d 2492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
86 wrdsymbcl 12674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word ..^
8786expcom 436 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ Word
8885, 87syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ Word
8988adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ Word
9089imp 430 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ Word
9190com12 32 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^
9291adantr 466 . . . . . . . . . . . . . . . . . . . . 21 Word Word ..^
9383, 92jcad 535 . . . . . . . . . . . . . . . . . . . 20 Word Word ..^
9493ex 435 . . . . . . . . . . . . . . . . . . 19 Word Word ..^
9594adantr 466 . . . . . . . . . . . . . . . . . 18 Word Word ..^
9695com12 32 . . . . . . . . . . . . . . . . 17 Word Word ..^
9796adantr 466 . . . . . . . . . . . . . . . 16 Word Word ..^
9897imp 430 . . . . . . . . . . . . . . 15 Word Word ..^
9973, 74, 98syl2an 479 . . . . . . . . . . . . . 14 Walks Walks ..^
10099expd 437 . . . . . . . . . . . . 13 Walks Walks ..^
101100expd 437 . . . . . . . . . . . 12 Walks Walks ..^
102101imp 430 . . . . . . . . . . 11 Walks Walks ..^
1031023adant1 1023 . . . . . . . . . 10 USGrph Walks Walks ..^
104103imp 430 . . . . . . . . 9 USGrph Walks Walks ..^
105104imp 430 . . . . . . . 8 USGrph Walks Walks ..^
106 f1veqaeq 6172 . . . . . . . 8
10772, 105, 106syl2anc 665 . . . . . . 7 USGrph Walks Walks ..^
10868, 107syl5bi 220 . . . . . 6 USGrph Walks Walks ..^
109108ralimdva 2833 . . . . 5 USGrph Walks Walks ..^ ..^
11033, 67, 1093syld 57 . . . 4 USGrph Walks Walks ..^
111110expimpd 606 . . 3 USGrph Walks Walks ..^
112111pm4.71d 638 . 2 USGrph Walks Walks ..^
1132, 5, 1123bitr4d 288 1 USGrph Walks Walks
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1868  wral 2775   wss 3436  cpr 3998   class class class wbr 4420   cdm 4849   crn 4850  wf 5593  wf1 5594  cfv 5597  (class class class)co 6301  c1st 6801  c2nd 6802  cc0 9539  c1 9540   caddc 9542  cfz 11784  ..^cfzo 11915  chash 12514  Word cword 12646   USGrph cusg 25041   Walks cwalk 25209 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11785  df-fzo 11916  df-hash 12515  df-word 12654  df-usgra 25044  df-wlk 25219 This theorem is referenced by:  usg2wlkeq2  25420  clwlkf1clwwlk  25561
 Copyright terms: Public domain W3C validator