Metamath Proof Explorer

Theorem numclwlk1lem1

Description: Lemma 1 for numclwlk1 (Statement 9 in Huneke p. 2 for n=2): "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)". (Contributed by AV, 23-May-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 numclwlk1lem1 
|- ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` 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 3anass 
 |-  ( ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) <-> ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) ) )
5 anidm 
 |-  ( ( ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) <-> ( ( 2nd ` w ) ` 0 ) = X )
6 5 anbi2i 
 |-  ( ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) ) <-> ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) )
7 4 6 bitri 
 |-  ( ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) <-> ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) )
8 7 rabbii 
 |-  { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) }
9 8 fveq2i 
 |-  ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } )
10 simpl 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> V e. Fin )
11 simpr 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> G RegUSGraph K )
12 simpl 
 |-  ( ( X e. V /\ N = 2 ) -> X e. V )
13 1 clwlknon2num 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = K )
14 10 11 12 13 syl2an3an 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = K )
15 9 14 syl5eq 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = K )
16 rusgrusgr 
 |-  ( G RegUSGraph K -> G e. USGraph )
17 16 anim2i 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( V e. Fin /\ G e. USGraph ) )
18 17 ancomd 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( G e. USGraph /\ V e. Fin ) )
19 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
20 18 19 sylibr 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> G e. FinUSGraph )
21 ne0i 
 |-  ( X e. V -> V =/= (/) )
22 21 adantr 
 |-  ( ( X e. V /\ N = 2 ) -> V =/= (/) )
23 1 frusgrnn0 
 |-  ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )
24 20 11 22 23 syl2an3an 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> K e. NN0 )
25 24 nn0red 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> K e. RR )
26 ax-1rid 
 |-  ( K e. RR -> ( K x. 1 ) = K )
27 25 26 syl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( K x. 1 ) = K )
28 1 wlkl0 
 |-  ( X e. V -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { <. (/) , { <. 0 , X >. } >. } )
29 28 ad2antrl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { <. (/) , { <. 0 , X >. } >. } )
30 29 fveq2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( # ` { <. (/) , { <. 0 , X >. } >. } ) )
31 opex 
 |-  <. (/) , { <. 0 , X >. } >. e. _V
32 hashsng 
 |-  ( <. (/) , { <. 0 , X >. } >. e. _V -> ( # ` { <. (/) , { <. 0 , X >. } >. } ) = 1 )
33 31 32 ax-mp 
 |-  ( # ` { <. (/) , { <. 0 , X >. } >. } ) = 1
34 30 33 eqtr2di 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> 1 = ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) )
35 34 oveq2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( K x. 1 ) = ( K x. ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) ) )
36 15 27 35 3eqtr2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( K x. ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) ) )
37 eqeq2 
 |-  ( N = 2 -> ( ( # ` ( 1st ` w ) ) = N <-> ( # ` ( 1st ` w ) ) = 2 ) )
38 oveq1 
 |-  ( N = 2 -> ( N - 2 ) = ( 2 - 2 ) )
39 2cn 
 |-  2 e. CC
40 39 subidi 
 |-  ( 2 - 2 ) = 0
41 38 40 eqtrdi 
 |-  ( N = 2 -> ( N - 2 ) = 0 )
42 41 fveqeq2d 
 |-  ( N = 2 -> ( ( ( 2nd ` w ) ` ( N - 2 ) ) = X <-> ( ( 2nd ` w ) ` 0 ) = X ) )
43 37 42 3anbi13d 
 |-  ( N = 2 -> ( ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) <-> ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) ) )
44 43 rabbidv 
 |-  ( N = 2 -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) } = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } )
45 2 44 syl5eq 
 |-  ( N = 2 -> C = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } )
46 45 fveq2d 
 |-  ( N = 2 -> ( # ` C ) = ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) )
47 41 eqeq2d 
 |-  ( N = 2 -> ( ( # ` ( 1st ` w ) ) = ( N - 2 ) <-> ( # ` ( 1st ` w ) ) = 0 ) )
48 47 anbi1d 
 |-  ( N = 2 -> ( ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) <-> ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) )
49 48 rabbidv 
 |-  ( N = 2 -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } )
50 3 49 syl5eq 
 |-  ( N = 2 -> F = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } )
51 50 fveq2d 
 |-  ( N = 2 -> ( # ` F ) = ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) )
52 51 oveq2d 
 |-  ( N = 2 -> ( K x. ( # ` F ) ) = ( K x. ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) ) )
53 46 52 eqeq12d 
 |-  ( N = 2 -> ( ( # ` C ) = ( K x. ( # ` F ) ) <-> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( K x. ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) ) ) )
54 53 ad2antll 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( ( # ` C ) = ( K x. ( # ` F ) ) <-> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( K x. ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) ) ) )
55 36 54 mpbird 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )