Theorem subg0cl

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

	Ref	Expression
Hypothesis	subg0cl.i	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	subg0cl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in S$$

Proof

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