Metamath Proof Explorer

Theorem submcmn2

Description: A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses subgabl.h ⊢ H = G ↾ 𝑠 S
submcmn2.z ⊢ Z = Cntz ⁡ G
Assertion submcmn2 ⊢ S ∈ SubMnd ⁡ G → H ∈ CMnd ↔ S ⊆ Z ⁡ S

Proof

Step Hyp Ref Expression
1 subgabl.h ⊢ H = G ↾ 𝑠 S
2 submcmn2.z ⊢ Z = Cntz ⁡ G
3 1 submbas ⊢ S ∈ SubMnd ⁡ G → S = Base H
4 eqid ⊢ + G = + G
5 1 4 ressplusg ⊢ S ∈ SubMnd ⁡ G → + G = + H
6 5 oveqd ⊢ S ∈ SubMnd ⁡ G → x + G y = x + H y
7 5 oveqd ⊢ S ∈ SubMnd ⁡ G → y + G x = y + H x
8 6 7 eqeq12d ⊢ S ∈ SubMnd ⁡ G → x + G y = y + G x ↔ x + H y = y + H x
9 3 8 raleqbidv ⊢ S ∈ SubMnd ⁡ G → ∀ y ∈ S x + G y = y + G x ↔ ∀ y ∈ Base H x + H y = y + H x
10 3 9 raleqbidv ⊢ S ∈ SubMnd ⁡ G → ∀ x ∈ S ∀ y ∈ S x + G y = y + G x ↔ ∀ x ∈ Base H ∀ y ∈ Base H x + H y = y + H x
11 eqid ⊢ Base G = Base G
12 11 submss ⊢ S ∈ SubMnd ⁡ G → S ⊆ Base G
13 11 4 2 sscntz ⊢ S ⊆ Base G ∧ S ⊆ Base G → S ⊆ Z ⁡ S ↔ ∀ x ∈ S ∀ y ∈ S x + G y = y + G x
14 12 12 13 syl2anc ⊢ S ∈ SubMnd ⁡ G → S ⊆ Z ⁡ S ↔ ∀ x ∈ S ∀ y ∈ S x + G y = y + G x
15 1 submmnd ⊢ S ∈ SubMnd ⁡ G → H ∈ Mnd
16 eqid ⊢ Base H = Base H
17 eqid ⊢ + H = + H
18 16 17 iscmn ⊢ H ∈ CMnd ↔ H ∈ Mnd ∧ ∀ x ∈ Base H ∀ y ∈ Base H x + H y = y + H x
19 18 baib ⊢ H ∈ Mnd → H ∈ CMnd ↔ ∀ x ∈ Base H ∀ y ∈ Base H x + H y = y + H x
20 15 19 syl ⊢ S ∈ SubMnd ⁡ G → H ∈ CMnd ↔ ∀ x ∈ Base H ∀ y ∈ Base H x + H y = y + H x
21 10 14 20 3bitr4rd ⊢ S ∈ SubMnd ⁡ G → H ∈ CMnd ↔ S ⊆ Z ⁡ S