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 ..^ ( ♯ ‘ 𝑤 ) ) ( ( ( 𝑢 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑥 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑥 ) ) ) )