Metamath Proof Explorer

Theorem nsgconj

Description: The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypotheses isnsg3.1 
|- X = ( Base ` G )
isnsg3.2 
|- .+ = ( +g ` G )
isnsg3.3 
|- .- = ( -g ` G )
Assertion nsgconj 
|- ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( A .+ B ) .- A ) e. S )

Proof

Step Hyp Ref Expression
1 isnsg3.1 
 |-  X = ( Base ` G )
2 isnsg3.2 
 |-  .+ = ( +g ` G )
3 isnsg3.3 
 |-  .- = ( -g ` G )
4 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
5 4 3ad2ant1 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> S e. ( SubGrp ` G ) )
6 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
7 5 6 syl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> G e. Grp )
8 simp2 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> A e. X )
9 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
10 5 9 syl 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> S C_ X )
11 simp3 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> B e. S )
12 10 11 sseldd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> B e. X )
13 1 2 3 grpaddsubass 
 |-  ( ( G e. Grp /\ ( A e. X /\ B e. X /\ A e. X ) ) -> ( ( A .+ B ) .- A ) = ( A .+ ( B .- A ) ) )
14 7 8 12 8 13 syl13anc 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( A .+ B ) .- A ) = ( A .+ ( B .- A ) ) )
15 1 2 3 grpnpcan 
 |-  ( ( G e. Grp /\ B e. X /\ A e. X ) -> ( ( B .- A ) .+ A ) = B )
16 7 12 8 15 syl3anc 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( B .- A ) .+ A ) = B )
17 16 11 eqeltrd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( B .- A ) .+ A ) e. S )
18 simp1 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> S e. ( NrmSGrp ` G ) )
19 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ B e. X /\ A e. X ) -> ( B .- A ) e. X )
20 7 12 8 19 syl3anc 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( B .- A ) e. X )
21 1 2 nsgbi 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ ( B .- A ) e. X /\ A e. X ) -> ( ( ( B .- A ) .+ A ) e. S <-> ( A .+ ( B .- A ) ) e. S ) )
22 18 20 8 21 syl3anc 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( ( B .- A ) .+ A ) e. S <-> ( A .+ ( B .- A ) ) e. S ) )
23 17 22 mpbid 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( A .+ ( B .- A ) ) e. S )
24 14 23 eqeltrd 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ A e. X /\ B e. S ) -> ( ( A .+ B ) .- A ) e. S )