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∈N→∀w∈WordT∃u∈WordRw=u∧∀i∈0..^wu⁡i⁡K=K∧∀x∈N∖Kw⁡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∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I=n∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡n∖I
8 1 2 7 pmtrdifwrdellem1 ⊢w∈WordT→j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∈WordR
9 8 adantl ⊢K∈N∧w∈WordT→j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∈WordR
10 1 2 7 pmtrdifwrdellem2 ⊢w∈WordT→w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
11 10 adantl ⊢K∈N∧w∈WordT→w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
12 1 2 7 pmtrdifwrdel2lem1 ⊢w∈WordT∧K∈N→∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K
13 12 ancoms ⊢K∈N∧w∈WordT→∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K
14 1 2 7 pmtrdifwrdellem3 ⊢w∈WordT→∀i∈0..^w∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
15 14 adantl ⊢K∈N∧w∈WordT→∀i∈0..^w∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
16 r19.26 ⊢∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x↔∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
17 13 15 16 sylanbrc ⊢K∈N∧w∈WordT→∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
18 fveq2 ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
19 18 eqeq2d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→w=u↔w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
20 fveq1 ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u⁡i=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i
21 20 fveq1d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u⁡i⁡K=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K
22 21 eqeq1d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u⁡i⁡K=K↔j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K
23 20 fveq1d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
24 23 eqeq2d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→w⁡i⁡x=u⁡i⁡x↔w⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
25 24 ralbidv ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→∀x∈N∖Kw⁡i⁡x=u⁡i⁡x↔∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
26 22 25 anbi12d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=u⁡i⁡x↔j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
27 26 ralbidv ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→∀i∈0..^wu⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=u⁡i⁡x↔∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
28 19 27 anbi12d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→w=u∧∀i∈0..^wu⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=u⁡i⁡x↔w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∧∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
29 28 rspcev ⊢j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∈WordR∧w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∧∀i∈0..^wj∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x→∃u∈WordRw=u∧∀i∈0..^wu⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=u⁡i⁡x
30 9 11 17 29 syl12anc ⊢K∈N∧w∈WordT→∃u∈WordRw=u∧∀i∈0..^wu⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=u⁡i⁡x
31 30 ralrimiva ⊢K∈N→∀w∈WordT∃u∈WordRw=u∧∀i∈0..^wu⁡i⁡K=K∧∀x∈N∖Kw⁡i⁡x=u⁡i⁡x