Metamath Proof Explorer

Theorem wlklenvclwlkOLD

Description: Obsolete version of wlklenvclwlk as of 14-Jan-2024. The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018) (Revised by AV, 2-May-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion wlklenvclwlkOLD 
|- ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. ( Walks ` G ) -> ( # ` F ) = ( # ` W ) ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( F ( Walks ` G ) ( W ++ <" ( W ` 0 ) "> ) <-> <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. ( Walks ` G ) )
2 wlklenvp1 
 |-  ( F ( Walks ` G ) ( W ++ <" ( W ` 0 ) "> ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` F ) + 1 ) )
3 wlkcl 
 |-  ( F ( Walks ` G ) ( W ++ <" ( W ` 0 ) "> ) -> ( # ` F ) e. NN0 )
4 wrdsymb1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. ( Vtx ` G ) )
5 4 s1cld 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> <" ( W ` 0 ) "> e. Word ( Vtx ` G ) )
6 ccatlenOLD 
 |-  ( ( W e. Word ( Vtx ` G ) /\ <" ( W ` 0 ) "> e. Word ( Vtx ` G ) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) )
7 5 6 syldan 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) )
8 s1len 
 |-  ( # ` <" ( W ` 0 ) "> ) = 1
9 8 a1i 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( # ` <" ( W ` 0 ) "> ) = 1 )
10 9 oveq2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( ( # ` W ) + ( # ` <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + 1 ) )
11 7 10 eqtrd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` W ) + 1 ) )
12 11 eqeq1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` F ) + 1 ) <-> ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) ) )
13 lencl 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` W ) e. NN0 )
14 eqcom 
 |-  ( ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) <-> ( ( # ` F ) + 1 ) = ( ( # ` W ) + 1 ) )
15 nn0cn 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC )
16 15 adantl 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` F ) e. NN0 ) -> ( # ` F ) e. CC )
17 nn0cn 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
18 17 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` F ) e. NN0 ) -> ( # ` W ) e. CC )
19 1cnd 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` F ) e. NN0 ) -> 1 e. CC )
20 16 18 19 addcan2d 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` F ) e. NN0 ) -> ( ( ( # ` F ) + 1 ) = ( ( # ` W ) + 1 ) <-> ( # ` F ) = ( # ` W ) ) )
21 20 biimpd 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` F ) e. NN0 ) -> ( ( ( # ` F ) + 1 ) = ( ( # ` W ) + 1 ) -> ( # ` F ) = ( # ` W ) ) )
22 14 21 syl5bi 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` F ) e. NN0 ) -> ( ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) -> ( # ` F ) = ( # ` W ) ) )
23 22 ex 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` F ) e. NN0 -> ( ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) -> ( # ` F ) = ( # ` W ) ) ) )
24 23 com23 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) -> ( ( # ` F ) e. NN0 -> ( # ` F ) = ( # ` W ) ) ) )
25 13 24 syl 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) -> ( ( # ` F ) e. NN0 -> ( # ` F ) = ( # ` W ) ) ) )
26 25 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( ( ( # ` W ) + 1 ) = ( ( # ` F ) + 1 ) -> ( ( # ` F ) e. NN0 -> ( # ` F ) = ( # ` W ) ) ) )
27 12 26 sylbid 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` F ) + 1 ) -> ( ( # ` F ) e. NN0 -> ( # ` F ) = ( # ` W ) ) ) )
28 27 com3l 
 |-  ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) = ( ( # ` F ) + 1 ) -> ( ( # ` F ) e. NN0 -> ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( # ` F ) = ( # ` W ) ) ) )
29 2 3 28 sylc 
 |-  ( F ( Walks ` G ) ( W ++ <" ( W ` 0 ) "> ) -> ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( # ` F ) = ( # ` W ) ) )
30 1 29 sylbir 
 |-  ( <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. ( Walks ` G ) -> ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( # ` F ) = ( # ` W ) ) )
31 30 com12 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> ( <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. ( Walks ` G ) -> ( # ` F ) = ( # ` W ) ) )