This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
Assertion pmtrdifwrdel2 ( 𝐾 ∈ 𝑁 → ∀ 𝑤 ∈ 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 8 adantl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ∈ Word 𝑅 )
10 1 2 7 pmtrdifwrdellem2 ⊢ ( 𝑤 ∈ Word 𝑇 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
11 10 adantl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
12 1 2 7 pmtrdifwrdel2lem1 ⊢ ( ( 𝑤 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
13 12 ancoms ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 )
14 1 2 7 pmtrdifwrdellem3 ⊢ ( 𝑤 ∈ Word 𝑇 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) )
15 14 adantl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) )
16 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
17 13 15 16 sylanbrc ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
18 fveq2 ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) )
19 18 eqeq2d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) ) )
20 fveq1 ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( 𝑢 ‘ 𝑖 ) = ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) )
21 20 fveq1d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) )
22 21 eqeq1d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
23 20 fveq1d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) )
24 23 eqeq2d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ↔ ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
25 24 ralbidv ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
26 22 25 anbi12d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ↔ ( ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
27 26 ralbidv ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
28 19 27 anbi12d ⊢ ( 𝑢 = ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) → ( ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ) ↔ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) ) )
29 28 rspcev ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ∈ Word 𝑅 ∧ ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( ( 𝑤 ‘ 𝑗 ) ∖ I ) ) ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) ) → ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
30 9 11 17 29 syl12anc ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑤 ∈ Word 𝑇 ) → ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )
31 30 ralrimiva ⊢ ( 𝐾 ∈ 𝑁 → ∀ 𝑤 ∈ Word 𝑇 ∃ 𝑢 ∈ Word 𝑅 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )