Metamath Proof Explorer


Theorem wlkl1loop

Description: A walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021)

Ref Expression
Assertion wlkl1loop Fun iEdg G F Walks G P F = 1 P 0 = P 1 P 0 Edg G

Proof

Step Hyp Ref Expression
1 wlkv F Walks G P G V F V P V
2 simp3l G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 Fun iEdg G
3 simp2 G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 F Walks G P
4 c0ex 0 V
5 4 snid 0 0
6 oveq2 F = 1 0 ..^ F = 0 ..^ 1
7 fzo01 0 ..^ 1 = 0
8 6 7 eqtrdi F = 1 0 ..^ F = 0
9 5 8 eleqtrrid F = 1 0 0 ..^ F
10 9 ad2antrl Fun iEdg G F = 1 P 0 = P 1 0 0 ..^ F
11 10 3ad2ant3 G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 0 0 ..^ F
12 eqid iEdg G = iEdg G
13 12 iedginwlk Fun iEdg G F Walks G P 0 0 ..^ F iEdg G F 0 ran iEdg G
14 2 3 11 13 syl3anc G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 iEdg G F 0 ran iEdg G
15 eqid Vtx G = Vtx G
16 15 12 iswlkg G V F Walks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
17 8 raleqdv F = 1 k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k k 0 if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
18 oveq1 k = 0 k + 1 = 0 + 1
19 0p1e1 0 + 1 = 1
20 18 19 eqtrdi k = 0 k + 1 = 1
21 wkslem2 k = 0 k + 1 = 1 if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0
22 20 21 mpdan k = 0 if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0
23 4 22 ralsn k 0 if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0
24 17 23 bitrdi F = 1 k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0
25 24 ad2antrl Fun iEdg G F = 1 P 0 = P 1 k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0
26 ifptru P 0 = P 1 if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0 iEdg G F 0 = P 0
27 26 biimpa P 0 = P 1 if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0 iEdg G F 0 = P 0
28 27 eqcomd P 0 = P 1 if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0 P 0 = iEdg G F 0
29 28 ex P 0 = P 1 if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0 P 0 = iEdg G F 0
30 29 ad2antll Fun iEdg G F = 1 P 0 = P 1 if- P 0 = P 1 iEdg G F 0 = P 0 P 0 P 1 iEdg G F 0 P 0 = iEdg G F 0
31 25 30 sylbid Fun iEdg G F = 1 P 0 = P 1 k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k P 0 = iEdg G F 0
32 31 com12 k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k Fun iEdg G F = 1 P 0 = P 1 P 0 = iEdg G F 0
33 32 3ad2ant3 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k Fun iEdg G F = 1 P 0 = P 1 P 0 = iEdg G F 0
34 16 33 syl6bi G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 = iEdg G F 0
35 34 3imp G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 = iEdg G F 0
36 edgval Edg G = ran iEdg G
37 36 a1i G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 Edg G = ran iEdg G
38 14 35 37 3eltr4d G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 Edg G
39 38 3exp G V F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 Edg G
40 39 3ad2ant1 G V F V P V F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 Edg G
41 1 40 mpcom F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 Edg G
42 41 expd F Walks G P Fun iEdg G F = 1 P 0 = P 1 P 0 Edg G
43 42 impcom Fun iEdg G F Walks G P F = 1 P 0 = P 1 P 0 Edg G
44 43 imp Fun iEdg G F Walks G P F = 1 P 0 = P 1 P 0 Edg G