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 ⊢∀w∈WordT∃u∈WordRw=u∧∀i∈0..^w∀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 1 2 7 pmtrdifwrdellem2 ⊢w∈WordT→w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
10 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
11 fveq2 ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
12 11 eqeq2d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→w=u↔w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I
13 fveq1 ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→u⁡i=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i
14 13 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
15 14 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
16 15 2ralbidv ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→∀i∈0..^w∀x∈N∖Kw⁡i⁡x=u⁡i⁡x↔∀i∈0..^w∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
17 12 16 anbi12d ⊢u=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I→w=u∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=u⁡i⁡x↔w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x
18 17 rspcev ⊢j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∈WordR∧w=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=j∈0..^w⟼pmTrsp⁡N⁡dom⁡w⁡j∖I⁡i⁡x→∃u∈WordRw=u∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=u⁡i⁡x
19 8 9 10 18 syl12anc ⊢w∈WordT→∃u∈WordRw=u∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=u⁡i⁡x
20 19 rgen ⊢∀w∈WordT∃u∈WordRw=u∧∀i∈0..^w∀x∈N∖Kw⁡i⁡x=u⁡i⁡x