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

Metamath Proof Explorer

Theorem erclwwlkneqlen

Description: If two classes are equivalent regarding .~ , then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-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	erclwwlkneqlen	$⊢ (T \in X \land U \in Y) \to (T \underset{˙}{\sim} U \to \|T\| = \|U\|)$

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	1 2	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))$
4		fveq2	$⊢ T = U cyclShift n \to \|T\| = \|U cyclShift n\|$
5		eqid	$⊢ Vtx (G) = Vtx (G)$
6	5	clwwlknwrd	$⊢ U \in (N ClWWalksN G) \to U \in Word Vtx (G)$
7	6 1	eleq2s	$⊢ U \in W \to U \in Word Vtx (G)$
8	7	adantl	$⊢ (T \in W \land U \in W) \to U \in Word Vtx (G)$
9		elfzelz	$⊢ n \in (0 \dots N) \to n \in ℤ$
10		cshwlen	$⊢ (U \in Word Vtx (G) \land n \in ℤ) \to \|U cyclShift n\| = \|U\|$
11	8 9 10	syl2an	$⊢ ((T \in W \land U \in W) \land n \in (0 \dots N)) \to \|U cyclShift n\| = \|U\|$
12	4 11	sylan9eqr	$⊢ (((T \in W \land U \in W) \land n \in (0 \dots N)) \land T = U cyclShift n) \to \|T\| = \|U\|$
13	12	rexlimdva2	$⊢ (T \in W \land U \in W) \to (\exists n \in (0 \dots N) T = U cyclShift n \to \|T\| = \|U\|)$
14	13	3impia	$⊢ (T \in W \land U \in W \land \exists n \in (0 \dots N) T = U cyclShift n) \to \|T\| = \|U\|$
15	3 14	biimtrdi	$⊢ (T \in X \land U \in Y) \to (T \underset{˙}{\sim} U \to \|T\| = \|U\|)$