Metamath Proof Explorer

Theorem isclwwlk

Description: Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Hypotheses clwwlk.v ⊢V=Vtx⁡G
clwwlk.e ⊢E=Edg⁡G
Assertion isclwwlk ⊢W∈ClWWalks⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E

Proof

Step Hyp Ref Expression
1 clwwlk.v ⊢V=Vtx⁡G
2 clwwlk.e ⊢E=Edg⁡G
3 neeq1 ⊢w=W→w≠∅↔W≠∅
4 fveq2 ⊢w=W→w=W
5 4 oveq1d ⊢w=W→w−1=W−1
6 5 oveq2d ⊢w=W→0..^w−1=0..^W−1
7 fveq1 ⊢w=W→w⁡i=W⁡i
8 fveq1 ⊢w=W→w⁡i+1=W⁡i+1
9 7 8 preq12d ⊢w=W→w⁡iw⁡i+1=W⁡iW⁡i+1
10 9 eleq1d ⊢w=W→w⁡iw⁡i+1∈E↔W⁡iW⁡i+1∈E
11 6 10 raleqbidv ⊢w=W→∀i∈0..^w−1w⁡iw⁡i+1∈E↔∀i∈0..^W−1W⁡iW⁡i+1∈E
12 fveq2 ⊢w=W→lastS⁡w=lastS⁡W
13 fveq1 ⊢w=W→w⁡0=W⁡0
14 12 13 preq12d ⊢w=W→lastS⁡ww⁡0=lastS⁡WW⁡0
15 14 eleq1d ⊢w=W→lastS⁡ww⁡0∈E↔lastS⁡WW⁡0∈E
16 3 11 15 3anbi123d ⊢w=W→w≠∅∧∀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
17 16 elrab ⊢W∈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 1 2 clwwlk ⊢ClWWalks⁡G=w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
19 18 eleq2i ⊢W∈ClWWalks⁡G↔W∈w∈WordV|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈E∧lastS⁡ww⁡0∈E
20 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
21 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
22 3anass ⊢W≠∅∧∀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
23 22 bicomi ⊢W≠∅∧∀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
24 23 anbi2i ⊢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
25 20 21 24 3bitri ⊢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
26 17 19 25 3bitr4i ⊢W∈ClWWalks⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E