This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ 𝑆 )