Metamath Proof Explorer

Theorem pmtrdifwrdel

Description: A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set. (Contributed by AV, 15-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t 
|- T = ran ( pmTrsp ` ( N \ { K } ) )
pmtrdifel.r 
|- R = ran ( pmTrsp ` N )
Assertion pmtrdifwrdel 
|- A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) )

Proof

Step Hyp Ref Expression
1 pmtrdifel.t 
 |-  T = ran ( pmTrsp ` ( N \ { K } ) )
2 pmtrdifel.r 
 |-  R = ran ( pmTrsp ` N )
3 fveq2 
 |-  ( j = n -> ( w ` j ) = ( w ` n ) )
4 3 difeq1d 
 |-  ( j = n -> ( ( w ` j ) \ _I ) = ( ( w ` n ) \ _I ) )
5 4 dmeqd 
 |-  ( j = n -> dom ( ( w ` j ) \ _I ) = dom ( ( w ` n ) \ _I ) )
6 5 fveq2d 
 |-  ( j = n -> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( ( w ` n ) \ _I ) ) )
7 6 cbvmptv 
 |-  ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) = ( n e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` n ) \ _I ) ) )
8 1 2 7 pmtrdifwrdellem1 
 |-  ( w e. Word T -> ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) e. Word R )
9 1 2 7 pmtrdifwrdellem2 
 |-  ( w e. Word T -> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) )
10 1 2 7 pmtrdifwrdellem3 
 |-  ( w e. Word T -> A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) )
11 fveq2 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( # ` u ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) )
12 11 eqeq2d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( # ` w ) = ( # ` u ) <-> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) ) )
13 fveq1 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( u ` i ) = ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) )
14 13 fveq1d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( u ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) )
15 14 eqeq2d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) <-> ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) )
16 15 2ralbidv 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) <-> A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) )
17 12 16 anbi12d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) <-> ( ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) )
18 17 rspcev 
 |-  ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) e. Word R /\ ( ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) -> E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) )
19 8 9 10 18 syl12anc 
 |-  ( w e. Word T -> E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) )
20 19 rgen 
 |-  A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) )