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		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
12	10 11	syl	⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Mnd )
13	2 1 4	symgtrf	⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
14	4 8	gsumwspan	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
15	12 13 14	sylancl	⊢ ( 𝐷 ∈ 𝑉 → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
16	9 15	eqtr3d	⊢ ( 𝐷 ∈ 𝑉 → { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
17	7 16	syl5eq	⊢ ( 𝐷 ∈ 𝑉 → dom 𝑁 = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
18	17	eleq2d	⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ dom 𝑁 ↔ 𝑃 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) )
19		eqid	⊢ ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) = ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) )
20		ovex	⊢ ( 𝐺 Σg 𝑤 ) ∈ V
21	19 20	elrnmpti	⊢ ( 𝑃 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) )
22	18 21	bitrdi	⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ dom 𝑁 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑃 = ( 𝐺 Σg 𝑤 ) ) )