| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > wlkf | Structured version Visualization version GIF version | ||
| Description: The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.) |
| Ref | Expression |
|---|---|
| wlkf.i | ⊢ 𝐼 = (iEdg‘𝐺) |
| Ref | Expression |
|---|---|
| wlkf | ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2761 | . . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
| 2 | wlkf.i | . . 3 ⊢ 𝐼 = (iEdg‘𝐺) | |
| 3 | 1, 2 | wlkprop 29927 | . 2 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
| 4 | 3 | simp1d 1158 | 1 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 if-wif 1076 = wceq 1568 ∈ wcel 2141 ∀wral 3077 ⊆ wss 3904 {csn 4588 {cpr 4590 class class class wbr 5108 dom cdm 5661 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 0cc0 11099 1c1 11100 + caddc 11102 ...cfz 13534 ..^cfzo 13682 ♯chash 14366 Word cword 14550 Vtxcvtx 29312 iEdgciedg 29313 Walkscwlks 29912 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-ifp 1077 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13683 df-hash 14367 df-word 14551 df-wlks 29915 |
| This theorem is referenced by: wlkcl 29931 iedginwlk 29952 wlk1ewlk 29955 wlkv0 29965 wlkonwlk1l 29977 wlkres 29984 redwlk 29986 wlkp1lem2 29988 wlkp1lem3 29989 wlkp1lem4 29990 wlkp1lem6 29992 wlkp1lem8 29994 wlkp1 29995 lfgriswlk 30002 trlf1 30012 trlreslem 30013 upgr2pthnlp 30047 uhgrwkspthlem1 30068 usgr2wlkspthlem1 30072 crctcshlem2 30133 crctcshlem4 30135 crctcshwlkn0 30136 eupth2eucrct 30534 eucrctshift 30560 eucrct2eupth 30562 pfxwlk 35582 revwlk 35583 swrdwlk 35585 upgrimwlklem5 48633 upgrimwlk 48634 upgrimwlklen 48635 upgrimtrlslem1 48636 upgrimtrlslem2 48637 upgrimtrls 48638 upgrimpths 48641 upgrimcycls 48643 |
| Copyright terms: Public domain | W3C validator |