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

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 ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( 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 ⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑈 ∼ 𝑊 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑊 ) ) )