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