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	syl5eq	⊢ ( ¬ 𝑆 ∈ 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 )