Theorem psgnfitr

Description: A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfitr.g	⊢ 𝐺 = ( SymGrp ‘ 𝑁 )
	psgnfitr.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
	psgnfitr.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 )
Assertion	psgnfitr	⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝐵 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnfitr.g	⊢ 𝐺 = ( SymGrp ‘ 𝑁 )
2		psgnfitr.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		psgnfitr.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 )
4		eqid	⊢ ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
5	3 1 2 4	symggen2	⊢ ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = 𝐵 )
6	1	symggrp	⊢ ( 𝑁 ∈ Fin → 𝐺 ∈ Grp )
7		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
8	6 7	syl	⊢ ( 𝑁 ∈ Fin → 𝐺 ∈ Mnd )
9		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10	3 1 9	symgtrf	⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
11	9 4	gsumwspan	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
12	8 10 11	sylancl	⊢ ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
13	5 12	eqtr3d	⊢ ( 𝑁 ∈ Fin → 𝐵 = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) )
14	13	eleq2d	⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝐵 ↔ 𝑄 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) )
15		eqid	⊢ ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) = ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) )
16		ovex	⊢ ( 𝐺 Σg 𝑤 ) ∈ V
17	15 16	elrnmpti	⊢ ( 𝑄 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) )
18	14 17	bitrdi	⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝐵 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) ) )