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