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 
|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
Assertion erclwwlkeqlen 
|- ( ( U e. X /\ W e. Y ) -> ( U .~ W -> ( # ` U ) = ( # ` W ) ) )

Proof

Step Hyp Ref Expression
1 erclwwlk.r 
 |-  .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
2 1 erclwwlkeq 
 |-  ( ( U e. X /\ W e. Y ) -> ( U .~ W <-> ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) ) )
3 fveq2 
 |-  ( U = ( W cyclShift n ) -> ( # ` U ) = ( # ` ( W cyclShift n ) ) )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 clwwlkbp 
 |-  ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word ( Vtx ` G ) /\ W =/= (/) ) )
6 5 simp2d 
 |-  ( W e. ( ClWWalks ` G ) -> W e. Word ( Vtx ` G ) )
7 6 ad2antlr 
 |-  ( ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) ) /\ ( U e. X /\ W e. Y ) ) -> W e. Word ( Vtx ` G ) )
8 elfzelz 
 |-  ( n e. ( 0 ... ( # ` W ) ) -> n e. ZZ )
9 cshwlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ n e. ZZ ) -> ( # ` ( W cyclShift n ) ) = ( # ` W ) )
10 7 8 9 syl2an 
 |-  ( ( ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) ) /\ ( U e. X /\ W e. Y ) ) /\ n e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W cyclShift n ) ) = ( # ` W ) )
11 3 10 sylan9eqr 
 |-  ( ( ( ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) ) /\ ( U e. X /\ W e. Y ) ) /\ n e. ( 0 ... ( # ` W ) ) ) /\ U = ( W cyclShift n ) ) -> ( # ` U ) = ( # ` W ) )
12 11 rexlimdva2 
 |-  ( ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) ) /\ ( U e. X /\ W e. Y ) ) -> ( E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) -> ( # ` U ) = ( # ` W ) ) )
13 12 ex 
 |-  ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) ) -> ( ( U e. X /\ W e. Y ) -> ( E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) -> ( # ` U ) = ( # ` W ) ) ) )
14 13 com23 
 |-  ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) ) -> ( E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) -> ( ( U e. X /\ W e. Y ) -> ( # ` U ) = ( # ` W ) ) ) )
15 14 3impia 
 |-  ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) -> ( ( U e. X /\ W e. Y ) -> ( # ` U ) = ( # ` W ) ) )
16 15 com12 
 |-  ( ( U e. X /\ W e. Y ) -> ( ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) -> ( # ` U ) = ( # ` W ) ) )
17 2 16 sylbid 
 |-  ( ( U e. X /\ W e. Y ) -> ( U .~ W -> ( # ` U ) = ( # ` W ) ) )