subg0cl

Description: The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Hypothesis	subg0cl.i	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	subg0cl	$⊢ S \in SubGrp (G) \to \underset{˙}{0} \in S$

Step	Hyp	Ref	Expression
1		subg0cl.i	$⊢ \underset{˙}{0} = 0_{G}$
2		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
3	2	subggrp	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
4		eqid	$⊢ {Base}_{(G ↾_{𝑠} S)} = {Base}_{(G ↾_{𝑠} S)}$
5		eqid	$⊢ 0_{(G ↾_{𝑠} S)} = 0_{(G ↾_{𝑠} S)}$
6	4 5	grpidcl	$⊢ G ↾_{𝑠} S \in Grp \to 0_{(G ↾_{𝑠} S)} \in {Base}_{(G ↾_{𝑠} S)}$
7	3 6	syl	$⊢ S \in SubGrp (G) \to 0_{(G ↾_{𝑠} S)} \in {Base}_{(G ↾_{𝑠} S)}$
8	2 1	subg0	$⊢ S \in SubGrp (G) \to \underset{˙}{0} = 0_{(G ↾_{𝑠} S)}$
9	2	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{(G ↾_{𝑠} S)}$
10	7 8 9	3eltr4d	$⊢ S \in SubGrp (G) \to \underset{˙}{0} \in S$

Metamath Proof Explorer