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

Metamath Proof Explorer

Theorem erclwwlkneq

Description: Two classes are equivalent regarding .~ if both are words of the same fixed length and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 30-Apr-2021)

		Ref	Expression
	Hypotheses	erclwwlkn.w	$⊢ W = N ClWWalksN G$
		erclwwlkn.r	$⊢ \underset{˙}{\sim} = \{⟨t, u⟩ \| (t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
	Assertion	erclwwlkneq	$⊢ (T \in X \land U \in Y) \to (T \underset{˙}{\sim} U \leftrightarrow (T \in W \land U \in W \land \exists n \in (0 \dots N) T = U cyclShift n))$

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	$⊢ W = N ClWWalksN G$
2		erclwwlkn.r	$⊢ \underset{˙}{\sim} = \{⟨t, u⟩ \| (t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
3		eleq1	$⊢ t = T \to (t \in W \leftrightarrow T \in W)$
4	3	adantr	$⊢ (t = T \land u = U) \to (t \in W \leftrightarrow T \in W)$
5		eleq1	$⊢ u = U \to (u \in W \leftrightarrow U \in W)$
6	5	adantl	$⊢ (t = T \land u = U) \to (u \in W \leftrightarrow U \in W)$
7		simpl	$⊢ (t = T \land u = U) \to t = T$
8		oveq1	$⊢ u = U \to u cyclShift n = U cyclShift n$
9	8	adantl	$⊢ (t = T \land u = U) \to u cyclShift n = U cyclShift n$
10	7 9	eqeq12d	$⊢ (t = T \land u = U) \to (t = u cyclShift n \leftrightarrow T = U cyclShift n)$
11	10	rexbidv	$⊢ (t = T \land u = U) \to (\exists n \in (0 \dots N) t = u cyclShift n \leftrightarrow \exists n \in (0 \dots N) T = U cyclShift n)$
12	4 6 11	3anbi123d	$⊢ (t = T \land u = U) \to ((t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n) \leftrightarrow (T \in W \land U \in W \land \exists n \in (0 \dots N) T = U cyclShift n))$
13	12 2	brabga	$⊢ (T \in X \land U \in Y) \to (T \underset{˙}{\sim} U \leftrightarrow (T \in W \land U \in W \land \exists n \in (0 \dots N) T = U cyclShift n))$