Theorem pmtrdifwrdellem3

Description: Lemma 3 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	pmtrdifwrdellem3	|- ( W e. Word T -> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )

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 /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) e. T )
5		eqid	|- ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) )
6	1 2 5	pmtrdifellem3	|- ( ( W ` i ) e. T -> A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` n ) )
7	4 6	syl	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` n ) )
8		fveq2	|- ( x = i -> ( W ` x ) = ( W ` i ) )
9	8	difeq1d	|- ( x = i -> ( ( W ` x ) \ _I ) = ( ( W ` i ) \ _I ) )
10	9	dmeqd	|- ( x = i -> dom ( ( W ` x ) \ _I ) = dom ( ( W ` i ) \ _I ) )
11	10	fveq2d	|- ( x = i -> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) )
12		simpr	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
13		fvexd	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) e. _V )
14	3 11 12 13	fvmptd3	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( U ` i ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) )
15	14	fveq1d	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( U ` i ) ` n ) = ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` n ) )
16	15	eqeq2d	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) <-> ( ( W ` i ) ` n ) = ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` n ) ) )
17	16	ralbidv	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) <-> A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` n ) ) )
18	7 17	mpbird	|- ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )
19	18	ralrimiva	|- ( W e. Word T -> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. ( N \ { K } ) ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) )