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 \in Word V \land N \in ℕ_{0}) \to (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to \|W\| = N)$

Proof

Step	Hyp	Ref	Expression
1		iswwlksn	$⊢ N \in ℕ_{0} \to (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \leftrightarrow (W ++ ⟨“ X ”⟩ \in WWalks (G) \land \|W ++ ⟨“ X ”⟩\| = N + 1))$
2	1	adantl	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \leftrightarrow (W ++ ⟨“ X ”⟩ \in WWalks (G) \land \|W ++ ⟨“ X ”⟩\| = N + 1))$
3		ccatws1lenp1b	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \leftrightarrow \|W\| = N)$
4	3	biimpd	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \to \|W\| = N)$
5	4	adantld	$⊢ (W \in Word V \land N \in ℕ_{0}) \to ((W ++ ⟨“ X ”⟩ \in WWalks (G) \land \|W ++ ⟨“ X ”⟩\| = N + 1) \to \|W\| = N)$
6	2 5	sylbid	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to \|W\| = N)$