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=\mathrm{SymGrp}\left(A\right)$$
Assertion	symgid	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_G$$

Proof

Step	Hyp	Ref	Expression
1		symggrp.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		eqid	$$⊢\mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(A\right)$$
3	2	efmndid	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_{\mathrm{EndoFMnd}\left(A\right)}$$
4		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
5	2 1 4	symgsubmefmnd	$$⊢A\in V\to {\mathrm{Base}}_G\in \mathrm{SubMnd}\left(\mathrm{EndoFMnd}\left(A\right)\right)$$
6	1 4 2	symgressbas	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_G$$
7		eqid	$$⊢0_{\mathrm{EndoFMnd}\left(A\right)}=0_{\mathrm{EndoFMnd}\left(A\right)}$$
8	6 7	subm0	$$⊢{\mathrm{Base}}_G\in \mathrm{SubMnd}\left(\mathrm{EndoFMnd}\left(A\right)\right)\to 0_{\mathrm{EndoFMnd}\left(A\right)}=0_G$$
9	5 8	syl	$$⊢A\in V\to 0_{\mathrm{EndoFMnd}\left(A\right)}=0_G$$
10	3 9	eqtrd	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_G$$