Metamath Proof Explorer

Theorem clwwlknscsh

Description: The set of cyclical shifts of a word representing a closed walk is the set of closed walks represented by cyclical shifts of a word. (Contributed by Alexander van der Vekens, 15-Jun-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Assertion clwwlknscsh ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑊 cyclShift 𝑛 ) ↔ 𝑥 = ( 𝑊 cyclShift 𝑛 ) ) )
2 1 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑊 cyclShift 𝑛 ) ) )
3 2 cbvrabv ⊢ { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } = { 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑊 cyclShift 𝑛 ) }
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 4 clwwlknwrd ⊢ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
6 5 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) → 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) )
7 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
8 6 7 jca ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
9 simprr ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) → 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
10 simpllr ⊢ ( ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) ∧ 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) → 𝑛 ∈ ( 0 ... 𝑁 ) )
11 clwwnisshclwwsn ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊 cyclShift 𝑛 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
12 9 10 11 syl2an2r ⊢ ( ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) ∧ 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) → ( 𝑊 cyclShift 𝑛 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
13 eleq1 ⊢ ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 cyclShift 𝑛 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
14 13 adantl ⊢ ( ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) ∧ 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) → ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 cyclShift 𝑛 ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
15 12 14 mpbird ⊢ ( ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) ∧ 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
16 15 exp31 ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) )
17 16 com23 ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) )
18 17 rexlimdva ⊢ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ) )
19 18 imp ⊢ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
20 19 impcom ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) → 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
21 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
22 20 21 jca ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) → ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
23 8 22 impbida ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) ) )
24 eqeq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = ( 𝑊 cyclShift 𝑛 ) ↔ 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
25 24 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑊 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
26 25 elrab ⊢ ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑊 cyclShift 𝑛 ) } ↔ ( 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
27 eqeq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 = ( 𝑊 cyclShift 𝑛 ) ↔ 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
28 27 rexbidv ⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
29 28 elrab ⊢ ( 𝑤 ∈ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
30 23 26 29 3bitr4g ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑤 ∈ { 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑊 cyclShift 𝑛 ) } ↔ 𝑤 ∈ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } ) )
31 30 eqrdv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑊 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } )
32 3 31 syl5eq ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑊 cyclShift 𝑛 ) } )