Metamath Proof Explorer


Theorem 0nsg

Description: The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis 0nsg.z 0 = ( 0g𝐺 )
Assertion 0nsg ( 𝐺 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 0nsg.z 0 = ( 0g𝐺 )
2 1 0subg ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
3 elsni ( 𝑦 ∈ { 0 } → 𝑦 = 0 )
4 3 ad2antll ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → 𝑦 = 0 )
5 4 oveq2d ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝐺 ) 0 ) )
6 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 eqid ( +g𝐺 ) = ( +g𝐺 )
8 6 7 1 grprid ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g𝐺 ) 0 ) = 𝑥 )
9 8 adantrr ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( 𝑥 ( +g𝐺 ) 0 ) = 𝑥 )
10 5 9 eqtrd ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = 𝑥 )
11 10 oveq1d ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) = ( 𝑥 ( -g𝐺 ) 𝑥 ) )
12 eqid ( -g𝐺 ) = ( -g𝐺 )
13 6 1 12 grpsubid ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( -g𝐺 ) 𝑥 ) = 0 )
14 13 adantrr ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( 𝑥 ( -g𝐺 ) 𝑥 ) = 0 )
15 11 14 eqtrd ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) = 0 )
16 ovex ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ V
17 16 elsn ( ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ { 0 } ↔ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) = 0 )
18 15 17 sylibr ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ { 0 } ) ) → ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ { 0 } )
19 18 ralrimivva ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ { 0 } )
20 6 7 12 isnsg3 ( { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ { 0 } ) )
21 2 19 20 sylanbrc ( 𝐺 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )