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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
isnsg3.2 ⊢ + = ( +g ‘ 𝐺 )
isnsg3.3 ⊢ − = ( -g ‘ 𝐺 )
Assertion nsgconj ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 isnsg3.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 isnsg3.2 ⊢ + = ( +g ‘ 𝐺 )
3 isnsg3.3 ⊢ − = ( -g ‘ 𝐺 )
4 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
5 4 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
6 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 5 6 syl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝐺 ∈ Grp )
8 simp2 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
9 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑋 )
10 5 9 syl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝑆 ⊆ 𝑋 )
11 simp3 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
12 10 11 sseldd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑋 )
13 1 2 3 grpaddsubass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = ( 𝐴 + ( 𝐵 − 𝐴 ) ) )
14 7 8 12 8 13 syl13anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = ( 𝐴 + ( 𝐵 − 𝐴 ) ) )
15 1 2 3 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = 𝐵 )
16 7 12 8 15 syl3anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = 𝐵 )
17 16 11 eqeltrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐵 − 𝐴 ) + 𝐴 ) ∈ 𝑆 )
18 simp1 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )
19 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 − 𝐴 ) ∈ 𝑋 )
20 7 12 8 19 syl3anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 − 𝐴 ) ∈ 𝑋 )
21 1 2 nsgbi ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐵 − 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐵 − 𝐴 ) + 𝐴 ) ∈ 𝑆 ↔ ( 𝐴 + ( 𝐵 − 𝐴 ) ) ∈ 𝑆 ) )
22 18 20 8 21 syl3anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝐵 − 𝐴 ) + 𝐴 ) ∈ 𝑆 ↔ ( 𝐴 + ( 𝐵 − 𝐴 ) ) ∈ 𝑆 ) )
23 17 22 mpbid ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 + ( 𝐵 − 𝐴 ) ) ∈ 𝑆 )
24 14 23 eqeltrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) ∈ 𝑆 )