Metamath Proof Explorer

Theorem ssnmz

Description: A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
Assertion ssnmz ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑁 )

Proof

Step Hyp Ref Expression
1 elnmz.1 ⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) }
2 nmzsubg.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 nmzsubg.3 ⊢ + = ( +g ‘ 𝐺 )
4 2 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑋 )
5 4 sselda ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑋 )
6 simpll ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
7 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
8 6 7 syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝐺 ∈ Grp )
9 6 4 syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝑆 ⊆ 𝑋 )
10 simplrl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
11 9 10 sseldd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝑧 ∈ 𝑋 )
12 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
14 2 3 12 13 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
15 8 11 14 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
16 15 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) + 𝑤 ) = ( ( 0g ‘ 𝐺 ) + 𝑤 ) )
17 13 subginvcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 )
18 6 10 17 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 )
19 9 18 sseldd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
20 simplrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝑤 ∈ 𝑋 )
21 2 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) + 𝑤 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) )
22 8 19 11 20 21 syl13anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) + 𝑤 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) )
23 2 3 12 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
24 8 20 23 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
25 16 22 24 3eqtr3d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) = 𝑤 )
26 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( 𝑧 + 𝑤 ) ∈ 𝑆 )
27 3 subgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 )
28 6 18 26 27 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) ∈ 𝑆 )
29 25 28 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → 𝑤 ∈ 𝑆 )
30 3 subgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑤 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑤 + 𝑧 ) ∈ 𝑆 )
31 6 29 10 30 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) → ( 𝑤 + 𝑧 ) ∈ 𝑆 )
32 simpll ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
33 simplrl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
34 32 7 syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → 𝐺 ∈ Grp )
35 simplrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → 𝑤 ∈ 𝑋 )
36 32 33 5 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → 𝑧 ∈ 𝑋 )
37 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
38 2 3 37 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑤 + 𝑧 ) ( -g ‘ 𝐺 ) 𝑧 ) = 𝑤 )
39 34 35 36 38 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → ( ( 𝑤 + 𝑧 ) ( -g ‘ 𝐺 ) 𝑧 ) = 𝑤 )
40 simpr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → ( 𝑤 + 𝑧 ) ∈ 𝑆 )
41 37 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑤 + 𝑧 ) ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
42 32 40 33 41 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → ( ( 𝑤 + 𝑧 ) ( -g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
43 39 42 eqeltrrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → 𝑤 ∈ 𝑆 )
44 3 subgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑧 + 𝑤 ) ∈ 𝑆 )
45 32 33 43 44 syl3anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) → ( 𝑧 + 𝑤 ) ∈ 𝑆 )
46 31 45 impbida ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
47 46 anassrs ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
48 47 ralrimiva ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧 ∈ 𝑆 ) → ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
49 1 elnmz ⊢ ( 𝑧 ∈ 𝑁 ↔ ( 𝑧 ∈ 𝑋 ∧ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) )
50 5 48 49 sylanbrc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑁 )
51 50 ex ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑧 ∈ 𝑆 → 𝑧 ∈ 𝑁 ) )
52 51 ssrdv ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑁 )