subgabl

Description: A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014)

		Ref	Expression
	Hypothesis	subgabl.h	$⊢ H = G ↾_{𝑠} S$
	Assertion	subgabl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H \in Abel$

Step	Hyp	Ref	Expression
1		subgabl.h	$⊢ H = G ↾_{𝑠} S$
2	1	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
3	2	adantl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to S = {Base}_{H}$
4		eqid	$⊢ +_{G} = +_{G}$
5	1 4	ressplusg	$⊢ S \in SubGrp (G) \to +_{G} = +_{H}$
6	5	adantl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to +_{G} = +_{H}$
7	1	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$
8	7	adantl	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H \in Grp$
9		simp1l	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to G \in Abel$
10		simp1r	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to S \in SubGrp (G)$
11		eqid	$⊢ {Base}_{G} = {Base}_{G}$
12	11	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
13	10 12	syl	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to S \subseteq {Base}_{G}$
14		simp2	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to x \in S$
15	13 14	sseldd	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to x \in {Base}_{G}$
16		simp3	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to y \in S$
17	13 16	sseldd	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to y \in {Base}_{G}$
18	11 4	ablcom	$⊢ (G \in Abel \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y = y +_{G} x$
19	9 15 17 18	syl3anc	$⊢ ((G \in Abel \land S \in SubGrp (G)) \land x \in S \land y \in S) \to x +_{G} y = y +_{G} x$
20	3 6 8 19	isabld	$⊢ (G \in Abel \land S \in SubGrp (G)) \to H \in Abel$

Metamath Proof Explorer