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

Metamath Proof Explorer

Theorem eleclclwwlknlem1

Description: Lemma 1 for eleclclwwlkn . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 30-Apr-2021)

		Ref	Expression
	Hypothesis	erclwwlkn1.w	$⊢ W = N ClWWalksN G$
	Assertion	eleclclwwlknlem1	$⊢ (K \in (0 \dots N) \land (X \in W \land Y \in W)) \to ((X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn1.w	$⊢ W = N ClWWalksN G$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	clwwlknbp	$⊢ Y \in (N ClWWalksN G) \to (Y \in Word Vtx (G) \land \|Y\| = N)$
4	3 1	eleq2s	$⊢ Y \in W \to (Y \in Word Vtx (G) \land \|Y\| = N)$
5	4	adantl	$⊢ (X \in W \land Y \in W) \to (Y \in Word Vtx (G) \land \|Y\| = N)$
6	5	adantl	$⊢ (K \in (0 \dots N) \land (X \in W \land Y \in W)) \to (Y \in Word Vtx (G) \land \|Y\| = N)$
7	6	adantr	$⊢ ((K \in (0 \dots N) \land (X \in W \land Y \in W)) \land (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)) \to (Y \in Word Vtx (G) \land \|Y\| = N)$
8		simpl	$⊢ (K \in (0 \dots N) \land (X \in W \land Y \in W)) \to K \in (0 \dots N)$
9	8	adantr	$⊢ ((K \in (0 \dots N) \land (X \in W \land Y \in W)) \land (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)) \to K \in (0 \dots N)$
10		simpl	$⊢ (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to X = Y cyclShift K$
11	10	adantl	$⊢ ((K \in (0 \dots N) \land (X \in W \land Y \in W)) \land (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)) \to X = Y cyclShift K$
12		simprr	$⊢ ((K \in (0 \dots N) \land (X \in W \land Y \in W)) \land (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)) \to \exists m \in (0 \dots N) Z = Y cyclShift m$
13	9 11 12	3jca	$⊢ ((K \in (0 \dots N) \land (X \in W \land Y \in W)) \land (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)) \to (K \in (0 \dots N) \land X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)$
14		2cshwcshw	$⊢ (Y \in Word Vtx (G) \land \|Y\| = N) \to ((K \in (0 \dots N) \land X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$
15	7 13 14	sylc	$⊢ ((K \in (0 \dots N) \land (X \in W \land Y \in W)) \land (X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m)) \to \exists n \in (0 \dots N) Z = X cyclShift n$
16	15	ex	$⊢ (K \in (0 \dots N) \land (X \in W \land Y \in W)) \to ((X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$