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 ⊢ 𝐺 = ( 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 ‘ 𝐺 ) )