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

Metamath Proof Explorer

Theorem symgid

Description: The group identity element of the symmetric group on a set A . (Contributed by Paul Chapman, 25-Jul-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 1-Apr-2024)

Ref Expression
Hypothesis symggrp.1 
|- G = ( SymGrp ` A )
Assertion symgid 
|- ( A e. V -> ( _I |` A ) = ( 0g ` G ) )

Proof

Step Hyp Ref Expression
1 symggrp.1 
 |-  G = ( SymGrp ` A )
2 eqid 
 |-  ( EndoFMnd ` A ) = ( EndoFMnd ` A )
3 2 efmndid 
 |-  ( A e. V -> ( _I |` A ) = ( 0g ` ( EndoFMnd ` A ) ) )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 2 1 4 symgsubmefmnd 
 |-  ( A e. V -> ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) )
6 1 4 2 symgressbas 
 |-  G = ( ( EndoFMnd ` A ) |`s ( Base ` G ) )
7 eqid 
 |-  ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` ( EndoFMnd ` A ) )
8 6 7 subm0 
 |-  ( ( Base ` G ) e. ( SubMnd ` ( EndoFMnd ` A ) ) -> ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` G ) )
9 5 8 syl 
 |-  ( A e. V -> ( 0g ` ( EndoFMnd ` A ) ) = ( 0g ` G ) )
10 3 9 eqtrd 
 |-  ( A e. V -> ( _I |` A ) = ( 0g ` G ) )