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 
|- V = ( Vtx ` G )
Assertion clwwlknun 
|- ( G e. USGraph -> ( N ClWWalksN G ) = U_ x e. V ( x ( ClWWalksNOn ` G ) N ) )

Proof

Step Hyp Ref Expression
1 clwwlknun.v 
 |-  V = ( Vtx ` G )
2 eliun 
 |-  ( y e. U_ x e. V ( x ( ClWWalksNOn ` G ) N ) <-> E. x e. V y e. ( x ( ClWWalksNOn ` G ) N ) )
3 isclwwlknon 
 |-  ( y e. ( x ( ClWWalksNOn ` G ) N ) <-> ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) )
4 3 rexbii 
 |-  ( E. x e. V y e. ( x ( ClWWalksNOn ` G ) N ) <-> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) )
5 simpl 
 |-  ( ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) -> y e. ( N ClWWalksN G ) )
6 5 rexlimivw 
 |-  ( E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) -> y e. ( N ClWWalksN G ) )
7 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
8 1 7 clwwlknp 
 |-  ( y e. ( N ClWWalksN G ) -> ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) )
9 8 anim2i 
 |-  ( ( G e. USGraph /\ y e. ( N ClWWalksN G ) ) -> ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) )
10 7 1 usgrpredgv 
 |-  ( ( G e. USGraph /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) -> ( ( lastS ` y ) e. V /\ ( y ` 0 ) e. V ) )
11 10 ex 
 |-  ( G e. USGraph -> ( { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) -> ( ( lastS ` y ) e. V /\ ( y ` 0 ) e. V ) ) )
12 simpr 
 |-  ( ( ( lastS ` y ) e. V /\ ( y ` 0 ) e. V ) -> ( y ` 0 ) e. V )
13 11 12 syl6com 
 |-  ( { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) -> ( G e. USGraph -> ( y ` 0 ) e. V ) )
14 13 3ad2ant3 
 |-  ( ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) -> ( G e. USGraph -> ( y ` 0 ) e. V ) )
15 14 impcom 
 |-  ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) -> ( y ` 0 ) e. V )
16 simpr 
 |-  ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> x = ( y ` 0 ) )
17 16 eqcomd 
 |-  ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> ( y ` 0 ) = x )
18 17 biantrud 
 |-  ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> ( y e. ( N ClWWalksN G ) <-> ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) )
19 18 bicomd 
 |-  ( ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) /\ x = ( y ` 0 ) ) -> ( ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) <-> y e. ( N ClWWalksN G ) ) )
20 15 19 rspcedv 
 |-  ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) -> ( y e. ( N ClWWalksN G ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) )
21 20 adantld 
 |-  ( ( G e. USGraph /\ ( ( y e. Word V /\ ( # ` y ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( y ` i ) , ( y ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` y ) , ( y ` 0 ) } e. ( Edg ` G ) ) ) -> ( ( G e. USGraph /\ y e. ( N ClWWalksN G ) ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) )
22 9 21 mpcom 
 |-  ( ( G e. USGraph /\ y e. ( N ClWWalksN G ) ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) )
23 22 ex 
 |-  ( G e. USGraph -> ( y e. ( N ClWWalksN G ) -> E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) ) )
24 6 23 impbid2 
 |-  ( G e. USGraph -> ( E. x e. V ( y e. ( N ClWWalksN G ) /\ ( y ` 0 ) = x ) <-> y e. ( N ClWWalksN G ) ) )
25 4 24 bitrid 
 |-  ( G e. USGraph -> ( E. x e. V y e. ( x ( ClWWalksNOn ` G ) N ) <-> y e. ( N ClWWalksN G ) ) )
26 2 25 bitr2id 
 |-  ( G e. USGraph -> ( y e. ( N ClWWalksN G ) <-> y e. U_ x e. V ( x ( ClWWalksNOn ` G ) N ) ) )
27 26 eqrdv 
 |-  ( G e. USGraph -> ( N ClWWalksN G ) = U_ x e. V ( x ( ClWWalksNOn ` G ) N ) )