Metamath Proof Explorer


Theorem clwwlk

Description: The set of closed walks (in an undirected graph) as words over the set of vertices. (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 clwwlk
|- ( ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) }

Proof

Step Hyp Ref Expression
1 clwwlk.v
 |-  V = ( Vtx ` G )
2 clwwlk.e
 |-  E = ( Edg ` G )
3 df-clwwlk
 |-  ClWWalks = ( g e. _V |-> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. ( Edg ` g ) ) } )
4 fveq2
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
5 4 1 eqtr4di
 |-  ( g = G -> ( Vtx ` g ) = V )
6 wrdeq
 |-  ( ( Vtx ` g ) = V -> Word ( Vtx ` g ) = Word V )
7 5 6 syl
 |-  ( g = G -> Word ( Vtx ` g ) = Word V )
8 fveq2
 |-  ( g = G -> ( Edg ` g ) = ( Edg ` G ) )
9 8 2 eqtr4di
 |-  ( g = G -> ( Edg ` g ) = E )
10 9 eleq2d
 |-  ( g = G -> ( { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) <-> { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
11 10 ralbidv
 |-  ( g = G -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) <-> A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) )
12 9 eleq2d
 |-  ( g = G -> ( { ( lastS ` w ) , ( w ` 0 ) } e. ( Edg ` g ) <-> { ( lastS ` w ) , ( w ` 0 ) } e. E ) )
13 11 12 3anbi23d
 |-  ( g = G -> ( ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. ( Edg ` g ) ) <-> ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) ) )
14 7 13 rabeqbidv
 |-  ( g = G -> { w e. Word ( Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` g ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. ( Edg ` g ) ) } = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } )
15 id
 |-  ( G e. _V -> G e. _V )
16 1 fvexi
 |-  V e. _V
17 16 a1i
 |-  ( G e. _V -> V e. _V )
18 wrdexg
 |-  ( V e. _V -> Word V e. _V )
19 rabexg
 |-  ( Word V e. _V -> { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } e. _V )
20 17 18 19 3syl
 |-  ( G e. _V -> { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } e. _V )
21 3 14 15 20 fvmptd3
 |-  ( G e. _V -> ( ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } )
22 fvprc
 |-  ( -. G e. _V -> ( ClWWalks ` G ) = (/) )
23 noel
 |-  -. { ( lastS ` w ) , ( w ` 0 ) } e. (/)
24 fvprc
 |-  ( -. G e. _V -> ( Edg ` G ) = (/) )
25 2 24 syl5eq
 |-  ( -. G e. _V -> E = (/) )
26 25 eleq2d
 |-  ( -. G e. _V -> ( { ( lastS ` w ) , ( w ` 0 ) } e. E <-> { ( lastS ` w ) , ( w ` 0 ) } e. (/) ) )
27 23 26 mtbiri
 |-  ( -. G e. _V -> -. { ( lastS ` w ) , ( w ` 0 ) } e. E )
28 27 adantr
 |-  ( ( -. G e. _V /\ w e. Word V ) -> -. { ( lastS ` w ) , ( w ` 0 ) } e. E )
29 28 intn3an3d
 |-  ( ( -. G e. _V /\ w e. Word V ) -> -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) )
30 29 ralrimiva
 |-  ( -. G e. _V -> A. w e. Word V -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) )
31 rabeq0
 |-  ( { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } = (/) <-> A. w e. Word V -. ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) )
32 30 31 sylibr
 |-  ( -. G e. _V -> { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } = (/) )
33 22 32 eqtr4d
 |-  ( -. G e. _V -> ( ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) } )
34 21 33 pm2.61i
 |-  ( ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { ( lastS ` w ) , ( w ` 0 ) } e. E ) }