Metamath Proof Explorer

Theorem pmtrdifwrdel2

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 not moving the special element. (Contributed by AV, 31-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t 
|- T = ran ( pmTrsp ` ( N \ { K } ) )
pmtrdifel.r 
|- R = ran ( pmTrsp ` N )
Assertion pmtrdifwrdel2 
|- ( K e. N -> A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ 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 8 adantl 
 |-  ( ( K e. N /\ w e. Word T ) -> ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) e. Word R )
10 1 2 7 pmtrdifwrdellem2 
 |-  ( w e. Word T -> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) )
11 10 adantl 
 |-  ( ( K e. N /\ w e. Word T ) -> ( # ` w ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) )
12 1 2 7 pmtrdifwrdel2lem1 
 |-  ( ( w e. Word T /\ K e. N ) -> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K )
13 12 ancoms 
 |-  ( ( K e. N /\ w e. Word T ) -> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K )
14 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 ) )
15 14 adantl 
 |-  ( ( K e. N /\ 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 ) )
16 r19.26 
 |-  ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) <-> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ 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 13 15 16 sylanbrc 
 |-  ( ( K e. N /\ w e. Word T ) -> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) )
18 fveq2 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( # ` u ) = ( # ` ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ) )
19 18 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 ) ) ) ) ) )
20 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 ) )
21 20 fveq1d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( u ` i ) ` K ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) )
22 21 eqeq1d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( u ` i ) ` K ) = K <-> ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K ) )
23 20 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 ) )
24 23 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 ) ) )
25 24 ralbidv 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) <-> A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) )
26 22 25 anbi12d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) <-> ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) )
27 26 ralbidv 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) <-> A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) )
28 19 27 anbi12d 
 |-  ( u = ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) -> ( ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ 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 ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` x ) ) ) ) )
29 28 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 ) ) ( ( ( ( j e. ( 0 ..^ ( # ` w ) ) |-> ( ( pmTrsp ` N ) ` dom ( ( w ` j ) \ _I ) ) ) ` i ) ` K ) = K /\ 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 ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) )
30 9 11 17 29 syl12anc 
 |-  ( ( K e. N /\ w e. Word T ) -> E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) )
31 30 ralrimiva 
 |-  ( K e. N -> A. w e. Word T E. u e. Word R ( ( # ` w ) = ( # ` u ) /\ A. i e. ( 0 ..^ ( # ` w ) ) ( ( ( u ` i ) ` K ) = K /\ A. x e. ( N \ { K } ) ( ( w ` i ) ` x ) = ( ( u ` i ) ` x ) ) ) )