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