Metamath Proof Explorer

Theorem qus0g

Description: The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypothesis qus0g.1 ⊢ Q = G / 𝑠 G ~ QG N
Assertion qus0g ⊢ N ∈ NrmSGrp ⁡ G → 0 Q = N

Proof

Step Hyp Ref Expression
1 qus0g.1 ⊢ Q = G / 𝑠 G ~ QG N
2 eqid ⊢ Base G = Base G
3 eqid ⊢ LSSum ⁡ G = LSSum ⁡ G
4 nsgsubg ⊢ N ∈ NrmSGrp ⁡ G → N ∈ SubGrp ⁡ G
5 subgrcl ⊢ N ∈ SubGrp ⁡ G → G ∈ Grp
6 eqid ⊢ 0 G = 0 G
7 2 6 grpidcl ⊢ G ∈ Grp → 0 G ∈ Base G
8 4 5 7 3syl ⊢ N ∈ NrmSGrp ⁡ G → 0 G ∈ Base G
9 2 3 4 8 quslsm ⊢ N ∈ NrmSGrp ⁡ G → 0 G G ~ QG N = 0 G LSSum ⁡ G N
10 1 6 qus0 ⊢ N ∈ NrmSGrp ⁡ G → 0 G G ~ QG N = 0 Q
11 6 3 lsm02 ⊢ N ∈ SubGrp ⁡ G → 0 G LSSum ⁡ G N = N
12 4 11 syl ⊢ N ∈ NrmSGrp ⁡ G → 0 G LSSum ⁡ G N = N
13 9 10 12 3eqtr3d ⊢ N ∈ NrmSGrp ⁡ G → 0 Q = N