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 ) )