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

Metamath Proof Explorer

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 𝑤 ) ) )