Theorem subg0cl

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

	Ref	Expression
Hypothesis	subg0cl.i	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	subg0cl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		subg0cl.i	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqid	⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
3	2	subggrp	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
4		eqid	⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) )
5		eqid	⊢ ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) = ( 0g ‘ ( 𝐺 ↾s 𝑆 ) )
6	4 5	grpidcl	⊢ ( ( 𝐺 ↾s 𝑆 ) ∈ Grp → ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
7	3 6	syl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
8	2 1	subg0	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 = ( 0g ‘ ( 𝐺 ↾s 𝑆 ) ) )
9	2	subgbas	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
10	7 8 9	3eltr4d	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑆 )