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 ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
Assertion nsgqus0 ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 nsgqus0.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
2 simpl ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
3 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
6 4 5 lsm02 ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) = 𝑁 )
7 2 3 6 3syl ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) = 𝑁 )
8 1 4 qus0 ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( 0g ‘ 𝑄 ) )
9 8 adantr ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( 0g ‘ 𝑄 ) )
10 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 3 adantr ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
12 subgrcl ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
13 3 12 syl ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
14 13 adantr ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝐺 ∈ Grp )
15 10 4 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
16 14 15 syl ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
17 10 5 11 16 quslsm ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) )
18 9 17 eqtr3d ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → ( 0g ‘ 𝑄 ) = ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) )
19 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
20 19 subg0cl ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝑄 ) → ( 0g ‘ 𝑄 ) ∈ 𝐹 )
21 20 adantl ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → ( 0g ‘ 𝑄 ) ∈ 𝐹 )
22 18 21 eqeltrrd ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → ( { ( 0g ‘ 𝐺 ) } ( LSSum ‘ 𝐺 ) 𝑁 ) ∈ 𝐹 )
23 7 22 eqeltrrd ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ 𝐹 )