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 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
8 6 7 syl ⊢ N ∈ Fin → G ∈ Mnd
9 eqid ⊢ Base G = Base G
10 3 1 9 symgtrf ⊢ T ⊆ Base G
11 9 4 gsumwspan ⊢ G ∈ Mnd ∧ T ⊆ Base G → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
12 8 10 11 sylancl ⊢ N ∈ Fin → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
13 5 12 eqtr3d ⊢ N ∈ Fin → B = ran ⁡ w ∈ Word T ⟼ ∑ G w
14 13 eleq2d ⊢ N ∈ Fin → Q ∈ B ↔ Q ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w
15 eqid ⊢ w ∈ Word T ⟼ ∑ G w = w ∈ Word T ⟼ ∑ G w
16 ovex ⊢ ∑ G w ∈ V
17 15 16 elrnmpti ⊢ Q ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w ↔ ∃ w ∈ Word T Q = ∑ G w
18 14 17 bitrdi ⊢ N ∈ Fin → Q ∈ B ↔ ∃ w ∈ Word T Q = ∑ G w