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 \in CMnd \land H \in Mnd) \to H \in CMnd$

Step	Hyp	Ref	Expression
1		subgabl.h	$⊢ H = G ↾_{𝑠} S$
2		eqidd	$⊢ (G \in CMnd \land H \in Mnd) \to {Base}_{H} = {Base}_{H}$
3		eqid	$⊢ {Base}_{H} = {Base}_{H}$
4		eqid	$⊢ 0_{H} = 0_{H}$
5	3 4	mndidcl	$⊢ H \in Mnd \to 0_{H} \in {Base}_{H}$
6		n0i	$⊢ 0_{H} \in {Base}_{H} \to \neg {Base}_{H} = \emptyset$
7	5 6	syl	$⊢ H \in Mnd \to \neg {Base}_{H} = \emptyset$
8		reldmress	$⊢ Rel dom ↾_{𝑠}$
9	8	ovprc2	$⊢ \neg S \in V \to G ↾_{𝑠} S = \emptyset$
10	1 9	eqtrid	$⊢ \neg S \in V \to H = \emptyset$
11	10	fveq2d	$⊢ \neg S \in V \to {Base}_{H} = {Base}_{\emptyset}$
12		base0	$⊢ \emptyset = {Base}_{\emptyset}$
13	11 12	eqtr4di	$⊢ \neg S \in V \to {Base}_{H} = \emptyset$
14	7 13	nsyl2	$⊢ H \in Mnd \to S \in V$
15	14	adantl	$⊢ (G \in CMnd \land H \in Mnd) \to S \in V$
16		eqid	$⊢ +_{G} = +_{G}$
17	1 16	ressplusg	$⊢ S \in V \to +_{G} = +_{H}$
18	15 17	syl	$⊢ (G \in CMnd \land H \in Mnd) \to +_{G} = +_{H}$
19		simpr	$⊢ (G \in CMnd \land H \in Mnd) \to H \in Mnd$
20		simpl	$⊢ (G \in CMnd \land H \in Mnd) \to G \in CMnd$
21		eqid	$⊢ {Base}_{G} = {Base}_{G}$
22	1 21	ressbasss	$⊢ {Base}_{H} \subseteq {Base}_{G}$
23	22	sseli	$⊢ x \in {Base}_{H} \to x \in {Base}_{G}$
24	22	sseli	$⊢ y \in {Base}_{H} \to y \in {Base}_{G}$
25	21 16	cmncom	$⊢ (G \in CMnd \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y = y +_{G} x$
26	20 23 24 25	syl3an	$⊢ ((G \in CMnd \land H \in Mnd) \land x \in {Base}_{H} \land y \in {Base}_{H}) \to x +_{G} y = y +_{G} x$
27	2 18 19 26	iscmnd	$⊢ (G \in CMnd \land H \in Mnd) \to H \in CMnd$

Metamath Proof Explorer