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