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 ∈ Word T ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w ∀ 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 1 2 7 pmtrdifwrdellem2 ⊢ w ∈ Word T → w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I
10 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
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 ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x ↔ ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ 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 ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x ↔ w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ∧ ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ 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 ∈ Word R ∧ w = j ∈ 0 ..^ w ⟼ pmTrsp ⁡ N ⁡ dom ⁡ w ⁡ j ∖ I ∧ ∀ i ∈ 0 ..^ w ∀ 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 ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x
19 8 9 10 18 syl12anc ⊢ w ∈ Word T → ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x
20 19 rgen ⊢ ∀ w ∈ Word T ∃ u ∈ Word R w = u ∧ ∀ i ∈ 0 ..^ w ∀ x ∈ N ∖ K w ⁡ i ⁡ x = u ⁡ i ⁡ x