Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem1

Description: Lemma 1 for clwlknf1oclwwlkn . (Contributed by AV, 26-May-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion clwlknf1oclwwlknlem1 
|- ( ( C e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( # ` ( 1st ` C ) ) )

Proof

Step Hyp Ref Expression
1 clwlkwlk 
 |-  ( C e. ( ClWalks ` G ) -> C e. ( Walks ` G ) )
2 wlkcpr 
 |-  ( C e. ( Walks ` G ) <-> ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 wlkpwrd 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( 2nd ` C ) e. Word ( Vtx ` G ) )
5 lencl 
 |-  ( ( 2nd ` C ) e. Word ( Vtx ` G ) -> ( # ` ( 2nd ` C ) ) e. NN0 )
6 4 5 syl 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( # ` ( 2nd ` C ) ) e. NN0 )
7 wlklenvm1 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( # ` ( 1st ` C ) ) = ( ( # ` ( 2nd ` C ) ) - 1 ) )
8 7 breq2d 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( 1 <_ ( # ` ( 1st ` C ) ) <-> 1 <_ ( ( # ` ( 2nd ` C ) ) - 1 ) ) )
9 1red 
 |-  ( ( # ` ( 2nd ` C ) ) e. NN0 -> 1 e. RR )
10 nn0re 
 |-  ( ( # ` ( 2nd ` C ) ) e. NN0 -> ( # ` ( 2nd ` C ) ) e. RR )
11 9 9 10 leaddsub2d 
 |-  ( ( # ` ( 2nd ` C ) ) e. NN0 -> ( ( 1 + 1 ) <_ ( # ` ( 2nd ` C ) ) <-> 1 <_ ( ( # ` ( 2nd ` C ) ) - 1 ) ) )
12 1p1e2 
 |-  ( 1 + 1 ) = 2
13 12 breq1i 
 |-  ( ( 1 + 1 ) <_ ( # ` ( 2nd ` C ) ) <-> 2 <_ ( # ` ( 2nd ` C ) ) )
14 13 biimpi 
 |-  ( ( 1 + 1 ) <_ ( # ` ( 2nd ` C ) ) -> 2 <_ ( # ` ( 2nd ` C ) ) )
15 11 14 biimtrrdi 
 |-  ( ( # ` ( 2nd ` C ) ) e. NN0 -> ( 1 <_ ( ( # ` ( 2nd ` C ) ) - 1 ) -> 2 <_ ( # ` ( 2nd ` C ) ) ) )
16 4 5 15 3syl 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( 1 <_ ( ( # ` ( 2nd ` C ) ) - 1 ) -> 2 <_ ( # ` ( 2nd ` C ) ) ) )
17 8 16 sylbid 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( 1 <_ ( # ` ( 1st ` C ) ) -> 2 <_ ( # ` ( 2nd ` C ) ) ) )
18 17 imp 
 |-  ( ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> 2 <_ ( # ` ( 2nd ` C ) ) )
19 ige2m1fz 
 |-  ( ( ( # ` ( 2nd ` C ) ) e. NN0 /\ 2 <_ ( # ` ( 2nd ` C ) ) ) -> ( ( # ` ( 2nd ` C ) ) - 1 ) e. ( 0 ... ( # ` ( 2nd ` C ) ) ) )
20 6 18 19 syl2an2r 
 |-  ( ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> ( ( # ` ( 2nd ` C ) ) - 1 ) e. ( 0 ... ( # ` ( 2nd ` C ) ) ) )
21 pfxlen 
 |-  ( ( ( 2nd ` C ) e. Word ( Vtx ` G ) /\ ( ( # ` ( 2nd ` C ) ) - 1 ) e. ( 0 ... ( # ` ( 2nd ` C ) ) ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( ( # ` ( 2nd ` C ) ) - 1 ) )
22 4 20 21 syl2an2r 
 |-  ( ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( ( # ` ( 2nd ` C ) ) - 1 ) )
23 7 eqcomd 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( ( # ` ( 2nd ` C ) ) - 1 ) = ( # ` ( 1st ` C ) ) )
24 23 adantr 
 |-  ( ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> ( ( # ` ( 2nd ` C ) ) - 1 ) = ( # ` ( 1st ` C ) ) )
25 22 24 eqtrd 
 |-  ( ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( # ` ( 1st ` C ) ) )
26 25 ex 
 |-  ( ( 1st ` C ) ( Walks ` G ) ( 2nd ` C ) -> ( 1 <_ ( # ` ( 1st ` C ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( # ` ( 1st ` C ) ) ) )
27 2 26 sylbi 
 |-  ( C e. ( Walks ` G ) -> ( 1 <_ ( # ` ( 1st ` C ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( # ` ( 1st ` C ) ) ) )
28 1 27 syl 
 |-  ( C e. ( ClWalks ` G ) -> ( 1 <_ ( # ` ( 1st ` C ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( # ` ( 1st ` C ) ) ) )
29 28 imp 
 |-  ( ( C e. ( ClWalks ` G ) /\ 1 <_ ( # ` ( 1st ` C ) ) ) -> ( # ` ( ( 2nd ` C ) prefix ( ( # ` ( 2nd ` C ) ) - 1 ) ) ) = ( # ` ( 1st ` C ) ) )