Metamath Proof Explorer

Theorem nsgqus0

Description: A normal subgroup N is a member of all subgroups F of the quotient group by N . In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypothesis nsgqus0.q ⊢ Q = G / 𝑠 G ~ QG N
Assertion nsgqus0 ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → N ∈ F

Proof

Step Hyp Ref Expression
1 nsgqus0.q ⊢ Q = G / 𝑠 G ~ QG N
2 simpl ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → N ∈ NrmSGrp ⁡ G
3 nsgsubg ⊢ N ∈ NrmSGrp ⁡ G → N ∈ SubGrp ⁡ G
4 eqid ⊢ 0 G = 0 G
5 eqid ⊢ LSSum ⁡ G = LSSum ⁡ G
6 4 5 lsm02 ⊢ N ∈ SubGrp ⁡ G → 0 G LSSum ⁡ G N = N
7 2 3 6 3syl ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 G LSSum ⁡ G N = N
8 1 4 qus0 ⊢ N ∈ NrmSGrp ⁡ G → 0 G G ~ QG N = 0 Q
9 8 adantr ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 G G ~ QG N = 0 Q
10 eqid ⊢ Base G = Base G
11 3 adantr ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → N ∈ SubGrp ⁡ G
12 subgrcl ⊢ N ∈ SubGrp ⁡ G → G ∈ Grp
13 3 12 syl ⊢ N ∈ NrmSGrp ⁡ G → G ∈ Grp
14 13 adantr ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → G ∈ Grp
15 10 4 grpidcl ⊢ G ∈ Grp → 0 G ∈ Base G
16 14 15 syl ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 G ∈ Base G
17 10 5 11 16 quslsm ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 G G ~ QG N = 0 G LSSum ⁡ G N
18 9 17 eqtr3d ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 Q = 0 G LSSum ⁡ G N
19 eqid ⊢ 0 Q = 0 Q
20 19 subg0cl ⊢ F ∈ SubGrp ⁡ Q → 0 Q ∈ F
21 20 adantl ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 Q ∈ F
22 18 21 eqeltrrd ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → 0 G LSSum ⁡ G N ∈ F
23 7 22 eqeltrrd ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → N ∈ F