Metamath Proof Explorer

Theorem isclwwlknx

Description: Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v ⊢V=Vtx⁡G
isclwwlknx.e ⊢E=Edg⁡G
Assertion isclwwlknx ⊢N∈ℕ→W∈NClWWalksNG↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N

Proof

Step Hyp Ref Expression
1 isclwwlknx.v ⊢V=Vtx⁡G
2 isclwwlknx.e ⊢E=Edg⁡G
3 eleq1 ⊢W=N→W∈ℕ↔N∈ℕ
4 len0nnbi ⊢W∈WordV→W≠∅↔W∈ℕ
5 4 biimprcd ⊢W∈ℕ→W∈WordV→W≠∅
6 3 5 syl6bir ⊢W=N→N∈ℕ→W∈WordV→W≠∅
7 6 impcom ⊢N∈ℕ∧W=N→W∈WordV→W≠∅
8 7 imp ⊢N∈ℕ∧W=N∧W∈WordV→W≠∅
9 8 biantrurd ⊢N∈ℕ∧W=N∧W∈WordV→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
10 9 bicomd ⊢N∈ℕ∧W=N∧W∈WordV→W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
11 10 pm5.32da ⊢N∈ℕ∧W=N→W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
12 11 ex ⊢N∈ℕ→W=N→W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
13 12 pm5.32rd ⊢N∈ℕ→W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N
14 isclwwlkn ⊢W∈NClWWalksNG↔W∈ClWWalks⁡G∧W=N
15 1 2 isclwwlk ⊢W∈ClWWalks⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
16 3anass ⊢W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
17 anass ⊢W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
18 16 17 bitri ⊢W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
19 15 18 bitri ⊢W∈ClWWalks⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
20 19 anbi1i ⊢W∈ClWWalks⁡G∧W=N↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N
21 14 20 bitri ⊢W∈NClWWalksNG↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N
22 3anass ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E
23 22 anbi1i ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N
24 13 21 23 3bitr4g ⊢N∈ℕ→W∈NClWWalksNG↔W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N