This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑤 ) ) )