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 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
idrespermg.e ⊢ 𝐸 = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
Assertion idrespermg ( 𝐴 ∈ 𝑉 → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 idressubgsymg.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 idrespermg.e ⊢ 𝐸 = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
3 1 idressubgsymg ⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 1 4 pgrpsubgsymgbi ⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) ↔ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) ) )
6 snex ⊢ { ( I ↾ 𝐴 ) } ∈ V
7 2 4 ressbas ⊢ ( { ( I ↾ 𝐴 ) } ∈ V → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
8 6 7 mp1i ⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
9 inss2 ⊢ ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) ⊆ ( Base ‘ 𝐺 )
10 8 9 eqsstrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) )
11 2 eqcomi ⊢ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) = 𝐸
12 11 eleq1i ⊢ ( ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ↔ 𝐸 ∈ Grp )
13 12 biimpi ⊢ ( ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp → 𝐸 ∈ Grp )
14 13 adantl ⊢ ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) → 𝐸 ∈ Grp )
15 10 14 anim12ci ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) ) → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )
16 15 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
17 5 16 sylbid ⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
18 3 17 mpd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )