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