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 ∈ V → I ↾ A = 0 G

Proof

Step Hyp Ref Expression
1 symggrp.1 ⊢ G = SymGrp ⁡ A
2 eqid ⊢ EndoFMnd ⁡ A = EndoFMnd ⁡ A
3 2 efmndid ⊢ A ∈ V → I ↾ A = 0 EndoFMnd ⁡ A
4 eqid ⊢ Base G = Base G
5 2 1 4 symgsubmefmnd ⊢ A ∈ V → Base G ∈ SubMnd ⁡ EndoFMnd ⁡ A
6 1 4 2 symgressbas ⊢ G = EndoFMnd ⁡ A ↾ 𝑠 Base G
7 eqid ⊢ 0 EndoFMnd ⁡ A = 0 EndoFMnd ⁡ A
8 6 7 subm0 ⊢ Base G ∈ SubMnd ⁡ EndoFMnd ⁡ A → 0 EndoFMnd ⁡ A = 0 G
9 5 8 syl ⊢ A ∈ V → 0 EndoFMnd ⁡ A = 0 G
10 3 9 eqtrd ⊢ A ∈ V → I ↾ A = 0 G