Step |
Hyp |
Ref |
Expression |
1 |
|
pmtrdifel.t |
|- T = ran ( pmTrsp ` ( N \ { K } ) ) |
2 |
|
pmtrdifel.r |
|- R = ran ( pmTrsp ` N ) |
3 |
|
fveq2 |
|- ( j = n -> ( w ` j ) = ( w ` n ) ) |
4 |
3
|
difeq1d |
|- ( j = n -> ( ( w ` j ) \ _I ) = ( ( w ` n ) \ _I ) ) |
5 |
4
|
dmeqd |
|- ( j = n -> dom ( ( w ` j ) \ _I ) = dom ( ( w ` n ) \ _I ) ) |
6 |
5
|
fveq2d |
|- ( j = n -> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( w ` n ) \ _I ) ) ) |
7 |
6
|
cbvmptv |
|- ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) = ( n e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` n ) \ _I ) ) ) |
8 |
1 2 7
|
pmtrdifwrdellem1 |
|- ( w e. Word T -> ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) e. Word R ) |
9 |
8
|
adantl |
|- ( ( K e. N /\ w e. Word T ) -> ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) e. Word R ) |
10 |
1 2 7
|
pmtrdifwrdellem2 |
|- ( w e. Word T -> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) ) |
11 |
10
|
adantl |
|- ( ( K e. N /\ w e. Word T ) -> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) ) |
12 |
1 2 7
|
pmtrdifwrdel2lem1 |
|- ( ( w e. Word T /\ K e. N ) -> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K ) |
13 |
12
|
ancoms |
|- ( ( K e. N /\ w e. Word T ) -> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K ) |
14 |
1 2 7
|
pmtrdifwrdellem3 |
|- ( w e. Word T -> A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) |
15 |
14
|
adantl |
|- ( ( K e. N /\ w e. Word T ) -> A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) |
16 |
|
r19.26 |
|- ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) <-> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) |
17 |
13 15 16
|
sylanbrc |
|- ( ( K e. N /\ w e. Word T ) -> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) |
18 |
|
fveq2 |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( # ` u ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) ) |
19 |
18
|
eqeq2d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( # ` w ) = ( # ` u ) <-> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) ) ) |
20 |
|
fveq1 |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( u ` i ) = ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ) |
21 |
20
|
fveq1d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( u ` i ) ` K ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) ) |
22 |
21
|
eqeq1d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( u ` i ) ` K ) = K <-> ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K ) ) |
23 |
20
|
fveq1d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( u ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) |
24 |
23
|
eqeq2d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) <-> ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) |
25 |
24
|
ralbidv |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) <-> A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) |
26 |
22 25
|
anbi12d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) <-> ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) ) |
27 |
26
|
ralbidv |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) <-> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) ) |
28 |
19 27
|
anbi12d |
|- ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) <-> ( ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) ) ) |
29 |
28
|
rspcev |
|- ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) e. Word R /\ ( ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) ) -> E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) ) |
30 |
9 11 17 29
|
syl12anc |
|- ( ( K e. N /\ w e. Word T ) -> E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) ) |
31 |
30
|
ralrimiva |
|- ( K e. N -> A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) ) |