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 ⊢ P = Base SymGrp ⁡ N
psgnfix.t ⊢ T = ran ⁡ pmTrsp ⁡ N ∖ K
psgnfix.s ⊢ S = SymGrp ⁡ N ∖ K
Assertion psgnfix1 ⊢ N ∈ Fin ∧ K ∈ N → Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word T Q ↾ N ∖ K = ∑ S w

Proof

Step Hyp Ref Expression
1 psgnfix.p ⊢ P = Base SymGrp ⁡ N
2 psgnfix.t ⊢ T = ran ⁡ pmTrsp ⁡ N ∖ K
3 psgnfix.s ⊢ S = SymGrp ⁡ N ∖ K
4 eqid ⊢ q ∈ P | q ⁡ K = K = q ∈ P | q ⁡ K = K
5 3 fveq2i ⊢ Base S = Base SymGrp ⁡ N ∖ K
6 eqid ⊢ N ∖ K = N ∖ K
7 1 4 5 6 symgfixelsi ⊢ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → Q ↾ N ∖ K ∈ Base S
8 7 adantll ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → Q ↾ N ∖ K ∈ Base S
9 diffi ⊢ N ∈ Fin → N ∖ K ∈ Fin
10 9 ad2antrr ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → N ∖ K ∈ Fin
11 eqid ⊢ Base S = Base S
12 3 11 2 psgnfitr ⊢ N ∖ K ∈ Fin → Q ↾ N ∖ K ∈ Base S ↔ ∃ w ∈ Word T Q ↾ N ∖ K = ∑ S w
13 10 12 syl ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → Q ↾ N ∖ K ∈ Base S ↔ ∃ w ∈ Word T Q ↾ N ∖ K = ∑ S w
14 8 13 mpbid ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word T Q ↾ N ∖ K = ∑ S w
15 14 ex ⊢ N ∈ Fin ∧ K ∈ N → Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word T Q ↾ N ∖ K = ∑ S w