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 ⊢ P = Base SymGrp ⁡ N
psgnfix.t ⊢ T = ran ⁡ pmTrsp ⁡ N ∖ K
psgnfix.s ⊢ S = SymGrp ⁡ N ∖ K
psgnfix.z ⊢ Z = SymGrp ⁡ N
psgnfix.r ⊢ R = ran ⁡ pmTrsp ⁡ N
Assertion psgnfix2 ⊢ N ∈ Fin ∧ K ∈ N → Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word R Q = ∑ Z 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 psgnfix.z ⊢ Z = SymGrp ⁡ N
5 psgnfix.r ⊢ R = ran ⁡ pmTrsp ⁡ N
6 elrabi ⊢ Q ∈ q ∈ P | q ⁡ K = K → Q ∈ P
7 6 adantl ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → Q ∈ P
8 4 fveq2i ⊢ Base Z = Base SymGrp ⁡ N
9 1 8 eqtr4i ⊢ P = Base Z
10 4 9 5 psgnfitr ⊢ N ∈ Fin → Q ∈ P ↔ ∃ w ∈ Word R Q = ∑ Z w
11 10 bicomd ⊢ N ∈ Fin → ∃ w ∈ Word R Q = ∑ Z w ↔ Q ∈ P
12 11 ad2antrr ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word R Q = ∑ Z w ↔ Q ∈ P
13 7 12 mpbird ⊢ N ∈ Fin ∧ K ∈ N ∧ Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word R Q = ∑ Z w
14 13 ex ⊢ N ∈ Fin ∧ K ∈ N → Q ∈ q ∈ P | q ⁡ K = K → ∃ w ∈ Word R Q = ∑ Z w