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 eqtrid 
 |-  ( -. 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 ) }