Metamath Proof Explorer

Theorem clwwlkn2

Description: A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Assertion clwwlkn2 ⊢W∈2ClWWalksNG↔W=2∧W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G

Proof

Step Hyp Ref Expression
1 2nn ⊢2∈ℕ
2 eqid ⊢Vtx⁡G=Vtx⁡G
3 eqid ⊢Edg⁡G=Edg⁡G
4 2 3 isclwwlknx ⊢2∈ℕ→W∈2ClWWalksNG↔W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=2
5 1 4 ax-mp ⊢W∈2ClWWalksNG↔W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=2
6 3anass ⊢W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G↔W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
7 oveq1 ⊢W=2→W−1=2−1
8 2m1e1 ⊢2−1=1
9 7 8 eqtrdi ⊢W=2→W−1=1
10 9 oveq2d ⊢W=2→0..^W−1=0..^1
11 fzo01 ⊢0..^1=0
12 10 11 eqtrdi ⊢W=2→0..^W−1=0
13 12 adantr ⊢W=2∧W∈WordVtx⁡G→0..^W−1=0
14 13 raleqdv ⊢W=2∧W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G↔∀i∈0W⁡iW⁡i+1∈Edg⁡G
15 c0ex ⊢0∈V
16 fveq2 ⊢i=0→W⁡i=W⁡0
17 fv0p1e1 ⊢i=0→W⁡i+1=W⁡1
18 16 17 preq12d ⊢i=0→W⁡iW⁡i+1=W⁡0W⁡1
19 18 eleq1d ⊢i=0→W⁡iW⁡i+1∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G
20 15 19 ralsn ⊢∀i∈0W⁡iW⁡i+1∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G
21 14 20 bitrdi ⊢W=2∧W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G
22 prcom ⊢lastS⁡WW⁡0=W⁡0lastS⁡W
23 lsw ⊢W∈WordVtx⁡G→lastS⁡W=W⁡W−1
24 9 fveq2d ⊢W=2→W⁡W−1=W⁡1
25 23 24 sylan9eqr ⊢W=2∧W∈WordVtx⁡G→lastS⁡W=W⁡1
26 25 preq2d ⊢W=2∧W∈WordVtx⁡G→W⁡0lastS⁡W=W⁡0W⁡1
27 22 26 eqtrid ⊢W=2∧W∈WordVtx⁡G→lastS⁡WW⁡0=W⁡0W⁡1
28 27 eleq1d ⊢W=2∧W∈WordVtx⁡G→lastS⁡WW⁡0∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G
29 21 28 anbi12d ⊢W=2∧W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G∧W⁡0W⁡1∈Edg⁡G
30 anidm ⊢W⁡0W⁡1∈Edg⁡G∧W⁡0W⁡1∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G
31 29 30 bitrdi ⊢W=2∧W∈WordVtx⁡G→∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G↔W⁡0W⁡1∈Edg⁡G
32 31 pm5.32da ⊢W=2→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G↔W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G
33 6 32 bitrid ⊢W=2→W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G↔W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G
34 33 pm5.32ri ⊢W∈WordVtx⁡G∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G∧W=2↔W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G∧W=2
35 3anass ⊢W=2∧W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G↔W=2∧W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G
36 ancom ⊢W=2∧W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G↔W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G∧W=2
37 35 36 bitr2i ⊢W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G∧W=2↔W=2∧W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G
38 5 34 37 3bitri ⊢W∈2ClWWalksNG↔W=2∧W∈WordVtx⁡G∧W⁡0W⁡1∈Edg⁡G