This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symggen2

Description: A finite permutation group is generated by the transpositions, see also Theorem 3.4 in Rotman p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses symgtrf.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
symgtrf.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
symgtrf.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
symggen.k ⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
Assertion symggen2 ( 𝐷 ∈ Fin → ( 𝐾 ‘ 𝑇 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 symgtrf.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
2 symgtrf.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3 symgtrf.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 symggen.k ⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
5 1 2 3 4 symggen ⊢ ( 𝐷 ∈ Fin → ( 𝐾 ‘ 𝑇 ) = { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
6 difss ⊢ ( 𝑥 ∖ I ) ⊆ 𝑥
7 dmss ⊢ ( ( 𝑥 ∖ I ) ⊆ 𝑥 → dom ( 𝑥 ∖ I ) ⊆ dom 𝑥 )
8 6 7 ax-mp ⊢ dom ( 𝑥 ∖ I ) ⊆ dom 𝑥
9 2 3 symgbasf1o ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 : 𝐷 –1-1-onto→ 𝐷 )
10 f1odm ⊢ ( 𝑥 : 𝐷 –1-1-onto→ 𝐷 → dom 𝑥 = 𝐷 )
11 9 10 syl ⊢ ( 𝑥 ∈ 𝐵 → dom 𝑥 = 𝐷 )
12 8 11 sseqtrid ⊢ ( 𝑥 ∈ 𝐵 → dom ( 𝑥 ∖ I ) ⊆ 𝐷 )
13 ssfi ⊢ ( ( 𝐷 ∈ Fin ∧ dom ( 𝑥 ∖ I ) ⊆ 𝐷 ) → dom ( 𝑥 ∖ I ) ∈ Fin )
14 12 13 sylan2 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → dom ( 𝑥 ∖ I ) ∈ Fin )
15 14 ralrimiva ⊢ ( 𝐷 ∈ Fin → ∀ 𝑥 ∈ 𝐵 dom ( 𝑥 ∖ I ) ∈ Fin )
16 rabid2 ⊢ ( 𝐵 = { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ↔ ∀ 𝑥 ∈ 𝐵 dom ( 𝑥 ∖ I ) ∈ Fin )
17 15 16 sylibr ⊢ ( 𝐷 ∈ Fin → 𝐵 = { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
18 5 17 eqtr4d ⊢ ( 𝐷 ∈ Fin → ( 𝐾 ‘ 𝑇 ) = 𝐵 )