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 ClWalks G | 1 st w = N 2 nd w 0 = X 2 nd w N 2 = X
numclwlk1.f F = w ClWalks G | 1 st w = N 2 2 nd w 0 = X
Assertion numclwlk1lem1 V Fin G RegUSGraph K X V N = 2 C = K F

Proof

Step Hyp Ref Expression
1 numclwlk1.v V = Vtx G
2 numclwlk1.c C = w ClWalks G | 1 st w = N 2 nd w 0 = X 2 nd w N 2 = X
3 numclwlk1.f F = w ClWalks G | 1 st w = N 2 2 nd w 0 = X
4 3anass 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X
5 anidm 2 nd w 0 = X 2 nd w 0 = X 2 nd w 0 = X
6 5 anbi2i 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X 1 st w = 2 2 nd w 0 = X
7 4 6 bitri 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X 1 st w = 2 2 nd w 0 = X
8 7 rabbii w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X = w ClWalks G | 1 st w = 2 2 nd w 0 = X
9 8 fveq2i w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X = w ClWalks G | 1 st w = 2 2 nd w 0 = X
10 simpl V Fin G RegUSGraph K V Fin
11 simpr V Fin G RegUSGraph K G RegUSGraph K
12 simpl X V N = 2 X V
13 1 clwlknon2num V Fin G RegUSGraph K X V w ClWalks G | 1 st w = 2 2 nd w 0 = X = K
14 10 11 12 13 syl2an3an V Fin G RegUSGraph K X V N = 2 w ClWalks G | 1 st w = 2 2 nd w 0 = X = K
15 9 14 syl5eq V Fin G RegUSGraph K X V N = 2 w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X = K
16 rusgrusgr G RegUSGraph K G USGraph
17 16 anim2i V Fin G RegUSGraph K V Fin G USGraph
18 17 ancomd V Fin G RegUSGraph K G USGraph V Fin
19 1 isfusgr G FinUSGraph G USGraph V Fin
20 18 19 sylibr V Fin G RegUSGraph K G FinUSGraph
21 ne0i X V V
22 21 adantr X V N = 2 V
23 1 frusgrnn0 G FinUSGraph G RegUSGraph K V K 0
24 20 11 22 23 syl2an3an V Fin G RegUSGraph K X V N = 2 K 0
25 24 nn0red V Fin G RegUSGraph K X V N = 2 K
26 ax-1rid K K 1 = K
27 25 26 syl V Fin G RegUSGraph K X V N = 2 K 1 = K
28 1 wlkl0 X V w ClWalks G | 1 st w = 0 2 nd w 0 = X = 0 X
29 28 ad2antrl V Fin G RegUSGraph K X V N = 2 w ClWalks G | 1 st w = 0 2 nd w 0 = X = 0 X
30 29 fveq2d V Fin G RegUSGraph K X V N = 2 w ClWalks G | 1 st w = 0 2 nd w 0 = X = 0 X
31 opex 0 X V
32 hashsng 0 X V 0 X = 1
33 31 32 ax-mp 0 X = 1
34 30 33 eqtr2di V Fin G RegUSGraph K X V N = 2 1 = w ClWalks G | 1 st w = 0 2 nd w 0 = X
35 34 oveq2d V Fin G RegUSGraph K X V N = 2 K 1 = K w ClWalks G | 1 st w = 0 2 nd w 0 = X
36 15 27 35 3eqtr2d V Fin G RegUSGraph K X V N = 2 w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X = K w ClWalks G | 1 st w = 0 2 nd w 0 = X
37 eqeq2 N = 2 1 st w = N 1 st w = 2
38 oveq1 N = 2 N 2 = 2 2
39 2cn 2
40 39 subidi 2 2 = 0
41 38 40 eqtrdi N = 2 N 2 = 0
42 41 fveqeq2d N = 2 2 nd w N 2 = X 2 nd w 0 = X
43 37 42 3anbi13d N = 2 1 st w = N 2 nd w 0 = X 2 nd w N 2 = X 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X
44 43 rabbidv N = 2 w ClWalks G | 1 st w = N 2 nd w 0 = X 2 nd w N 2 = X = w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X
45 2 44 syl5eq N = 2 C = w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X
46 45 fveq2d N = 2 C = w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X
47 41 eqeq2d N = 2 1 st w = N 2 1 st w = 0
48 47 anbi1d N = 2 1 st w = N 2 2 nd w 0 = X 1 st w = 0 2 nd w 0 = X
49 48 rabbidv N = 2 w ClWalks G | 1 st w = N 2 2 nd w 0 = X = w ClWalks G | 1 st w = 0 2 nd w 0 = X
50 3 49 syl5eq N = 2 F = w ClWalks G | 1 st w = 0 2 nd w 0 = X
51 50 fveq2d N = 2 F = w ClWalks G | 1 st w = 0 2 nd w 0 = X
52 51 oveq2d N = 2 K F = K w ClWalks G | 1 st w = 0 2 nd w 0 = X
53 46 52 eqeq12d N = 2 C = K F w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X = K w ClWalks G | 1 st w = 0 2 nd w 0 = X
54 53 ad2antll V Fin G RegUSGraph K X V N = 2 C = K F w ClWalks G | 1 st w = 2 2 nd w 0 = X 2 nd w 0 = X = K w ClWalks G | 1 st w = 0 2 nd w 0 = X
55 36 54 mpbird V Fin G RegUSGraph K X V N = 2 C = K F