This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) )