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

Metamath Proof Explorer

Theorem psgneldm2

Description: The finitary permutations are the span of the transpositions. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgneldm2 ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ dom 𝑁 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnval.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnval.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 eqid ⊢ { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
6 1 4 5 3 psgnfn ⊢ 𝑁 Fn { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
7 6 fndmi ⊢ dom 𝑁 = { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
8 eqid ⊢ ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
9 2 1 4 8 symggen ⊢ ( 𝐷 ∈ 𝑉 → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
10 1 symggrp ⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Grp )
11 10 grpmndd ⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Mnd )
12 2 1 4 symgtrf ⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
13 4 8 gsumwspan ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
14 11 12 13 sylancl ⊢ ( 𝐷 ∈ 𝑉 → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
15 9 14 eqtr3d ⊢ ( 𝐷 ∈ 𝑉 → { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
16 7 15 eqtrid ⊢ ( 𝐷 ∈ 𝑉 → dom 𝑁 = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
17 16 eleq2d ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ dom 𝑁 ↔ 𝑃 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) )
18 eqid ⊢ ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) = ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) )
19 ovex ⊢ ( 𝐺 Σg 𝑤 ) ∈ V
20 18 19 elrnmpti ⊢ ( 𝑃 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) )
21 17 20 bitrdi ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ dom 𝑁 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) ) )