This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wwlksnprcl

Description: Derivation of the length of a word W whose concatenation with a singleton word represents a walk of a fixed length N (a partial reverse closure theorem). (Contributed by AV, 4-Mar-2022)

Ref Expression
Assertion wwlksnprcl 
|- ( ( W e. Word V /\ N e. NN0 ) -> ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( # ` W ) = N ) )

Proof

Step Hyp Ref Expression
1 iswwlksn 
 |-  ( N e. NN0 -> ( ( W ++ <" X "> ) e. ( N WWalksN G ) <-> ( ( W ++ <" X "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) ) )
2 1 adantl 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( W ++ <" X "> ) e. ( N WWalksN G ) <-> ( ( W ++ <" X "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) ) )
3 ccatws1lenp1b 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )
4 3 biimpd 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) -> ( # ` W ) = N ) )
5 4 adantld 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( ( W ++ <" X "> ) e. ( WWalks ` G ) /\ ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) ) -> ( # ` W ) = N ) )
6 2 5 sylbid 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( W ++ <" X "> ) e. ( N WWalksN G ) -> ( # ` W ) = N ) )