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 𝐺 = ( SymGrp ‘ 𝑁 )
psgnfitr.p 𝐵 = ( Base ‘ 𝐺 )
psgnfitr.t 𝑇 = ran ( pmTrsp ‘ 𝑁 )
Assertion psgnfitr ( 𝑁 ∈ Fin → ( 𝑄𝐵 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 psgnfitr.g 𝐺 = ( SymGrp ‘ 𝑁 )
2 psgnfitr.p 𝐵 = ( Base ‘ 𝐺 )
3 psgnfitr.t 𝑇 = ran ( pmTrsp ‘ 𝑁 )
4 eqid ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
5 3 1 2 4 symggen2 ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = 𝐵 )
6 1 symggrp ( 𝑁 ∈ Fin → 𝐺 ∈ Grp )
7 6 grpmndd ( 𝑁 ∈ Fin → 𝐺 ∈ Mnd )
8 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9 3 1 8 symgtrf 𝑇 ⊆ ( Base ‘ 𝐺 )
10 8 4 gsumwspan ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
11 7 9 10 sylancl ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
12 5 11 eqtr3d ( 𝑁 ∈ Fin → 𝐵 = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
13 12 eleq2d ( 𝑁 ∈ Fin → ( 𝑄𝐵𝑄 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) )
14 eqid ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) = ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) )
15 ovex ( 𝐺 Σg 𝑤 ) ∈ V
16 14 15 elrnmpti ( 𝑄 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) )
17 13 16 bitrdi ( 𝑁 ∈ Fin → ( 𝑄𝐵 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) ) )