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 ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion subcmn ( ( 𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd ) → 𝐻 ∈ CMnd )

Proof

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