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 ) )