Theorem psgnfix2

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

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

Proof

Step	Hyp	Ref	Expression
1		psgnfix.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		psgnfix.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
3		psgnfix.s	⊢ 𝑆 = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
4		psgnfix.z	⊢ 𝑍 = ( SymGrp ‘ 𝑁 )
5		psgnfix.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
6		elrabi	⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → 𝑄 ∈ 𝑃 )
7	6	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → 𝑄 ∈ 𝑃 )
8	4	fveq2i	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
9	1 8	eqtr4i	⊢ 𝑃 = ( Base ‘ 𝑍 )
10	4 9 5	psgnfitr	⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝑃 ↔ ∃ 𝑤 ∈ Word 𝑅 𝑄 = ( 𝑍 Σg 𝑤 ) ) )
11	10	bicomd	⊢ ( 𝑁 ∈ Fin → ( ∃ 𝑤 ∈ Word 𝑅 𝑄 = ( 𝑍 Σg 𝑤 ) ↔ 𝑄 ∈ 𝑃 ) )
12	11	ad2antrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ∃ 𝑤 ∈ Word 𝑅 𝑄 = ( 𝑍 Σg 𝑤 ) ↔ 𝑄 ∈ 𝑃 ) )
13	7 12	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ∃ 𝑤 ∈ Word 𝑅 𝑄 = ( 𝑍 Σg 𝑤 ) )
14	13	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ∃ 𝑤 ∈ Word 𝑅 𝑄 = ( 𝑍 Σg 𝑤 ) ) )