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 syl5bb
 |-  ( 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 ) )