Metamath Proof Explorer


Theorem eqgid

Description: The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses eqger.x 𝑋 = ( Base ‘ 𝐺 )
eqger.r = ( 𝐺 ~QG 𝑌 )
eqgid.3 0 = ( 0g𝐺 )
Assertion eqgid ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → [ 0 ] = 𝑌 )

Proof

Step Hyp Ref Expression
1 eqger.x 𝑋 = ( Base ‘ 𝐺 )
2 eqger.r = ( 𝐺 ~QG 𝑌 )
3 eqgid.3 0 = ( 0g𝐺 )
4 2 releqg Rel
5 relelec ( Rel → ( 𝑥 ∈ [ 0 ] 0 𝑥 ) )
6 4 5 ax-mp ( 𝑥 ∈ [ 0 ] 0 𝑥 )
7 subgrcl ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
8 7 adantr ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑋 ) → 𝐺 ∈ Grp )
9 eqid ( invg𝐺 ) = ( invg𝐺 )
10 3 9 grpinvid ( 𝐺 ∈ Grp → ( ( invg𝐺 ) ‘ 0 ) = 0 )
11 8 10 syl ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑋 ) → ( ( invg𝐺 ) ‘ 0 ) = 0 )
12 11 oveq1d ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑋 ) → ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) = ( 0 ( +g𝐺 ) 𝑥 ) )
13 eqid ( +g𝐺 ) = ( +g𝐺 )
14 1 13 3 grplid ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) → ( 0 ( +g𝐺 ) 𝑥 ) = 𝑥 )
15 7 14 sylan ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑋 ) → ( 0 ( +g𝐺 ) 𝑥 ) = 𝑥 )
16 12 15 eqtrd ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑋 ) → ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) = 𝑥 )
17 16 eleq1d ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑋 ) → ( ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌𝑥𝑌 ) )
18 17 pm5.32da ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ↔ ( 𝑥𝑋𝑥𝑌 ) ) )
19 1 subgss ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌𝑋 )
20 1 3 grpidcl ( 𝐺 ∈ Grp → 0𝑋 )
21 7 20 syl ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 0𝑋 )
22 1 9 13 2 eqgval ( ( 𝐺 ∈ Grp ∧ 𝑌𝑋 ) → ( 0 𝑥 ↔ ( 0𝑋𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ) )
23 3anass ( ( 0𝑋𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ↔ ( 0𝑋 ∧ ( 𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ) )
24 22 23 bitrdi ( ( 𝐺 ∈ Grp ∧ 𝑌𝑋 ) → ( 0 𝑥 ↔ ( 0𝑋 ∧ ( 𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ) ) )
25 24 baibd ( ( ( 𝐺 ∈ Grp ∧ 𝑌𝑋 ) ∧ 0𝑋 ) → ( 0 𝑥 ↔ ( 𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ) )
26 7 19 21 25 syl21anc ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 0 𝑥 ↔ ( 𝑥𝑋 ∧ ( ( ( invg𝐺 ) ‘ 0 ) ( +g𝐺 ) 𝑥 ) ∈ 𝑌 ) ) )
27 19 sseld ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥𝑌𝑥𝑋 ) )
28 27 pm4.71rd ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥𝑌 ↔ ( 𝑥𝑋𝑥𝑌 ) ) )
29 18 26 28 3bitr4d ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 0 𝑥𝑥𝑌 ) )
30 6 29 syl5bb ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ [ 0 ] 𝑥𝑌 ) )
31 30 eqrdv ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → [ 0 ] = 𝑌 )