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 ∈ Word T ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w u ⁡ i ⁡ K = K ∧ ∀ x ∈ 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 ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I = n ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ n ∖ I
8 1 2 7 pmtrdifwrdellem1 ⊢ w ∈ Word T → j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ∈ Word R
9 8 adantl ⊢ K ∈ N ∧ w ∈ Word T → j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ∈ Word R
10 1 2 7 pmtrdifwrdellem2 ⊢ w ∈ Word T → w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I
11 10 adantl ⊢ K ∈ N ∧ w ∈ Word T → w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I
12 1 2 7 pmtrdifwrdel2lem1 ⊢ w ∈ Word T ∧ K ∈ N → ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K
13 12 ancoms ⊢ K ∈ N ∧ w ∈ Word T → ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K
14 1 2 7 pmtrdifwrdellem3 ⊢ w ∈ Word T → ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ i ⁡ x = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ x
15 14 adantl ⊢ K ∈ N ∧ w ∈ Word T → ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ i ⁡ x = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ x
16 r19.26 ⊢ ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ x ↔ ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ i ⁡ x = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ x
17 13 15 16 sylanbrc ⊢ K ∈ N ∧ w ∈ Word T → ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ 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 ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x ↔ ∀ x ∈ N ∖ K w ⁡ 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 ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x ↔ j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ 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 ..^ w u ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x ↔ ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ 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 ..^ w u ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x ↔ w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ∧ ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ 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 ∈ Word R ∧ w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ∧ ∀ i ∈ 0 ..^ w j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ⁡ i ⁡ x → ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w u ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x
30 9 11 17 29 syl12anc ⊢ K ∈ N ∧ w ∈ Word T → ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w u ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x
31 30 ralrimiva ⊢ K ∈ N → ∀ w ∈ Word T ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w u ⁡ i ⁡ K = K ∧ ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x