Metamath Proof Explorer

Theorem clwwlk1loop

Description: A closed walk of length 1 is a loop. See also clwlkl1loop . (Contributed by AV, 24-Apr-2021)

Ref Expression
Assertion clwwlk1loop ⊢W∈ClWWalks⁡G∧W=1→W⁡0W⁡0∈Edg⁡G

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢Edg⁡G=Edg⁡G
3 1 2 isclwwlk ⊢W∈ClWWalks⁡G↔W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
4 lsw1 ⊢W∈WordVtx⁡G∧W=1→lastS⁡W=W⁡0
5 4 preq1d ⊢W∈WordVtx⁡G∧W=1→lastS⁡WW⁡0=W⁡0W⁡0
6 5 eleq1d ⊢W∈WordVtx⁡G∧W=1→lastS⁡WW⁡0∈Edg⁡G↔W⁡0W⁡0∈Edg⁡G
7 6 biimpd ⊢W∈WordVtx⁡G∧W=1→lastS⁡WW⁡0∈Edg⁡G→W⁡0W⁡0∈Edg⁡G
8 7 ex ⊢W∈WordVtx⁡G→W=1→lastS⁡WW⁡0∈Edg⁡G→W⁡0W⁡0∈Edg⁡G
9 8 com23 ⊢W∈WordVtx⁡G→lastS⁡WW⁡0∈Edg⁡G→W=1→W⁡0W⁡0∈Edg⁡G
10 9 adantr ⊢W∈WordVtx⁡G∧W≠∅→lastS⁡WW⁡0∈Edg⁡G→W=1→W⁡0W⁡0∈Edg⁡G
11 10 imp ⊢W∈WordVtx⁡G∧W≠∅∧lastS⁡WW⁡0∈Edg⁡G→W=1→W⁡0W⁡0∈Edg⁡G
12 11 3adant2 ⊢W∈WordVtx⁡G∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G→W=1→W⁡0W⁡0∈Edg⁡G
13 3 12 sylbi ⊢W∈ClWWalks⁡G→W=1→W⁡0W⁡0∈Edg⁡G
14 13 imp ⊢W∈ClWWalks⁡G∧W=1→W⁡0W⁡0∈Edg⁡G