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 
|- B = ( Base ` G )
Assertion nsgid 
|- ( G e. Grp -> B e. ( NrmSGrp ` G ) )

Proof

Step Hyp Ref Expression
1 nsgid.z 
 |-  B = ( Base ` G )
2 1 subgid 
 |-  ( G e. Grp -> B e. ( SubGrp ` G ) )
3 simp1 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> G e. Grp )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 1 4 grpcl 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
6 simp2 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> x e. B )
7 eqid 
 |-  ( -g ` G ) = ( -g ` G )
8 1 7 grpsubcl 
 |-  ( ( G e. Grp /\ ( x ( +g ` G ) y ) e. B /\ x e. B ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
9 3 5 6 8 syl3anc 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
10 9 3expb 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
11 10 ralrimivva 
 |-  ( G e. Grp -> A. x e. B A. y e. B ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B )
12 1 4 7 isnsg3 
 |-  ( B e. ( NrmSGrp ` G ) <-> ( B e. ( SubGrp ` G ) /\ A. x e. B A. y e. B ( ( x ( +g ` G ) y ) ( -g ` G ) x ) e. B ) )
13 2 11 12 sylanbrc 
 |-  ( G e. Grp -> B e. ( NrmSGrp ` G ) )