Metamath Proof Explorer

Theorem subgcl

Description: A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Hypothesis	subgcl.p	$⊢ \underset{˙}{+} = +_{G}$
	Assertion	subgcl	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$

Proof

Step	Hyp	Ref	Expression
1		subgcl.p	$⊢ \underset{˙}{+} = +_{G}$
2		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
3	2	subggrp	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
4	3	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to G ↾_{𝑠} S \in Grp$
5		simp2	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in S$
6	2	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{(G ↾_{𝑠} S)}$
7	6	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to S = {Base}_{(G ↾_{𝑠} S)}$
8	5 7	eleqtrd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in {Base}_{(G ↾_{𝑠} S)}$
9		simp3	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in S$
10	9 7	eleqtrd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in {Base}_{(G ↾_{𝑠} S)}$
11		eqid	$⊢ {Base}_{(G ↾_{𝑠} S)} = {Base}_{(G ↾_{𝑠} S)}$
12		eqid	$⊢ +_{(G ↾_{𝑠} S)} = +_{(G ↾_{𝑠} S)}$
13	11 12	grpcl	$⊢ (G ↾_{𝑠} S \in Grp \land X \in {Base}_{(G ↾_{𝑠} S)} \land Y \in {Base}_{(G ↾_{𝑠} S)}) \to X +_{(G ↾_{𝑠} S)} Y \in {Base}_{(G ↾_{𝑠} S)}$
14	4 8 10 13	syl3anc	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X +_{(G ↾_{𝑠} S)} Y \in {Base}_{(G ↾_{𝑠} S)}$
15	2 1	ressplusg	$⊢ S \in SubGrp (G) \to \underset{˙}{+} = +_{(G ↾_{𝑠} S)}$
16	15	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to \underset{˙}{+} = +_{(G ↾_{𝑠} S)}$
17	16	oveqd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{+} Y = X +_{(G ↾_{𝑠} S)} Y$
18	14 17 7	3eltr4d	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$