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	⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
Assertion	erclwwlkeqlen	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑈 ∼ 𝑊 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
2	1	erclwwlkeq	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑈 ∼ 𝑊 ↔ ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) ) )
3		fveq2	⊢ ( 𝑈 = ( 𝑊 cyclShift 𝑛 ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 𝑊 cyclShift 𝑛 ) ) )
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5	4	clwwlkbp	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) )
6	5	simp2d	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
7	6	ad2antlr	⊢ ( ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
8		elfzelz	⊢ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑛 ∈ ℤ )
9		cshwlen	⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑛 ) ) = ( ♯ ‘ 𝑊 ) )
10	7 8 9	syl2an	⊢ ( ( ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑛 ) ) = ( ♯ ‘ 𝑊 ) )
11	3 10	sylan9eqr	⊢ ( ( ( ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) )
12	11	rexlimdva2	⊢ ( ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )
13	12	ex	⊢ ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) ) )
14	13	com23	⊢ ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) → ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) ) )
15	14	3impia	⊢ ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) → ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )
16	15	com12	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )
17	2 16	sylbid	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑈 ∼ 𝑊 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )