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

Metamath Proof Explorer

Theorem nsgid

Description: The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis nsgid.z ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion nsgid ( 𝐺 ∈ Grp → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 nsgid.z ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 1 subgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
3 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝐺 ∈ Grp )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 1 4 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
6 simp2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
7 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
8 1 7 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
9 3 5 6 8 syl3anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
10 9 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
11 10 ralrimivva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
12 1 4 7 isnsg3 ⊢ ( 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) )
13 2 11 12 sylanbrc ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )