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 biimtrdi ⊢ 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