This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subcmn

Description: A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypothesis subgabl.h ⊢ H = G ↾ 𝑠 S
Assertion subcmn ⊢ G ∈ CMnd ∧ H ∈ Mnd → H ∈ CMnd

Proof

Step Hyp Ref Expression
1 subgabl.h ⊢ H = G ↾ 𝑠 S
2 eqidd ⊢ G ∈ CMnd ∧ H ∈ Mnd → Base H = Base H
3 eqid ⊢ Base H = Base H
4 eqid ⊢ 0 H = 0 H
5 3 4 mndidcl ⊢ H ∈ Mnd → 0 H ∈ Base H
6 n0i ⊢ 0 H ∈ Base H → ¬ Base H = ∅
7 5 6 syl ⊢ H ∈ Mnd → ¬ Base H = ∅
8 reldmress ⊢ Rel ⁡ dom ⁡ ↾ 𝑠
9 8 ovprc2 ⊢ ¬ S ∈ V → G ↾ 𝑠 S = ∅
10 1 9 eqtrid ⊢ ¬ S ∈ V → H = ∅
11 10 fveq2d ⊢ ¬ S ∈ V → Base H = Base ∅
12 base0 ⊢ ∅ = Base ∅
13 11 12 eqtr4di ⊢ ¬ S ∈ V → Base H = ∅
14 7 13 nsyl2 ⊢ H ∈ Mnd → S ∈ V
15 14 adantl ⊢ G ∈ CMnd ∧ H ∈ Mnd → S ∈ V
16 eqid ⊢ + G = + G
17 1 16 ressplusg ⊢ S ∈ V → + G = + H
18 15 17 syl ⊢ G ∈ CMnd ∧ H ∈ Mnd → + G = + H
19 simpr ⊢ G ∈ CMnd ∧ H ∈ Mnd → H ∈ Mnd
20 simpl ⊢ G ∈ CMnd ∧ H ∈ Mnd → G ∈ CMnd
21 eqid ⊢ Base G = Base G
22 1 21 ressbasss ⊢ Base H ⊆ Base G
23 22 sseli ⊢ x ∈ Base H → x ∈ Base G
24 22 sseli ⊢ y ∈ Base H → y ∈ Base G
25 21 16 cmncom ⊢ G ∈ CMnd ∧ x ∈ Base G ∧ y ∈ Base G → x + G y = y + G x
26 20 23 24 25 syl3an ⊢ G ∈ CMnd ∧ H ∈ Mnd ∧ x ∈ Base H ∧ y ∈ Base H → x + G y = y + G x
27 2 18 19 26 iscmnd ⊢ G ∈ CMnd ∧ H ∈ Mnd → H ∈ CMnd