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∧FWalks⁡GP∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G

Proof

Step Hyp Ref Expression
1 wlkv ⊢FWalks⁡GP→G∈V∧F∈V∧P∈V
2 simp3l ⊢G∈V∧FWalks⁡GP∧Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→Fun⁡iEdg⁡G
3 simp2 ⊢G∈V∧FWalks⁡GP∧Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→FWalks⁡GP
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∧FWalks⁡GP∧Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→0∈0..^F
12 eqid ⊢iEdg⁡G=iEdg⁡G
13 12 iedginwlk ⊢Fun⁡iEdg⁡G∧FWalks⁡GP∧0∈0..^F→iEdg⁡G⁡F⁡0∈ran⁡iEdg⁡G
14 2 3 11 13 syl3anc ⊢G∈V∧FWalks⁡GP∧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→FWalks⁡GP↔F∈Worddom⁡iEdg⁡G∧P:0…F⟶Vtx⁡G∧∀k∈0..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k
17 8 raleqdv ⊢F=1→∀k∈0..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔∀k∈0if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡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+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0
22 20 21 mpdan ⊢k=0→if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0
23 4 22 ralsn ⊢∀k∈0if-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0
24 17 23 bitrdi ⊢F=1→∀k∈0..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0
25 24 ad2antrl ⊢Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→∀k∈0..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k↔if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0
26 ifptru ⊢P⁡0=P⁡1→if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0↔iEdg⁡G⁡F⁡0=P⁡0
27 26 biimpa ⊢P⁡0=P⁡1∧if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0→iEdg⁡G⁡F⁡0=P⁡0
28 27 eqcomd ⊢P⁡0=P⁡1∧if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡1⊆iEdg⁡G⁡F⁡0→P⁡0=iEdg⁡G⁡F⁡0
29 28 ex ⊢P⁡0=P⁡1→if-P⁡0=P⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡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⁡1iEdg⁡G⁡F⁡0=P⁡0P⁡0P⁡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..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡F⁡k→P⁡0=iEdg⁡G⁡F⁡0
32 31 com12 ⊢∀k∈0..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡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∈Worddom⁡iEdg⁡G∧P:0…F⟶Vtx⁡G∧∀k∈0..^Fif-P⁡k=P⁡k+1iEdg⁡G⁡F⁡k=P⁡kP⁡kP⁡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→FWalks⁡GP→Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→P⁡0=iEdg⁡G⁡F⁡0
35 34 3imp ⊢G∈V∧FWalks⁡GP∧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∧FWalks⁡GP∧Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→Edg⁡G=ran⁡iEdg⁡G
38 14 35 37 3eltr4d ⊢G∈V∧FWalks⁡GP∧Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
39 38 3exp ⊢G∈V→FWalks⁡GP→Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
40 39 3ad2ant1 ⊢G∈V∧F∈V∧P∈V→FWalks⁡GP→Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
41 1 40 mpcom ⊢FWalks⁡GP→Fun⁡iEdg⁡G∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
42 41 expd ⊢FWalks⁡GP→Fun⁡iEdg⁡G→F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
43 42 impcom ⊢Fun⁡iEdg⁡G∧FWalks⁡GP→F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
44 43 imp ⊢Fun⁡iEdg⁡G∧FWalks⁡GP∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G