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

Metamath Proof Explorer

Theorem erclwwlkeq

Description: Two classes are equivalent regarding .~ if both are words and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-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

|- ( ( 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 ) ) ) )

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		eleq1	\|- ( u = U -> ( u e. ( ClWWalks ` G ) <-> U e. ( ClWWalks ` G ) ) )
3	2	adantr	\|- ( ( u = U /\ w = W ) -> ( u e. ( ClWWalks ` G ) <-> U e. ( ClWWalks ` G ) ) )
4		eleq1	\|- ( w = W -> ( w e. ( ClWWalks ` G ) <-> W e. ( ClWWalks ` G ) ) )
5	4	adantl	\|- ( ( u = U /\ w = W ) -> ( w e. ( ClWWalks ` G ) <-> W e. ( ClWWalks ` G ) ) )
6		fveq2	\|- ( w = W -> ( # ` w ) = ( # ` W ) )
7	6	oveq2d	\|- ( w = W -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` W ) ) )
8	7	adantl	\|- ( ( u = U /\ w = W ) -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` W ) ) )
9		simpl	\|- ( ( u = U /\ w = W ) -> u = U )
10		oveq1	\|- ( w = W -> ( w cyclShift n ) = ( W cyclShift n ) )
11	10	adantl	\|- ( ( u = U /\ w = W ) -> ( w cyclShift n ) = ( W cyclShift n ) )
12	9 11	eqeq12d	\|- ( ( u = U /\ w = W ) -> ( u = ( w cyclShift n ) <-> U = ( W cyclShift n ) ) )
13	8 12	rexeqbidv	\|- ( ( u = U /\ w = W ) -> ( E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) <-> E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) )
14	3 5 13	3anbi123d	\|- ( ( u = U /\ w = W ) -> ( ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) <-> ( U e. ( ClWWalks ` G ) /\ W e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) ) )
15	14 1	brabga	\|- ( ( 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 ) ) ) )