Metamath Proof Explorer

Theorem numclwlk1lem2

Description: Lemma 2 for numclwlk1 (Statement 9 in Huneke p. 2 for n>2). This theorem corresponds to numclwwlk1 , using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022)

Ref Expression
Hypotheses numclwlk1.v 
|- V = ( Vtx ` G )
numclwlk1.c 
|- C = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
numclwlk1.f 
|- F = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) }
Assertion numclwlk1lem2 
|- ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )

Proof

Step Hyp Ref Expression
1 numclwlk1.v 
 |-  V = ( Vtx ` G )
2 numclwlk1.c 
 |-  C = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
3 numclwlk1.f 
 |-  F = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) }
4 rusgrusgr 
 |-  ( G RegUSGraph K -> G e. USGraph )
5 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
6 4 5 syl 
 |-  ( G RegUSGraph K -> G e. USPGraph )
7 6 ad2antlr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G e. USPGraph )
8 simpl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> X e. V )
9 8 adantl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
10 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
11 10 ad2antll 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> N e. ( ZZ>= ` 2 ) )
12 eqid 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X }
13 1 2 12 dlwwlknondlwlknonen 
 |-  ( ( G e. USPGraph /\ X e. V /\ N e. ( ZZ>= ` 2 ) ) -> C ~~ { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
14 7 9 11 13 syl3anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> C ~~ { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
15 4 anim2i 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( V e. Fin /\ G e. USGraph ) )
16 15 ancomd 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( G e. USGraph /\ V e. Fin ) )
17 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
18 16 17 sylibr 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> G e. FinUSGraph )
19 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
20 19 nnnn0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN0 )
21 20 adantl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> N e. NN0 )
22 wlksnfi 
 |-  ( ( G e. FinUSGraph /\ N e. NN0 ) -> { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = N } e. Fin )
23 18 21 22 syl2an 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = N } e. Fin )
24 clwlkswks 
 |-  ( ClWalks ` G ) C_ ( Walks ` G )
25 24 a1i 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ClWalks ` G ) C_ ( Walks ` G ) )
26 simp21 
 |-  ( ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) /\ w e. ( ClWalks ` G ) ) -> ( # ` ( 1st ` w ) ) = N )
27 25 26 rabssrabd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) } C_ { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = N } )
28 23 27 ssfid 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) } e. Fin )
29 2 28 eqeltrid 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> C e. Fin )
30 1 clwwlknonfin 
 |-  ( V e. Fin -> ( X ( ClWWalksNOn ` G ) N ) e. Fin )
31 30 ad2antrr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X ( ClWWalksNOn ` G ) N ) e. Fin )
32 ssrab2 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } C_ ( X ( ClWWalksNOn ` G ) N )
33 32 a1i 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } C_ ( X ( ClWWalksNOn ` G ) N ) )
34 31 33 ssfid 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. Fin )
35 hashen 
 |-  ( ( C e. Fin /\ { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. Fin ) -> ( ( # ` C ) = ( # ` { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) <-> C ~~ { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
36 29 34 35 syl2anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` C ) = ( # ` { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) <-> C ~~ { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
37 14 36 mpbird 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` C ) = ( # ` { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
38 eqidd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) )
39 oveq12 
 |-  ( ( v = X /\ n = N ) -> ( v ( ClWWalksNOn ` G ) n ) = ( X ( ClWWalksNOn ` G ) N ) )
40 fvoveq1 
 |-  ( n = N -> ( w ` ( n - 2 ) ) = ( w ` ( N - 2 ) ) )
41 40 adantl 
 |-  ( ( v = X /\ n = N ) -> ( w ` ( n - 2 ) ) = ( w ` ( N - 2 ) ) )
42 simpl 
 |-  ( ( v = X /\ n = N ) -> v = X )
43 41 42 eqeq12d 
 |-  ( ( v = X /\ n = N ) -> ( ( w ` ( n - 2 ) ) = v <-> ( w ` ( N - 2 ) ) = X ) )
44 39 43 rabeqbidv 
 |-  ( ( v = X /\ n = N ) -> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
45 44 adantl 
 |-  ( ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ ( v = X /\ n = N ) ) -> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
46 ovex 
 |-  ( X ( ClWWalksNOn ` G ) N ) e. _V
47 46 rabex 
 |-  { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. _V
48 47 a1i 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } e. _V )
49 38 45 9 11 48 ovmpod 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) = { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } )
50 49 fveq2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) = ( # ` { w e. ( X ( ClWWalksNOn ` G ) N ) | ( w ` ( N - 2 ) ) = X } ) )
51 eqid 
 |-  ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
52 eqid 
 |-  ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
53 1 51 52 numclwwlk1 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) = ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )
54 8 1 eleqtrdi 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> X e. ( Vtx ` G ) )
55 54 adantl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. ( Vtx ` G ) )
56 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
57 56 ad2antll 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) e. NN )
58 clwwlknonclwlknonen 
 |-  ( ( G e. USPGraph /\ X e. ( Vtx ` G ) /\ ( N - 2 ) e. NN ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
59 7 55 57 58 syl3anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
60 3 59 eqbrtrid 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> F ~~ ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
61 uznn0sub 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
62 10 61 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN0 )
63 62 adantl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. NN0 )
64 wlksnfi 
 |-  ( ( G e. FinUSGraph /\ ( N - 2 ) e. NN0 ) -> { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = ( N - 2 ) } e. Fin )
65 18 63 64 syl2an 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = ( N - 2 ) } e. Fin )
66 simp2l 
 |-  ( ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) /\ w e. ( ClWalks ` G ) ) -> ( # ` ( 1st ` w ) ) = ( N - 2 ) )
67 25 66 rabssrabd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) } C_ { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = ( N - 2 ) } )
68 65 67 ssfid 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) } e. Fin )
69 3 68 eqeltrid 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> F e. Fin )
70 1 clwwlknonfin 
 |-  ( V e. Fin -> ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin )
71 70 ad2antrr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin )
72 hashen 
 |-  ( ( F e. Fin /\ ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin ) -> ( ( # ` F ) = ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) <-> F ~~ ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) )
73 69 71 72 syl2anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` F ) = ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) <-> F ~~ ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) )
74 60 73 mpbird 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` F ) = ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) )
75 74 eqcomd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) = ( # ` F ) )
76 75 oveq2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) = ( K x. ( # ` F ) ) )
77 53 76 eqtrd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) = ( K x. ( # ` F ) ) )
78 37 50 77 3eqtr2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )