| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pmtrdifel.t |
|- T = ran ( pmTrsp ` ( N \ { K } ) ) |
| 2 |
|
pmtrdifel.r |
|- R = ran ( pmTrsp ` N ) |
| 3 |
|
pmtrdifwrdel.0 |
|- U = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) ) |
| 4 |
|
wrdsymbcl |
|- ( ( W e. Word T /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` x ) e. T ) |
| 5 |
|
eqid |
|- ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) |
| 6 |
1 2 5
|
pmtrdifellem1 |
|- ( ( W ` x ) e. T -> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) e. R ) |
| 7 |
4 6
|
syl |
|- ( ( W e. Word T /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) e. R ) |
| 8 |
7
|
ralrimiva |
|- ( W e. Word T -> A. x e. ( 0 ..^ ( # ` W ) ) ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) e. R ) |
| 9 |
3
|
fnmpt |
|- ( A. x e. ( 0 ..^ ( # ` W ) ) ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) e. R -> U Fn ( 0 ..^ ( # ` W ) ) ) |
| 10 |
|
hashfn |
|- ( U Fn ( 0 ..^ ( # ` W ) ) -> ( # ` U ) = ( # ` ( 0 ..^ ( # ` W ) ) ) ) |
| 11 |
8 9 10
|
3syl |
|- ( W e. Word T -> ( # ` U ) = ( # ` ( 0 ..^ ( # ` W ) ) ) ) |
| 12 |
|
lencl |
|- ( W e. Word T -> ( # ` W ) e. NN0 ) |
| 13 |
|
hashfzo0 |
|- ( ( # ` W ) e. NN0 -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) ) |
| 14 |
12 13
|
syl |
|- ( W e. Word T -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) ) |
| 15 |
11 14
|
eqtr2d |
|- ( W e. Word T -> ( # ` W ) = ( # ` U ) ) |