Metamath Proof Explorer

Theorem erclwwlkeqlen

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, 29-Apr-2021)

		Ref	Expression
	Hypothesis	erclwwlk.r	$⊢ \underset{˙}{\sim} = \{⟨u, w⟩ \| (u \in ClWWalks (G) \land w \in ClWWalks (G) \land \exists n \in (0 \dots \|w\|) u = w cyclShift n)\}$
	Assertion	erclwwlkeqlen	$⊢ (U \in X \land W \in Y) \to (U \underset{˙}{\sim} W \to \|U\| = \|W\|)$

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	$⊢ \underset{˙}{\sim} = \{⟨u, w⟩ \| (u \in ClWWalks (G) \land w \in ClWWalks (G) \land \exists n \in (0 \dots \|w\|) u = w cyclShift n)\}$
2	1	erclwwlkeq	$⊢ (U \in X \land W \in Y) \to (U \underset{˙}{\sim} W \leftrightarrow (U \in ClWWalks (G) \land W \in ClWWalks (G) \land \exists n \in (0 \dots \|W\|) U = W cyclShift n))$
3		fveq2	$⊢ U = W cyclShift n \to \|U\| = \|W cyclShift n\|$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5	4	clwwlkbp	$⊢ W \in ClWWalks (G) \to (G \in V \land W \in Word Vtx (G) \land W \neq \emptyset)$
6	5	simp2d	$⊢ W \in ClWWalks (G) \to W \in Word Vtx (G)$
7	6	ad2antlr	$⊢ ((U \in ClWWalks (G) \land W \in ClWWalks (G)) \land (U \in X \land W \in Y)) \to W \in Word Vtx (G)$
8		elfzelz	$⊢ n \in (0 \dots \|W\|) \to n \in ℤ$
9		cshwlen	$⊢ (W \in Word Vtx (G) \land n \in ℤ) \to \|W cyclShift n\| = \|W\|$
10	7 8 9	syl2an	$⊢ (((U \in ClWWalks (G) \land W \in ClWWalks (G)) \land (U \in X \land W \in Y)) \land n \in (0 \dots \|W\|)) \to \|W cyclShift n\| = \|W\|$
11	3 10	sylan9eqr	$⊢ ((((U \in ClWWalks (G) \land W \in ClWWalks (G)) \land (U \in X \land W \in Y)) \land n \in (0 \dots \|W\|)) \land U = W cyclShift n) \to \|U\| = \|W\|$
12	11	rexlimdva2	$⊢ ((U \in ClWWalks (G) \land W \in ClWWalks (G)) \land (U \in X \land W \in Y)) \to (\exists n \in (0 \dots \|W\|) U = W cyclShift n \to \|U\| = \|W\|)$
13	12	ex	$⊢ (U \in ClWWalks (G) \land W \in ClWWalks (G)) \to ((U \in X \land W \in Y) \to (\exists n \in (0 \dots \|W\|) U = W cyclShift n \to \|U\| = \|W\|))$
14	13	com23	$⊢ (U \in ClWWalks (G) \land W \in ClWWalks (G)) \to (\exists n \in (0 \dots \|W\|) U = W cyclShift n \to ((U \in X \land W \in Y) \to \|U\| = \|W\|))$
15	14	3impia	$⊢ (U \in ClWWalks (G) \land W \in ClWWalks (G) \land \exists n \in (0 \dots \|W\|) U = W cyclShift n) \to ((U \in X \land W \in Y) \to \|U\| = \|W\|)$
16	15	com12	$⊢ (U \in X \land W \in Y) \to ((U \in ClWWalks (G) \land W \in ClWWalks (G) \land \exists n \in (0 \dots \|W\|) U = W cyclShift n) \to \|U\| = \|W\|)$
17	2 16	sylbid	$⊢ (U \in X \land W \in Y) \to (U \underset{˙}{\sim} W \to \|U\| = \|W\|)$