Metamath Proof Explorer

Theorem clwwlknun

Description: The set of closed walks of fixed length N in a simple graph G is the union of the closed walks of the fixed length N on each of the vertices of graph G . (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 28-May-2021) (Revised by AV, 3-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Hypothesis clwwlknun.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clwwlknun ( 𝐺 ∈ USGraph → ( 𝑁 ClWWalksN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Proof

Step Hyp Ref Expression
1 clwwlknun.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ∃ 𝑥 ∈ 𝑉 𝑦 ∈ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
3 isclwwlknon ⊢ ( 𝑦 ∈ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) )
4 3 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑉 𝑦 ∈ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) )
5 simpl ⊢ ( ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) → 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
6 5 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) → 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
7 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
8 1 7 clwwlknp ⊢ ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
9 8 anim2i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
10 7 1 usgrpredgv ⊢ ( ( 𝐺 ∈ USGraph ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( lastS ‘ 𝑦 ) ∈ 𝑉 ∧ ( 𝑦 ‘ 0 ) ∈ 𝑉 ) )
11 10 ex ⊢ ( 𝐺 ∈ USGraph → ( { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( lastS ‘ 𝑦 ) ∈ 𝑉 ∧ ( 𝑦 ‘ 0 ) ∈ 𝑉 ) ) )
12 simpr ⊢ ( ( ( lastS ‘ 𝑦 ) ∈ 𝑉 ∧ ( 𝑦 ‘ 0 ) ∈ 𝑉 ) → ( 𝑦 ‘ 0 ) ∈ 𝑉 )
13 11 12 syl6com ⊢ ( { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝐺 ∈ USGraph → ( 𝑦 ‘ 0 ) ∈ 𝑉 ) )
14 13 3ad2ant3 ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐺 ∈ USGraph → ( 𝑦 ‘ 0 ) ∈ 𝑉 ) )
15 14 impcom ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑦 ‘ 0 ) ∈ 𝑉 )
16 simpr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑥 = ( 𝑦 ‘ 0 ) ) → 𝑥 = ( 𝑦 ‘ 0 ) )
17 16 eqcomd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑥 = ( 𝑦 ‘ 0 ) ) → ( 𝑦 ‘ 0 ) = 𝑥 )
18 17 biantrud ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑥 = ( 𝑦 ‘ 0 ) ) → ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) ) )
19 18 bicomd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑥 = ( 𝑦 ‘ 0 ) ) → ( ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) ↔ 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
20 15 19 rspcedv ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) ) )
21 20 adantld ⊢ ( ( 𝐺 ∈ USGraph ∧ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑦 ) , ( 𝑦 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) ) )
22 9 21 mpcom ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) )
23 22 ex ⊢ ( 𝐺 ∈ USGraph → ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) ) )
24 6 23 impbid2 ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ 𝑉 ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑥 ) ↔ 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
25 4 24 syl5bb ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ 𝑉 𝑦 ∈ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) )
26 2 25 syl5rbb ⊢ ( 𝐺 ∈ USGraph → ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
27 26 eqrdv ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ClWWalksN 𝐺 ) = ∪ 𝑥 ∈ 𝑉 ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )