Metamath Proof Explorer

Theorem numclwwlk3lem2

Description: Lemma 1 for numclwwlk3 : The number of closed vertices of a fixed length N on a fixed vertex V is the sum of the number of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 1-Jun-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk3lem2.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
numclwwlk3lem2.h 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
Assertion numclwwlk3lem2 
|- ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( ( # ` ( X H N ) ) + ( # ` ( X C N ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk3lem2.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
2 numclwwlk3lem2.h 
 |-  H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
3 1 2 numclwwlk3lem2lem 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X ( ClWWalksNOn ` G ) N ) = ( ( X H N ) u. ( X C N ) ) )
4 3 adantll 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X ( ClWWalksNOn ` G ) N ) = ( ( X H N ) u. ( X C N ) ) )
5 4 fveq2d 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( # ` ( ( X H N ) u. ( X C N ) ) ) )
6 2 numclwwlkovh0 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )
7 6 adantll 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } )
8 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
9 8 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> ( Vtx ` G ) e. Fin )
10 9 ad2antrr 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( Vtx ` G ) e. Fin )
11 8 clwwlknonfin 
 |-  ( ( Vtx ` G ) e. Fin -> ( X ( ClWWalksNOn ` G ) N ) e. Fin )
12 rabfi 
 |-  ( ( X ( ClWWalksNOn ` G ) N ) e. Fin -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } e. Fin )
13 10 11 12 3syl 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } e. Fin )
14 7 13 eqeltrd 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) e. Fin )
15 1 2clwwlk 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
16 15 adantll 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
17 rabfi 
 |-  ( ( X ( ClWWalksNOn ` G ) N ) e. Fin -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. Fin )
18 10 11 17 3syl 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. Fin )
19 16 18 eqeltrd 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X C N ) e. Fin )
20 7 16 ineq12d 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( X H N ) i^i ( X C N ) ) = ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } i^i { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
21 inrab 
 |-  ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } i^i { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X ) }
22 exmid 
 |-  ( ( w ` ( N - 2 ) ) = X \/ -. ( w ` ( N - 2 ) ) = X )
23 ianor 
 |-  ( -. ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X ) <-> ( -. ( w ` ( N - 2 ) ) =/= X \/ -. ( w ` ( N - 2 ) ) = X ) )
24 nne 
 |-  ( -. ( w ` ( N - 2 ) ) =/= X <-> ( w ` ( N - 2 ) ) = X )
25 24 orbi1i 
 |-  ( ( -. ( w ` ( N - 2 ) ) =/= X \/ -. ( w ` ( N - 2 ) ) = X ) <-> ( ( w ` ( N - 2 ) ) = X \/ -. ( w ` ( N - 2 ) ) = X ) )
26 23 25 bitri 
 |-  ( -. ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( w ` ( N - 2 ) ) = X \/ -. ( w ` ( N - 2 ) ) = X ) )
27 22 26 mpbir 
 |-  -. ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X )
28 27 rgenw 
 |-  A. w e. ( X ( ClWWalksNOn ` G ) N ) -. ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X )
29 rabeq0 
 |-  ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X ) } = (/) <-> A. w e. ( X ( ClWWalksNOn ` G ) N ) -. ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X ) )
30 28 29 mpbir 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( ( w ` ( N - 2 ) ) =/= X /\ ( w ` ( N - 2 ) ) = X ) } = (/)
31 21 30 eqtri 
 |-  ( { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) =/= X } i^i { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) = (/)
32 20 31 eqtrdi 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( X H N ) i^i ( X C N ) ) = (/) )
33 hashun 
 |-  ( ( ( X H N ) e. Fin /\ ( X C N ) e. Fin /\ ( ( X H N ) i^i ( X C N ) ) = (/) ) -> ( # ` ( ( X H N ) u. ( X C N ) ) ) = ( ( # ` ( X H N ) ) + ( # ` ( X C N ) ) ) )
34 14 19 32 33 syl3anc 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( ( X H N ) u. ( X C N ) ) ) = ( ( # ` ( X H N ) ) + ( # ` ( X C N ) ) ) )
35 5 34 eqtrd 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( ( # ` ( X H N ) ) + ( # ` ( X C N ) ) ) )