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

Metamath Proof Explorer

Theorem psgnfitr

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

Ref Expression
Hypotheses psgnfitr.g 
|- G = ( SymGrp ` N )
psgnfitr.p 
|- B = ( Base ` G )
psgnfitr.t 
|- T = ran ( pmTrsp ` N )
Assertion psgnfitr 
|- ( N e. Fin -> ( Q e. B <-> E. w e. Word T Q = ( G gsum w ) ) )

Proof

Step Hyp Ref Expression
1 psgnfitr.g 
 |-  G = ( SymGrp ` N )
2 psgnfitr.p 
 |-  B = ( Base ` G )
3 psgnfitr.t 
 |-  T = ran ( pmTrsp ` N )
4 eqid 
 |-  ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) )
5 3 1 2 4 symggen2 
 |-  ( N e. Fin -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = B )
6 1 symggrp 
 |-  ( N e. Fin -> G e. Grp )
7 6 grpmndd 
 |-  ( N e. Fin -> G e. Mnd )
8 eqid 
 |-  ( Base ` G ) = ( Base ` G )
9 3 1 8 symgtrf 
 |-  T C_ ( Base ` G )
10 8 4 gsumwspan 
 |-  ( ( G e. Mnd /\ T C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
11 7 9 10 sylancl 
 |-  ( N e. Fin -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) )
12 5 11 eqtr3d 
 |-  ( N e. Fin -> B = ran ( w e. Word T |-> ( G gsum w ) ) )
13 12 eleq2d 
 |-  ( N e. Fin -> ( Q e. B <-> Q e. ran ( w e. Word T |-> ( G gsum w ) ) ) )
14 eqid 
 |-  ( w e. Word T |-> ( G gsum w ) ) = ( w e. Word T |-> ( G gsum w ) )
15 ovex 
 |-  ( G gsum w ) e. _V
16 14 15 elrnmpti 
 |-  ( Q e. ran ( w e. Word T |-> ( G gsum w ) ) <-> E. w e. Word T Q = ( G gsum w ) )
17 13 16 bitrdi 
 |-  ( N e. Fin -> ( Q e. B <-> E. w e. Word T Q = ( G gsum w ) ) )