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

Metamath Proof Explorer

Theorem idrespermg

Description: The structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation (constructed by (structure) restricting the symmetric group to that singleton) is a permutation group (group consisting of permutations). (Contributed by AV, 17-Mar-2019)

Ref Expression
Hypotheses idressubgsymg.g 
|- G = ( SymGrp ` A )
idrespermg.e 
|- E = ( G |`s { ( _I |` A ) } )
Assertion idrespermg 
|- ( A e. V -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )

Proof

Step Hyp Ref Expression
1 idressubgsymg.g 
 |-  G = ( SymGrp ` A )
2 idrespermg.e 
 |-  E = ( G |`s { ( _I |` A ) } )
3 1 idressubgsymg 
 |-  ( A e. V -> { ( _I |` A ) } e. ( SubGrp ` G ) )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 1 4 pgrpsubgsymgbi 
 |-  ( A e. V -> ( { ( _I |` A ) } e. ( SubGrp ` G ) <-> ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) ) )
6 snex 
 |-  { ( _I |` A ) } e. _V
7 2 4 ressbas 
 |-  ( { ( _I |` A ) } e. _V -> ( { ( _I |` A ) } i^i ( Base ` G ) ) = ( Base ` E ) )
8 6 7 mp1i 
 |-  ( A e. V -> ( { ( _I |` A ) } i^i ( Base ` G ) ) = ( Base ` E ) )
9 inss2 
 |-  ( { ( _I |` A ) } i^i ( Base ` G ) ) C_ ( Base ` G )
10 8 9 eqsstrrdi 
 |-  ( A e. V -> ( Base ` E ) C_ ( Base ` G ) )
11 2 eqcomi 
 |-  ( G |`s { ( _I |` A ) } ) = E
12 11 eleq1i 
 |-  ( ( G |`s { ( _I |` A ) } ) e. Grp <-> E e. Grp )
13 12 biimpi 
 |-  ( ( G |`s { ( _I |` A ) } ) e. Grp -> E e. Grp )
14 13 adantl 
 |-  ( ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) -> E e. Grp )
15 10 14 anim12ci 
 |-  ( ( A e. V /\ ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) ) -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )
16 15 ex 
 |-  ( A e. V -> ( ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) ) )
17 5 16 sylbid 
 |-  ( A e. V -> ( { ( _I |` A ) } e. ( SubGrp ` G ) -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) ) )
18 3 17 mpd 
 |-  ( A e. V -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )