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 )