Metamath Proof Explorer

Theorem psgnfitr

Description: A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfitr.g ⊢ G = SymGrp ⁡ N
psgnfitr.p ⊢ B = Base G
psgnfitr.t ⊢ T = ran ⁡ pmTrsp ⁡ N
Assertion psgnfitr ⊢ N ∈ Fin → Q ∈ B ↔ ∃ w ∈ Word T Q = ∑ G w

Proof

Step Hyp Ref Expression
1 psgnfitr.g ⊢ G = SymGrp ⁡ N
2 psgnfitr.p ⊢ B = Base G
3 psgnfitr.t ⊢ T = ran ⁡ pmTrsp ⁡ N
4 eqid ⊢ mrCls ⁡ SubMnd ⁡ G = mrCls ⁡ SubMnd ⁡ G
5 3 1 2 4 symggen2 ⊢ N ∈ Fin → mrCls ⁡ SubMnd ⁡ G ⁡ T = B
6 1 symggrp ⊢ N ∈ Fin → G ∈ Grp
7 6 grpmndd ⊢ N ∈ Fin → G ∈ Mnd
8 eqid ⊢ Base G = Base G
9 3 1 8 symgtrf ⊢ T ⊆ Base G
10 8 4 gsumwspan ⊢ G ∈ Mnd ∧ T ⊆ Base G → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
11 7 9 10 sylancl ⊢ N ∈ Fin → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
12 5 11 eqtr3d ⊢ N ∈ Fin → B = ran ⁡ w ∈ Word T ⟼ ∑ G w
13 12 eleq2d ⊢ N ∈ Fin → Q ∈ B ↔ Q ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w
14 eqid ⊢ w ∈ Word T ⟼ ∑ G w = w ∈ Word T ⟼ ∑ G w
15 ovex ⊢ ∑ G w ∈ V
16 14 15 elrnmpti ⊢ Q ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w ↔ ∃ w ∈ Word T Q = ∑ G w
17 13 16 bitrdi ⊢ N ∈ Fin → Q ∈ B ↔ ∃ w ∈ Word T Q = ∑ G w