This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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