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 ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
Assertion pmtrdifwrdel ∀ 𝑤 ∈ Word 𝑇 ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 pmtrdifel.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2 pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3 fveq2 ⊢ ( 𝑗 = 𝑛 → ( 𝑤 ‘ 𝑗 ) = ( 𝑤 ‘ 𝑛 ) )
4 3 difeq1d ⊢ ( 𝑗 = 𝑛 → ( ( 𝑤 ‘ 𝑗 ) ∖ I ) = ( ( 𝑤 ‘ 𝑛 ) ∖ I ) )
5 4 dmeqd ⊢ ( 𝑗 = 𝑛 → dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) = dom ( ( 𝑤 ‘ 𝑛 ) ∖ I ) )
6 5 fveq2d ⊢ ( 𝑗 = 𝑛 → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑛 ) ∖ I ) ) )
7 6 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑛 ) ∖ I ) ) )
8 1 2 7 pmtrdifwrdellem1 ⊢ ( 𝑤 ∈ Word 𝑇 → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ∈ Word 𝑅 )
9 1 2 7 pmtrdifwrdellem2 ⊢ ( 𝑤 ∈ Word 𝑇 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
10 1 2 7 pmtrdifwrdellem3 ⊢ ( 𝑤 ∈ Word 𝑇 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) )
11 fveq2 ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
12 11 eqeq2d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) ) )
13 fveq1 ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( 𝑢 ‘ 𝑖 ) = ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) )
14 13 fveq1d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) )
15 14 eqeq2d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ↔ ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
16 15 2ralbidv ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
17 12 16 anbi12d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
18 17 rspcev ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) → ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) )
19 8 9 10 18 syl12anc ⊢ ( 𝑤 ∈ Word 𝑇 → ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) )
20 19 rgen ⊢ ∀ 𝑤 ∈ Word 𝑇 ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) )