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 e. V -> ( P e. dom N <-> E. w e. Word T P = ( G gsum w ) ) )

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	|- ( Base ` G ) = ( Base ` G )
5		eqid	|- { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin }
6	1 4 5 3	psgnfn	|- N Fn { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin }
7	6	fndmi	|- dom N = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin }
8		eqid	|- ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) )
9	2 1 4 8	symggen	|- ( D e. V -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } )
10	1	symggrp	|- ( D e. V -> G e. Grp )
11	10	grpmndd	|- ( D e. V -> G e. Mnd )
12	2 1 4	symgtrf	|- T C_ ( Base ` G )
13	4 8	gsumwspan	|- ( ( G e. Mnd /\ T C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
14	11 12 13	sylancl	|- ( D e. V -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
15	9 14	eqtr3d	|- ( D e. V -> { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } = ran ( w e. Word T |-> ( G gsum w ) ) )
16	7 15	eqtrid	|- ( D e. V -> dom N = ran ( w e. Word T |-> ( G gsum w ) ) )
17	16	eleq2d	|- ( D e. V -> ( P e. dom N <-> P e. ran ( w e. Word T |-> ( G gsum w ) ) ) )
18		eqid	|- ( w e. Word T |-> ( G gsum w ) ) = ( w e. Word T |-> ( G gsum w ) )
19		ovex	|- ( G gsum w ) e. _V
20	18 19	elrnmpti	|- ( P e. ran ( w e. Word T |-> ( G gsum w ) ) <-> E. w e. Word T P = ( G gsum w ) )
21	17 20	bitrdi	|- ( D e. V -> ( P e. dom N <-> E. w e. Word T P = ( G gsum w ) ) )