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 ] ∼ = 𝑌 )