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

Metamath Proof Explorer

Theorem subg0

Description: A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses subg0.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
subg0.i ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion subg0 ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 = ( 0g ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 subg0.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
2 subg0.i ⊢ 0 = ( 0g ‘ 𝐺 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 1 3 ressplusg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
5 4 oveqd ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐻 ) ) = ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) )
6 1 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
7 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
8 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
9 7 8 grpidcl ⊢ ( 𝐻 ∈ Grp → ( 0g ‘ 𝐻 ) ∈ ( Base ‘ 𝐻 ) )
10 6 9 syl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐻 ) ∈ ( Base ‘ 𝐻 ) )
11 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
12 7 11 8 grplid ⊢ ( ( 𝐻 ∈ Grp ∧ ( 0g ‘ 𝐻 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
13 6 10 12 syl2anc ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
14 5 13 eqtrd ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
15 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
16 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
17 16 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
18 1 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
19 10 18 eleqtrrd ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐻 ) ∈ 𝑆 )
20 17 19 sseldd ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐻 ) ∈ ( Base ‘ 𝐺 ) )
21 16 3 2 grpid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐻 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) ↔ 0 = ( 0g ‘ 𝐻 ) ) )
22 15 20 21 syl2anc ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ( ( 0g ‘ 𝐻 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) ↔ 0 = ( 0g ‘ 𝐻 ) ) )
23 14 22 mpbid ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 = ( 0g ‘ 𝐻 ) )