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 ⊢G=SymGrp⁡D
psgnval.t ⊢T=ran⁡pmTrsp⁡D
psgnval.n ⊢N=pmSgn⁡D
Assertion psgneldm2 ⊢D∈V→P∈dom⁡N↔∃w∈WordTP=∑Gw

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢G=SymGrp⁡D
2 psgnval.t ⊢T=ran⁡pmTrsp⁡D
3 psgnval.n ⊢N=pmSgn⁡D
4 eqid ⊢BaseG=BaseG
5 eqid ⊢p∈BaseG|dom⁡p∖I∈Fin=p∈BaseG|dom⁡p∖I∈Fin
6 1 4 5 3 psgnfn ⊢NFnp∈BaseG|dom⁡p∖I∈Fin
7 6 fndmi ⊢dom⁡N=p∈BaseG|dom⁡p∖I∈Fin
8 eqid ⊢mrCls⁡SubMnd⁡G=mrCls⁡SubMnd⁡G
9 2 1 4 8 symggen ⊢D∈V→mrCls⁡SubMnd⁡G⁡T=p∈BaseG|dom⁡p∖I∈Fin
10 1 symggrp ⊢D∈V→G∈Grp
11 10 grpmndd ⊢D∈V→G∈Mnd
12 2 1 4 symgtrf ⊢T⊆BaseG
13 4 8 gsumwspan ⊢G∈Mnd∧T⊆BaseG→mrCls⁡SubMnd⁡G⁡T=ran⁡w∈WordT⟼∑Gw
14 11 12 13 sylancl ⊢D∈V→mrCls⁡SubMnd⁡G⁡T=ran⁡w∈WordT⟼∑Gw
15 9 14 eqtr3d ⊢D∈V→p∈BaseG|dom⁡p∖I∈Fin=ran⁡w∈WordT⟼∑Gw
16 7 15 eqtrid ⊢D∈V→dom⁡N=ran⁡w∈WordT⟼∑Gw
17 16 eleq2d ⊢D∈V→P∈dom⁡N↔P∈ran⁡w∈WordT⟼∑Gw
18 eqid ⊢w∈WordT⟼∑Gw=w∈WordT⟼∑Gw
19 ovex ⊢∑Gw∈V
20 18 19 elrnmpti ⊢P∈ran⁡w∈WordT⟼∑Gw↔∃w∈WordTP=∑Gw
21 17 20 bitrdi ⊢D∈V→P∈dom⁡N↔∃w∈WordTP=∑Gw