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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion	symgid	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		eqid	⊢ ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ 𝐴 )
3	2	efmndid	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ ( EndoFMnd ‘ 𝐴 ) ) )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	2 1 4	symgsubmefmnd	⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐺 ) ∈ ( SubMnd ‘ ( EndoFMnd ‘ 𝐴 ) ) )
6	1 4 2	symgressbas	⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s ( Base ‘ 𝐺 ) )
7		eqid	⊢ ( 0g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( 0g ‘ ( EndoFMnd ‘ 𝐴 ) )
8	6 7	subm0	⊢ ( ( Base ‘ 𝐺 ) ∈ ( SubMnd ‘ ( EndoFMnd ‘ 𝐴 ) ) → ( 0g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
9	5 8	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 0g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
10	3 9	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝐺 ) )