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

Metamath Proof Explorer

Theorem pmtrdifwrdel2lem1

Description: Lemma 1 for pmtrdifwrdel2 . (Contributed by AV, 31-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 pmtrdifwrdel2lem1 
|- ( ( W e. Word T /\ K e. N ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K )

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 simpr 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )
5 fvex 
 |-  ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) e. _V
6 fveq2 
 |-  ( x = i -> ( W ` x ) = ( W ` i ) )
7 6 difeq1d 
 |-  ( x = i -> ( ( W ` x ) \ _I ) = ( ( W ` i ) \ _I ) )
8 7 dmeqd 
 |-  ( x = i -> dom ( ( W ` x ) \ _I ) = dom ( ( W ` i ) \ _I ) )
9 8 fveq2d 
 |-  ( x = i -> ( ( pmTrsp ` N ) ` dom ( ( W ` x ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) )
10 9 3 fvmptg 
 |-  ( ( i e. ( 0 ..^ ( # ` W ) ) /\ ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) e. _V ) -> ( U ` i ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) )
11 4 5 10 sylancl 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( U ` i ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) )
12 11 fveq1d 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( U ` i ) ` K ) = ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` K ) )
13 wrdsymbcl 
 |-  ( ( W e. Word T /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) e. T )
14 13 adantlr 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) e. T )
15 simplr 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> K e. N )
16 eqid 
 |-  ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) )
17 1 2 16 pmtrdifellem4 
 |-  ( ( ( W ` i ) e. T /\ K e. N ) -> ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` K ) = K )
18 14 15 17 syl2anc 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( pmTrsp ` N ) ` dom ( ( W ` i ) \ _I ) ) ` K ) = K )
19 12 18 eqtrd 
 |-  ( ( ( W e. Word T /\ K e. N ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( U ` i ) ` K ) = K )
20 19 ralrimiva 
 |-  ( ( W e. Word T /\ K e. N ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( U ` i ) ` K ) = K )