Metamath Proof Explorer


Theorem pmtrdifwrdellem2

Description: Lemma 2 for pmtrdifwrdel . (Contributed by AV, 15-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t
|- T = ran ( pmTrsp ` ( N \ { K } ) )
pmtrdifel.r
|- R = ran ( pmTrsp ` N )
pmtrdifwrdel.0
|- U = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) )
Assertion pmtrdifwrdellem2
|- ( W e. Word T -> ( # ` W ) = ( # ` U ) )

Proof

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