Metamath Proof Explorer

Theorem cntrnsg

Description: The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypothesis cntrnsg.z ⊢ Z = Cntr ⁡ M
Assertion cntrnsg ⊢ M ∈ Grp → Z ∈ NrmSGrp ⁡ M

Proof

Step Hyp Ref Expression
1 cntrnsg.z ⊢ Z = Cntr ⁡ M
2 eqid ⊢ Base M = Base M
3 eqid ⊢ Cntz ⁡ M = Cntz ⁡ M
4 2 3 cntrval ⊢ Cntz ⁡ M ⁡ Base M = Cntr ⁡ M
5 1 4 eqtr4i ⊢ Z = Cntz ⁡ M ⁡ Base M
6 ssid ⊢ Base M ⊆ Base M
7 2 3 cntzsubg ⊢ M ∈ Grp ∧ Base M ⊆ Base M → Cntz ⁡ M ⁡ Base M ∈ SubGrp ⁡ M
8 6 7 mpan2 ⊢ M ∈ Grp → Cntz ⁡ M ⁡ Base M ∈ SubGrp ⁡ M
9 5 8 eqeltrid ⊢ M ∈ Grp → Z ∈ SubGrp ⁡ M
10 ssid ⊢ Z ⊆ Z
11 1 cntrsubgnsg ⊢ Z ∈ SubGrp ⁡ M ∧ Z ⊆ Z → Z ∈ NrmSGrp ⁡ M
12 9 10 11 sylancl ⊢ M ∈ Grp → Z ∈ NrmSGrp ⁡ M