Theorem psgnfix1

Description: A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfix.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	psgnfix.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
	psgnfix.s	⊢ 𝑆 = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
Assertion	psgnfix1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnfix.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		psgnfix.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
3		psgnfix.s	⊢ 𝑆 = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
4		eqid	⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
5	3	fveq2i	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
6		eqid	⊢ ( 𝑁 ∖ { 𝐾 } ) = ( 𝑁 ∖ { 𝐾 } )
7	1 4 5 6	symgfixelsi	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ 𝑆 ) )
8	7	adantll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ 𝑆 ) )
9		diffi	⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
10	9	ad2antrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
11		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
12	3 11 2	psgnfitr	⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ 𝑆 ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑤 ) ) )
13	10 12	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ ( Base ‘ 𝑆 ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑤 ) ) )
14	8 13	mpbid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑤 ) )
15	14	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( 𝑆 Σg 𝑤 ) ) )