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

Metamath Proof Explorer

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