Metamath Proof Explorer


Theorem clwlknf1oclwwlknlem3

Description: Lemma 3 for clwlknf1oclwwlkn : The bijective function of clwlknf1oclwwlkn is the bijective function of clwlkclwwlkf1o restricted to the closed walks with a fixed positive length. (Contributed by AV, 26-May-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwlknf1oclwwlkn.a A = 1 st c
clwlknf1oclwwlkn.b B = 2 nd c
clwlknf1oclwwlkn.c C = w ClWalks G | 1 st w = N
clwlknf1oclwwlkn.f F = c C B prefix A
Assertion clwlknf1oclwwlknlem3 G USHGraph N F = c w ClWalks G | 1 1 st w B prefix A C

Proof

Step Hyp Ref Expression
1 clwlknf1oclwwlkn.a A = 1 st c
2 clwlknf1oclwwlkn.b B = 2 nd c
3 clwlknf1oclwwlkn.c C = w ClWalks G | 1 st w = N
4 clwlknf1oclwwlkn.f F = c C B prefix A
5 nnge1 N 1 N
6 breq2 1 st w = N 1 1 st w 1 N
7 5 6 syl5ibrcom N 1 st w = N 1 1 st w
8 7 ad2antlr G USHGraph N w ClWalks G 1 st w = N 1 1 st w
9 8 ss2rabdv G USHGraph N w ClWalks G | 1 st w = N w ClWalks G | 1 1 st w
10 3 9 eqsstrid G USHGraph N C w ClWalks G | 1 1 st w
11 10 resmptd G USHGraph N c w ClWalks G | 1 1 st w B prefix A C = c C B prefix A
12 4 11 eqtr4id G USHGraph N F = c w ClWalks G | 1 1 st w B prefix A C